diff --git a/library/data/set/equinumerosity.lean b/library/data/set/equinumerosity.lean
index 65738dcca1..b708c6c7c5 100644
--- a/library/data/set/equinumerosity.lean
+++ b/library/data/set/equinumerosity.lean
@@ -111,14 +111,15 @@ open set
   noncomputable definition h x := if x ∈ Union U then f x else ginv x
 
   lemma h_maps_to : maps_to h A B :=
+  using f_maps_to dfltB,
   take a,
   suppose a ∈ A,
   show h a ∈ B, from
     by_cases
       (suppose a ∈ Union U,
-        by rewrite [↑h, if_pos this]; exact f_maps_to `a ∈ A`)
+        begin rewrite [↑h, if_pos this], exact f_maps_to `a ∈ A` end)
       (suppose a ∉ Union U,
-        by rewrite [↑h, if_neg this]; exact ginv_maps_to `a ∈ A`)
+        begin rewrite [↑h, if_neg this], exact ginv_maps_to `a ∈ A` end)
 
   /- h is injective -/