diff --git a/library/data/set/filter.lean b/library/data/set/filter.lean
index 64fd71489..ebc12d461 100644
--- a/library/data/set/filter.lean
+++ b/library/data/set/filter.lean
@@ -401,6 +401,7 @@ le.antisymm !bot_le
   begin
     apply le_of_forall_eventually,
     intro P H,
+    unfold eventually,
     apply mem_univ
   end
 
diff --git a/library/data/set/map.lean b/library/data/set/map.lean
index 69bead8a2..f9e99a024 100644
--- a/library/data/set/map.lean
+++ b/library/data/set/map.lean
@@ -121,8 +121,10 @@ inj_on_of_left_inv_on H
 theorem left_inverse_comp {f' : map b a} {g' : map c b} {g : map b c} {f : map a b}
     (Hf : map.left_inverse f' f) (Hg : map.left_inverse g' g) :
   map.left_inverse (f' ∘ g') (g ∘ f) :=
-left_inv_on_comp (mapsto f) Hf Hg
-
+begin
+  unfold map.left_inverse,
+  exact left_inv_on_comp (mapsto f) Hf Hg
+end
 /- right inverse -/
 
 -- g is a right inverse to f