diff --git a/src/data/equiv/basic.lean b/src/data/equiv/basic.lean
index 43e07a8863d49..122c048c44161 100644
--- a/src/data/equiv/basic.lean
+++ b/src/data/equiv/basic.lean
@@ -41,20 +41,19 @@ instance : has_coe_to_fun (α ≃ β) :=
 @[simp] theorem coe_fn_mk (f : α → β) (g l r) : (equiv.mk f g l r : α → β) = f :=
 rfl
 
-theorem eq_of_to_fun_eq : ∀ {e₁ e₂ : equiv α β}, (e₁ : α → β) = e₂ → e₁ = e₂
+/-- The map `coe_fn : (r ≃ s) → (r → s)` is injective. We can't use `function.injective`
+here but mimic its signature by using `⦃e₁ e₂⦄`. -/
+theorem coe_fn_injective : ∀ ⦃e₁ e₂ : equiv α β⦄, (e₁ : α → β) = e₂ → e₁ = e₂
 | ⟨f₁, g₁, l₁, r₁⟩ ⟨f₂, g₂, l₂, r₂⟩ h :=
   have f₁ = f₂, from h,
-  have g₁ = g₂, from funext $ assume x,
-    have f₁ (g₁ x) = f₂ (g₂ x), from (r₁ x).trans (r₂ x).symm,
-    have f₁ (g₁ x) = f₁ (g₂ x), by { subst f₂, exact this },
-    show g₁ x = g₂ x,           from l₁.injective this,
+  have g₁ = g₂, from l₁.eq_right_inverse (this.symm ▸ r₂),
   by simp *
 
-@[ext] lemma ext (f g : equiv α β) (H : ∀ x, f x = g x) : f = g :=
-eq_of_to_fun_eq (funext H)
+@[ext] lemma ext {f g : equiv α β} (H : ∀ x, f x = g x) : f = g :=
+coe_fn_injective (funext H)
 
-@[ext] lemma perm.ext (σ τ : equiv.perm α) (H : ∀ x, σ x = τ x) : σ = τ :=
-equiv.ext _ _ H
+@[ext] lemma perm.ext {σ τ : equiv.perm α} (H : ∀ x, σ x = τ x) : σ = τ :=
+equiv.ext H
 
 @[refl] protected def refl (α : Sort*) : α ≃ α := ⟨id, id, λ x, rfl, λ x, rfl⟩
 
@@ -136,13 +135,13 @@ lemma eq_symm_apply {α β} (e : α ≃ β) {x y} : y = e.symm x ↔ e y = x :=
 
 @[simp] theorem refl_trans (e : α ≃ β) : (equiv.refl α).trans e = e := by { cases e, refl }
 
-@[simp] theorem symm_trans (e : α ≃ β) : e.symm.trans e = equiv.refl β :=  ext _ _ (by simp)
+@[simp] theorem symm_trans (e : α ≃ β) : e.symm.trans e = equiv.refl β := ext (by simp)
 
-@[simp] theorem trans_symm (e : α ≃ β) : e.trans e.symm = equiv.refl α := ext _ _ (by simp)
+@[simp] theorem trans_symm (e : α ≃ β) : e.trans e.symm = equiv.refl α := ext (by simp)
 
 lemma trans_assoc {δ} (ab : α ≃ β) (bc : β ≃ γ) (cd : γ ≃ δ) :
   (ab.trans bc).trans cd = ab.trans (bc.trans cd) :=
-equiv.ext _ _ $ assume a, rfl
+equiv.ext $ assume a, rfl
 
 theorem left_inverse_symm (f : equiv α β) : left_inverse f.symm f := f.left_inv
 
@@ -244,8 +243,8 @@ def of_iff {P Q : Prop} (h : P ↔ Q) : P ≃ Q :=
   (α₁ → β₁) ≃ (α₂ → β₂) :=
 { to_fun := λ f, e₂.to_fun ∘ f ∘ e₁.inv_fun,
   inv_fun := λ f, e₂.inv_fun ∘ f ∘ e₁.to_fun,
-  left_inv := λ f, funext $ λ x, by { dsimp, simp },
-  right_inv := λ f, funext $ λ x, by { dsimp, simp } }
+  left_inv := λ f, funext $ λ x, by simp,
+  right_inv := λ f, funext $ λ x, by simp }
 
 @[simp] lemma arrow_congr_apply {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂)
   (f : α₁ → β₁) (x : α₂) :
@@ -1028,10 +1027,10 @@ def swap (a b : α) : perm α :=
 ⟨swap_core a b, swap_core a b, λr, swap_core_swap_core r a b, λr, swap_core_swap_core r a b⟩
 
 theorem swap_self (a : α) : swap a a = equiv.refl _ :=
-eq_of_to_fun_eq $ funext $ λ r, swap_core_self r a
+ext $ λ r, swap_core_self r a
 
 theorem swap_comm (a b : α) : swap a b = swap b a :=
-eq_of_to_fun_eq $ funext $ λ r, swap_core_comm r _ _
+ext $ λ r, swap_core_comm r _ _
 
 theorem swap_apply_def (a b x : α) : swap a b x = if x = a then b else if x = b then a else x :=
 rfl
@@ -1046,7 +1045,7 @@ theorem swap_apply_of_ne_of_ne {a b x : α} : x ≠ a → x ≠ b → swap a b x
 by simp [swap_apply_def] {contextual := tt}
 
 @[simp] theorem swap_swap (a b : α) : (swap a b).trans (swap a b) = equiv.refl _ :=
-eq_of_to_fun_eq $ funext $ λ x, swap_core_swap_core _ _ _
+ext $ λ x, swap_core_swap_core _ _ _
 
 theorem swap_comp_apply {a b x : α} (π : perm α) :
   π.trans (swap a b) x = if π x = a then b else if π x = b then a else π x :=
@@ -1057,7 +1056,7 @@ by { cases π, refl }
 
 @[simp] lemma symm_trans_swap_trans [decidable_eq β] (a b : α)
   (e : α ≃ β) : (e.symm.trans (swap a b)).trans e = swap (e a) (e b) :=
-equiv.ext _ _ (λ x, begin
+equiv.ext (λ x, begin
   have : ∀ a, e.symm x = a ↔ x = e a :=
     λ a, by { rw @eq_comm _ (e.symm x), split; intros; simp * at * },
   simp [swap_apply_def, this],
diff --git a/src/data/equiv/local_equiv.lean b/src/data/equiv/local_equiv.lean
index d9e05714e04ae..c35aef05cfc3c 100644
--- a/src/data/equiv/local_equiv.lean
+++ b/src/data/equiv/local_equiv.lean
@@ -192,7 +192,7 @@ lemma target_subset_preimage_source : e.target ⊆ e.symm ⁻¹' e.source :=
 
 /-- Two local equivs that have the same `source`, same `to_fun` and same `inv_fun`, coincide. -/
 @[ext]
-protected lemma ext (e' : local_equiv α β) (h : ∀x, e x = e' x)
+protected lemma ext {e e' : local_equiv α β} (h : ∀x, e x = e' x)
   (hsymm : ∀x, e.symm x = e'.symm x) (hs : e.source = e'.source) : e = e' :=
 begin
   have A : (e : α → β) = e', by { ext x, exact h x },
@@ -234,7 +234,7 @@ protected def restr (s : set α) : local_equiv α β :=
 
 lemma restr_eq_of_source_subset {e : local_equiv α β} {s : set α} (h : e.source ⊆ s) :
   e.restr s = e :=
-local_equiv.ext _ _ (λ_, rfl) (λ_, rfl) (by simp [inter_eq_self_of_subset_left h])
+local_equiv.ext (λ_, rfl) (λ_, rfl) (by simp [inter_eq_self_of_subset_left h])
 
 @[simp] lemma restr_univ {e : local_equiv α β} : e.restr univ = e :=
 restr_eq_of_source_subset (subset_univ _)
@@ -329,25 +329,25 @@ lemma inv_image_trans_target : e'.symm '' (e.trans e').target = e'.source ∩ e.
 image_trans_source e'.symm e.symm
 
 lemma trans_assoc (e'' : local_equiv γ δ) : (e.trans e').trans e'' = e.trans (e'.trans e'') :=
-local_equiv.ext _ _ (λx, rfl) (λx, rfl) (by simp [trans_source, @preimage_comp α β γ, inter_assoc])
+local_equiv.ext (λx, rfl) (λx, rfl) (by simp [trans_source, @preimage_comp α β γ, inter_assoc])
 
 @[simp] lemma trans_refl : e.trans (local_equiv.refl β) = e :=
-local_equiv.ext _ _ (λx, rfl) (λx, rfl) (by simp [trans_source])
+local_equiv.ext (λx, rfl) (λx, rfl) (by simp [trans_source])
 
 @[simp] lemma refl_trans : (local_equiv.refl α).trans e = e :=
-local_equiv.ext _ _ (λx, rfl) (λx, rfl) (by simp [trans_source, preimage_id])
+local_equiv.ext (λx, rfl) (λx, rfl) (by simp [trans_source, preimage_id])
 
 lemma trans_refl_restr (s : set β) :
   e.trans ((local_equiv.refl β).restr s) = e.restr (e ⁻¹' s) :=
-local_equiv.ext _ _ (λx, rfl) (λx, rfl) (by simp [trans_source])
+local_equiv.ext (λx, rfl) (λx, rfl) (by simp [trans_source])
 
 lemma trans_refl_restr' (s : set β) :
   e.trans ((local_equiv.refl β).restr s) = e.restr (e.source ∩ e ⁻¹' s) :=
-local_equiv.ext _ _ (λx, rfl) (λx, rfl) $ by { simp [trans_source], rw [← inter_assoc, inter_self] }
+local_equiv.ext (λx, rfl) (λx, rfl) $ by { simp [trans_source], rw [← inter_assoc, inter_self] }
 
 lemma restr_trans (s : set α) :
   (e.restr s).trans e' = (e.trans e').restr s :=
-local_equiv.ext _ _ (λx, rfl) (λx, rfl) $ by { simp [trans_source, inter_comm], rwa inter_assoc }
+local_equiv.ext (λx, rfl) (λx, rfl) $ by { simp [trans_source, inter_comm], rwa inter_assoc }
 
 /-- `eq_on_source e e'` means that `e` and `e'` have the same source, and coincide there. Then `e`
 and `e'` should really be considered the same local equiv. -/
@@ -464,7 +464,7 @@ trans_self_symm (e.symm)
 lemma eq_of_eq_on_source_univ (e e' : local_equiv α β) (h : e ≈ e')
   (s : e.source = univ) (t : e.target = univ) : e = e' :=
 begin
-  apply local_equiv.ext _ _ (λx, _) (λx, _) h.1,
+  apply local_equiv.ext (λx, _) (λx, _) h.1,
   { apply h.2 x,
     rw s,
     exact mem_univ _ },
@@ -540,6 +540,6 @@ variables (e : equiv α β) (e' : equiv β γ)
 @[simp] lemma symm_to_local_equiv : e.symm.to_local_equiv = e.to_local_equiv.symm := rfl
 @[simp] lemma trans_to_local_equiv :
   (e.trans e').to_local_equiv = e.to_local_equiv.trans e'.to_local_equiv :=
-local_equiv.ext _ _ (λx, rfl) (λx, rfl) (by simp [local_equiv.trans_source, equiv.to_local_equiv])
+local_equiv.ext (λx, rfl) (λx, rfl) (by simp [local_equiv.trans_source, equiv.to_local_equiv])
 
 end equiv
diff --git a/src/data/equiv/mul_add.lean b/src/data/equiv/mul_add.lean
index b39746aea8b57..b0897fce5df3f 100644
--- a/src/data/equiv/mul_add.lean
+++ b/src/data/equiv/mul_add.lean
@@ -162,7 +162,7 @@ instance is_group_hom {G H} [group G] [group H] (h : G ≃* H) :
   "Two additive isomorphisms agree if they are defined by the same underlying function."]
 lemma ext {f g : mul_equiv M N} (h : ∀ x, f x = g x) : f = g :=
 begin
-  have h₁ := equiv.ext f.to_equiv g.to_equiv h,
+  have h₁ : f.to_equiv = g.to_equiv := equiv.ext h,
   cases f, cases g, congr,
   { exact (funext h) },
   { exact congr_arg equiv.inv_fun h₁ }
diff --git a/src/data/equiv/ring.lean b/src/data/equiv/ring.lean
index 561954fa19511..5557539ed8c45 100644
--- a/src/data/equiv/ring.lean
+++ b/src/data/equiv/ring.lean
@@ -198,7 +198,7 @@ end ring_hom
 @[ext] lemma ext {R S : Type*} [has_mul R] [has_add R] [has_mul S] [has_add S]
   {f g : R ≃+* S} (h : ∀ x, f x = g x) : f = g :=
 begin
-  have h₁ := equiv.ext f.to_equiv g.to_equiv h,
+  have h₁ : f.to_equiv = g.to_equiv := equiv.ext h,
   cases f, cases g, congr,
   { exact (funext h) },
   { exact congr_arg equiv.inv_fun h₁ }
diff --git a/src/data/fintype/basic.lean b/src/data/fintype/basic.lean
index 39a2d05ccae3b..eeb8b575d6b47 100644
--- a/src/data/fintype/basic.lean
+++ b/src/data/fintype/basic.lean
@@ -71,7 +71,7 @@ decidable_of_iff (∃ a ∈ @univ α _, p a) (by simp)
 
 instance decidable_eq_equiv_fintype [decidable_eq β] [fintype α] :
   decidable_eq (α ≃ β) :=
-λ a b, decidable_of_iff (a.1 = b.1) ⟨λ h, equiv.ext _ _ (congr_fun h), congr_arg _⟩
+λ a b, decidable_of_iff (a.1 = b.1) ⟨λ h, equiv.ext (congr_fun h), congr_arg _⟩
 
 instance decidable_injective_fintype [decidable_eq α] [decidable_eq β] [fintype α] :
   decidable_pred (injective : (α → β) → Prop) := λ x, by unfold injective; apply_instance
@@ -711,7 +711,7 @@ begin
 end
 
 lemma mem_perms_of_list_of_mem : ∀ {l : list α} {f : perm α} (h : ∀ x, f x ≠ x → x ∈ l), f ∈ perms_of_list l
-| []     f h := list.mem_singleton.2 $ equiv.ext _ _$ λ x, by simp [imp_false, *] at *
+| []     f h := list.mem_singleton.2 $ equiv.ext $ λ x, by simp [imp_false, *] at *
 | (a::l) f h :=
 if hfa : f a = a
 then
diff --git a/src/group_theory/group_action.lean b/src/group_theory/group_action.lean
index 31145732e3293..0994ae417bbb4 100644
--- a/src/group_theory/group_action.lean
+++ b/src/group_theory/group_action.lean
@@ -156,7 +156,7 @@ def to_perm (g : α) : equiv.perm β :=
 variables {α} {β}
 
 instance : is_group_hom (to_perm α β) :=
-{ map_mul := λ x y, equiv.ext _ _ (λ a, mul_action.mul_smul x y a) }
+{ map_mul := λ x y, equiv.ext (λ a, mul_action.mul_smul x y a) }
 
 lemma bijective (g : α) : function.bijective (λ b : β, g • b) :=
 (to_perm α β g).bijective
diff --git a/src/group_theory/perm/cycles.lean b/src/group_theory/perm/cycles.lean
index 4cf2f71275f0f..99cd5289872ad 100644
--- a/src/group_theory/perm/cycles.lean
+++ b/src/group_theory/perm/cycles.lean
@@ -68,7 +68,7 @@ lemma cycle_of_apply [fintype α] (f : perm α) (x y : α) :
 
 lemma cycle_of_inv [fintype α] (f : perm α) (x : α) :
   (cycle_of f x)⁻¹ = cycle_of f⁻¹ x :=
-equiv.ext _ _ $ λ y, begin
+equiv.ext $ λ y, begin
   rw [inv_eq_iff_eq, cycle_of_apply, cycle_of_apply];
   split_ifs; simp [*, same_cycle_inv, same_cycle_inv_apply] at *
 end
@@ -97,7 +97,7 @@ lemma cycle_of_apply_of_not_same_cycle [fintype α] {f : perm α} {x y : α} (h
 
 lemma cycle_of_cycle [fintype α] {f : perm α} (hf : is_cycle f) {x : α} (hx : f x ≠ x) :
   cycle_of f x = f :=
-equiv.ext _ _ $ λ y,
+equiv.ext $ λ y,
   if h : same_cycle f x y then by rw [cycle_of_apply_of_same_cycle h]
   else by rw [cycle_of_apply_of_not_same_cycle h, not_not.1 (mt ((same_cycle_cycle hx).1 hf).2 h)]
 
diff --git a/src/group_theory/perm/sign.lean b/src/group_theory/perm/sign.lean
index 164608e7eb2d4..12af03d64ac8c 100644
--- a/src/group_theory/perm/sign.lean
+++ b/src/group_theory/perm/sign.lean
@@ -17,7 +17,7 @@ def subtype_perm (f : perm α) {p : α → Prop} (h : ∀ x, p x ↔ p (f x)) :
   λ _, by simp, λ _, by simp⟩
 
 @[simp] lemma subtype_perm_one (p : α → Prop) (h : ∀ x, p x ↔ p ((1 : perm α) x)) : @subtype_perm α 1 p h = 1 :=
-equiv.ext _ _ $ λ ⟨_, _⟩, rfl
+equiv.ext $ λ ⟨_, _⟩, rfl
 
 def of_subtype {p : α → Prop} [decidable_pred p] (f : perm (subtype p)) : perm α :=
 ⟨λ x, if h : p x then f ⟨x, h⟩ else x, λ x, if h : p x then f⁻¹ ⟨x, h⟩ else x,
@@ -27,7 +27,7 @@ def of_subtype {p : α → Prop} [decidable_pred p] (f : perm (subtype p)) : per
     by simp; split_ifs at *; simp * at *⟩
 
 instance of_subtype.is_group_hom {p : α → Prop} [decidable_pred p] : is_group_hom (@of_subtype α p _) :=
-{ map_mul := λ f g, equiv.ext _ _ $ λ x, begin
+{ map_mul := λ f g, equiv.ext $ λ x, begin
   rw [of_subtype, of_subtype, of_subtype],
   by_cases h : p x,
   { have h₁ : p (f (g ⟨x, h⟩)), from (f (g ⟨x, h⟩)).2,
@@ -56,7 +56,7 @@ lemma disjoint_comm {f g : perm α} : disjoint f g ↔ disjoint g f :=
 ⟨disjoint.symm, disjoint.symm⟩
 
 lemma disjoint_mul_comm {f g : perm α} (h : disjoint f g) : f * g = g * f :=
-equiv.ext _ _ $ λ x, (h x).elim
+equiv.ext $ λ x, (h x).elim
   (λ hf, (h (g x)).elim (λ hg, by simp [mul_apply, hf, hg])
     (λ hg, by simp [mul_apply, hf, g.injective hg]))
   (λ hg, (h (f x)).elim (λ hf, by simp [mul_apply, f.injective hf, hg])
@@ -90,7 +90,7 @@ hp.prod_eq' $ hl.imp $ λ f g, disjoint_mul_comm
 
 lemma of_subtype_subtype_perm {f : perm α} {p : α → Prop} [decidable_pred p] (h₁ : ∀ x, p x ↔ p (f x))
   (h₂ : ∀ x, f x ≠ x → p x) : of_subtype (subtype_perm f h₁) = f :=
-equiv.ext _ _ $ λ x, begin
+equiv.ext $ λ x, begin
   rw [of_subtype, subtype_perm],
   by_cases hx : p x,
   { simp [hx] },
@@ -108,7 +108,7 @@ else by simp [h, of_subtype_apply_of_not_mem f h]
 
 @[simp] lemma subtype_perm_of_subtype {p : α → Prop} [decidable_pred p] (f : perm (subtype p)) :
   subtype_perm (of_subtype f) (mem_iff_of_subtype_apply_mem f) = f :=
-equiv.ext _ _ $ λ ⟨x, hx⟩, by dsimp [subtype_perm, of_subtype]; simp [show p x, from hx]
+equiv.ext $ λ ⟨x, hx⟩, by dsimp [subtype_perm, of_subtype]; simp [show p x, from hx]
 
 lemma pow_apply_eq_self_of_apply_eq_self {f : perm α} {x : α} (hfx : f x = x) :
   ∀ n : ℕ, (f ^ n) x = x
@@ -145,7 +145,7 @@ by simp [support]
 def is_swap (f : perm α) := ∃ x y, x ≠ y ∧ f = swap x y
 
 lemma swap_mul_eq_mul_swap (f : perm α) (x y : α) : swap x y * f = f * swap (f⁻¹ x) (f⁻¹ y) :=
-equiv.ext _ _ $ λ z, begin
+equiv.ext $ λ z, begin
   simp [mul_apply, swap_apply_def],
   split_ifs;
   simp [*, eq_inv_iff_eq] at * <|> cc
@@ -171,7 +171,7 @@ lemma is_swap_of_subtype {p : α → Prop} [decidable_pred p]
   {f : perm (subtype p)} (h : is_swap f) : is_swap (of_subtype f) :=
 let ⟨⟨x, hx⟩, ⟨y, hy⟩, hxy⟩ := h in
 ⟨x, y, by simp at hxy; tauto,
-  equiv.ext _ _ $ λ z, begin
+  equiv.ext $ λ z, begin
     rw [hxy.2, of_subtype],
     simp [swap_apply_def],
     split_ifs;
@@ -207,7 +207,7 @@ finset.card_lt_card
 
 def swap_factors_aux : Π (l : list α) (f : perm α), (∀ {x}, f x ≠ x → x ∈ l) →
   {l : list (perm α) // l.prod = f ∧ ∀ g ∈ l, is_swap g}
-| []       := λ f h, ⟨[], equiv.ext _ _ $ λ x, by rw [list.prod_nil];
+| []       := λ f h, ⟨[], equiv.ext $ λ x, by rw [list.prod_nil];
     exact eq.symm (not_not.1 (mt h (list.not_mem_nil _))), by simp⟩
 | (x :: l) := λ f h,
 if hfx : x = f x
@@ -248,7 +248,7 @@ end
 
 lemma swap_mul_swap_mul_swap {x y z : α} (hwz: x ≠ y) (hxz : x ≠ z) :
   swap y z * swap x y * swap y z = swap z x :=
-equiv.ext _ _ $ λ n, by simp only [swap_apply_def, mul_apply]; split_ifs; cc
+equiv.ext $ λ n, by simp only [swap_apply_def, mul_apply]; split_ifs; cc
 
 lemma is_conj_swap {w x y z : α} (hwx : w ≠ x) (hyz : y ≠ z) : is_conj (swap w x) (swap y z) :=
 have h : ∀ {y z : α}, y ≠ z → w ≠ z →
@@ -399,7 +399,7 @@ def sign_aux2 : list α → perm α → units ℤ
 
 lemma sign_aux_eq_sign_aux2 {n : ℕ} : ∀ (l : list α) (f : perm α) (e : α ≃ fin n)
   (h : ∀ x, f x ≠ x → x ∈ l), sign_aux ((e.symm.trans f).trans e) = sign_aux2 l f
-| []     f e h := have f = 1, from equiv.ext _ _ $
+| []     f e h := have f = 1, from equiv.ext $
   λ y, not_not.1 (mt (h y) (list.not_mem_nil _)),
 by rw [this, one_def, equiv.trans_refl, equiv.symm_trans, ← one_def,
   sign_aux_one, sign_aux2]
@@ -439,7 +439,7 @@ begin
   show sign_aux2 l (f * g) = sign_aux2 l f * sign_aux2 l g ∧
     ∀ x y, x ≠ y → sign_aux2 l (swap x y) = -1,
   have hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e,
-    from equiv.ext _ _ (λ h, by simp [mul_apply]),
+    from equiv.ext (λ h, by simp [mul_apply]),
   split,
   { rw [← sign_aux_eq_sign_aux2 _ _ e (λ _ _, hs _), ← sign_aux_eq_sign_aux2 _ _ e (λ _ _, hs _),
       ← sign_aux_eq_sign_aux2 _ _ e (λ _ _, hs _), hfg, sign_aux_mul] },
@@ -491,7 +491,7 @@ quotient.induction_on₂ t s
     from let n := trunc.out (equiv_fin β) in
     by rw [← sign_aux_eq_sign_aux2 _ _ n (λ _ _, h₁ _),
         ← sign_aux_eq_sign_aux2 _ _ (e.trans n) (λ _ _, h₂ _)];
-      exact congr_arg sign_aux (equiv.ext _ _ (λ x, by simp)))
+      exact congr_arg sign_aux (equiv.ext (λ x, by simp)))
   ht hs
 
 lemma sign_symm_trans_trans [decidable_eq β] [fintype β] (f : perm α)
@@ -554,7 +554,7 @@ by conv {to_rhs, rw [← subtype_perm_of_subtype f, sign_subtype_perm _ _ this]}
 
 lemma sign_eq_sign_of_equiv [decidable_eq β] [fintype β] (f : perm α) (g : perm β)
   (e : α ≃ β) (h : ∀ x, e (f x) = g (e x)) : sign f = sign g :=
-have hg : g = (e.symm.trans f).trans e, from equiv.ext _ _ $ by simp [h],
+have hg : g = (e.symm.trans f).trans e, from equiv.ext $ by simp [h],
 by rw [hg, sign_symm_trans_trans]
 
 lemma sign_bij [decidable_eq β] [fintype β]
@@ -640,7 +640,7 @@ lemma is_cycle_swap_mul_aux₂ : ∀ (n : ℤ) {b x : α} {f : perm α}
 
 lemma eq_swap_of_is_cycle_of_apply_apply_eq_self {f : perm α} (hf : is_cycle f) {x : α}
   (hfx : f x ≠ x) (hffx : f (f x) = x) : f = swap x (f x) :=
-equiv.ext _ _ $ λ y,
+equiv.ext $ λ y,
 let ⟨z, hz⟩ := hf in
 let ⟨i, hi⟩ := hz.2 x hfx in
 if hyx : y = x then by simp [hyx]
diff --git a/src/linear_algebra/basic.lean b/src/linear_algebra/basic.lean
index 1a8164cc16327..079e1a2f419ae 100644
--- a/src/linear_algebra/basic.lean
+++ b/src/linear_algebra/basic.lean
@@ -1436,8 +1436,8 @@ variables (e e' : M ≃ₗ[R] M₂)
 
 section
 variables {e e'}
-@[ext] lemma ext (h : (e : M → M₂) = e') : e = e' :=
-to_equiv_injective (equiv.eq_of_to_fun_eq h)
+@[ext] lemma ext (h : ∀ x, e x = e' x) : e = e' :=
+to_equiv_injective (equiv.ext h)
 end
 
 section
diff --git a/src/linear_algebra/determinant.lean b/src/linear_algebra/determinant.lean
index dd6b41c31b241..346637ba3956e 100644
--- a/src/linear_algebra/determinant.lean
+++ b/src/linear_algebra/determinant.lean
@@ -25,7 +25,7 @@ univ.sum (λ (σ : perm n), ε σ * univ.prod (λ i, M (σ i) i))
 begin
   refine (finset.sum_eq_single 1 _ _).trans _,
   { intros σ h1 h2,
-    cases not_forall.1 (mt (equiv.ext _ _) h2) with x h3,
+    cases not_forall.1 (mt equiv.ext h2) with x h3,
     convert ring.mul_zero _,
     apply finset.prod_eq_zero,
     { change x ∈ _, simp },
@@ -66,7 +66,7 @@ begin
       by simp [sign_mul, this, sign_swap hij, prod_mul_distrib])
     (λ σ _ _ h, hij (σ.injective $ by conv {to_lhs, rw ← h}; simp))
     (λ _ _, mem_univ _)
-    (λ _ _, equiv.ext _ _ $ by simp)
+    (λ _ _, equiv.ext $ by simp)
 end
 
 @[simp] lemma det_mul (M N : matrix n n R) : det (M ⬝ N) = det M * det N :=
@@ -82,7 +82,7 @@ calc det (M ⬝ N) = univ.sum (λ p : n → n, univ.sum
     (λ σ : perm n, ε σ * univ.prod (λ i, M (σ i) (τ i) * N (τ i) i))) :
   sum_bij (λ p h, equiv.of_bijective (mem_filter.1 h).2) (λ _ _, mem_univ _)
     (λ _ _, rfl) (λ _ _ _ _ h, by injection h)
-    (λ b _, ⟨b, mem_filter.2 ⟨mem_univ _, b.bijective⟩, eq_of_to_fun_eq rfl⟩)
+    (λ b _, ⟨b, mem_filter.2 ⟨mem_univ _, b.bijective⟩, coe_fn_injective rfl⟩)
 ... = univ.sum (λ σ : perm n, univ.sum (λ τ : perm n,
     (univ.prod (λ i, N (σ i) i) * ε τ) * univ.prod (λ j, M (τ j) (σ j)))) :
   by simp [mul_sum, det, mul_comm, mul_left_comm, prod_mul_distrib, mul_assoc]
diff --git a/src/logic/function/basic.lean b/src/logic/function/basic.lean
index 6c54aa795522e..1ef4eb05c2360 100644
--- a/src/logic/function/basic.lean
+++ b/src/logic/function/basic.lean
@@ -115,6 +115,12 @@ theorem right_inverse.injective {f : α → β} {g : β → α} (h : right_inver
   injective f :=
 h.left_inverse.injective
 
+theorem left_inverse.eq_right_inverse {f : α → β} {g₁ g₂ : β → α} (h₁ : left_inverse g₁ f)
+  (h₂ : right_inverse g₂ f) :
+  g₁ = g₂ :=
+calc g₁ = g₁ ∘ f ∘ g₂ : by rw [h₂.comp_eq_id, comp.right_id]
+    ... = g₂          : by rw [← comp.assoc, h₁.comp_eq_id, comp.left_id]
+
 local attribute [instance, priority 10] classical.prop_decidable
 
 /-- We can use choice to construct explicitly a partial inverse for
diff --git a/src/order/order_iso.lean b/src/order/order_iso.lean
index 9fff2b5d009da..25fd1d3d784ec 100644
--- a/src/order/order_iso.lean
+++ b/src/order/order_iso.lean
@@ -52,8 +52,10 @@ theorem ord (f : r ≼o s) : ∀ {a b}, r a b ↔ s (f a) (f b) := f.ord'
 
 @[simp] theorem coe_fn_to_embedding (f : r ≼o s) : (f.to_embedding : α → β) = f := rfl
 
-theorem eq_of_to_fun_eq : ∀ {e₁ e₂ : r ≼o s}, (e₁ : α → β) = e₂ → e₁ = e₂
-| ⟨⟨f₁, h₁⟩, o₁⟩ ⟨⟨f₂, h₂⟩, o₂⟩ h := by congr; exact h
+/-- The map `coe_fn : (r ≼o s) → (r → s)` is injective. We can't use `function.injective`
+here but mimic its signature by using `⦃e₁ e₂⦄`. -/
+theorem coe_fn_injective : ∀ ⦃e₁ e₂ : r ≼o s⦄, (e₁ : α → β) = e₂ → e₁ = e₂
+| ⟨⟨f₁, h₁⟩, o₁⟩ ⟨⟨f₂, h₂⟩, o₂⟩ h := by { congr, exact h }
 
 @[refl] protected def refl (r : α → α → Prop) : r ≼o r :=
 ⟨embedding.refl _, λ a b, iff.rfl⟩
@@ -227,8 +229,10 @@ lemma ord'' {r : α → α → Prop} {s : β → β → Prop} (f : r ≃o s) {x
 
 @[simp] theorem coe_fn_to_equiv (f : r ≃o s) : (f.to_equiv : α → β) = f := rfl
 
-theorem eq_of_to_fun_eq : ∀ {e₁ e₂ : r ≃o s}, (e₁ : α → β) = e₂ → e₁ = e₂
-| ⟨e₁, o₁⟩ ⟨e₂, o₂⟩ h := by congr; exact equiv.eq_of_to_fun_eq h
+/-- The map `coe_fn : (r ≃o s) → (r → s)` is injective. We can't use `function.injective`
+here but mimic its signature by using `⦃e₁ e₂⦄`. -/
+theorem coe_fn_injective : ∀ ⦃e₁ e₂ : r ≃o s⦄, (e₁ : α → β) = e₂ → e₁ = e₂
+| ⟨e₁, o₁⟩ ⟨e₂, o₂⟩ h := by { congr, exact equiv.coe_fn_injective h }
 
 @[refl] protected def refl (r : α → α → Prop) : r ≃o r :=
 ⟨equiv.refl _, λ a b, iff.rfl⟩
diff --git a/src/set_theory/ordinal.lean b/src/set_theory/ordinal.lean
index 39024d1e0cb21..0cb0a750ea8ec 100644
--- a/src/set_theory/ordinal.lean
+++ b/src/set_theory/ordinal.lean
@@ -17,7 +17,9 @@ universes u v w
 variables {α : Type*} {β : Type*} {γ : Type*}
   {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
 
-/-- If `r` is a relation on `α` and `s` in a relation on `β`, then `f : r ≼i s` is an order embedding whose range is an initial segment. That is, whenever `b < f a` in `β` then `b` is in the range of `f`. -/
+/-- If `r` is a relation on `α` and `s` in a relation on `β`, then `f : r ≼i s` is an order
+embedding whose range is an initial segment. That is, whenever `b < f a` in `β` then `b` is in the
+range of `f`. -/
 structure initial_seg {α β : Type*} (r : α → α → Prop) (s : β → β → Prop) extends r ≼o s :=
 (init : ∀ a b, s b (to_order_embedding a) → ∃ a', to_order_embedding a' = b)
 
@@ -66,7 +68,7 @@ theorem unique_of_extensional [is_extensional β s] :
   well_founded r → subsingleton (r ≼i s) | ⟨h⟩ :=
 ⟨λ f g, begin
   suffices : (f : α → β) = g, { cases f, cases g,
-    congr, exact order_embedding.eq_of_to_fun_eq this },
+    congr, exact order_embedding.coe_fn_injective this },
   funext a, have := h a, induction this with a H IH,
   refine @is_extensional.ext _ s _ _ _ (λ x, ⟨λ h, _, λ h, _⟩),
   { rcases f.init_iff.1 h with ⟨y, rfl, h'⟩,
@@ -95,7 +97,7 @@ by haveI := f.to_order_embedding.is_well_order; exact
 
 @[simp] theorem antisymm_symm [is_well_order α r] [is_well_order β s]
   (f : r ≼i s) (g : s ≼i r) : (antisymm f g).symm = antisymm g f :=
-order_iso.eq_of_to_fun_eq rfl
+order_iso.coe_fn_injective rfl
 
 theorem eq_or_principal [is_well_order β s] (f : r ≼i s) : surjective f ∨ ∃ b, ∀ x, s x b ↔ ∃ y, f y = x :=
 or_iff_not_imp_right.2 $ λ h b,
@@ -211,7 +213,7 @@ instance [is_well_order β s] : subsingleton (r ≺i s) :=
   { refine @is_extensional.ext _ s _ _ _ (λ x, _),
     simp only [f.down, g.down, ef, coe_fn_to_order_embedding] },
   cases f, cases g,
-  have := order_embedding.eq_of_to_fun_eq ef; congr'
+  have := order_embedding.coe_fn_injective ef; congr'
 end⟩
 
 theorem top_eq [is_well_order γ t]
diff --git a/src/topology/local_homeomorph.lean b/src/topology/local_homeomorph.lean
index 403f025ae6057..171fdf65e61ae 100644
--- a/src/topology/local_homeomorph.lean
+++ b/src/topology/local_homeomorph.lean
@@ -140,7 +140,7 @@ called `eq_on_source`. -/
 @[ext]
 protected lemma ext (e' : local_homeomorph α β) (h : ∀x, e x = e' x)
   (hinv: ∀x, e.symm x = e'.symm x) (hs : e.source = e'.source) : e = e' :=
-eq_of_local_equiv_eq (local_equiv.ext e.to_local_equiv e'.to_local_equiv h hinv hs)
+eq_of_local_equiv_eq (local_equiv.ext h hinv hs)
 
 @[simp] lemma symm_to_local_equiv : e.symm.to_local_equiv = e.to_local_equiv.symm := rfl
 -- The following lemmas are already simp via local_equiv
diff --git a/src/topology/metric_space/isometry.lean b/src/topology/metric_space/isometry.lean
index c184a585e40f6..f4df1d2def4c3 100644
--- a/src/topology/metric_space/isometry.lean
+++ b/src/topology/metric_space/isometry.lean
@@ -139,7 +139,7 @@ lemma to_equiv_inj : ∀ ⦃h₁ h₂ : α ≃ᵢ β⦄, (h₁.to_equiv = h₂.t
 | ⟨e₁, h₁⟩ ⟨e₂, h₂⟩ H := by { dsimp at H, subst e₁ }
 
 @[ext] lemma ext ⦃h₁ h₂ : α ≃ᵢ β⦄ (H : ∀ x, h₁ x = h₂ x) : h₁ = h₂ :=
-to_equiv_inj $ equiv.ext _ _ H
+to_equiv_inj $ equiv.ext H
 
 /-- Alternative constructor for isometric bijections,
 taking as input an isometry, and a right inverse. -/