diff --git a/src/category_theory/adjunction.lean b/src/category_theory/adjunction.lean
index 028217dae91b4..742a0e2a8a030 100644
--- a/src/category_theory/adjunction.lean
+++ b/src/category_theory/adjunction.lean
@@ -216,8 +216,8 @@ def left_adjoint_of_equiv : C ⥤ D :=
 { obj := F_obj,
   map := λ X X' f, (e X (F_obj X')).symm (f ≫ e X' (F_obj X') (𝟙 _)),
   map_comp' := λ X X' X'' f f', begin
-    rw [equiv.symm_apply_eq, he, equiv.apply_inverse_apply],
-    conv { to_rhs, rw [assoc, ←he, id_comp, equiv.apply_inverse_apply] },
+    rw [equiv.symm_apply_eq, he, equiv.apply_symm_apply],
+    conv { to_rhs, rw [assoc, ←he, id_comp, equiv.apply_symm_apply] },
     simp
   end }
 
@@ -247,8 +247,8 @@ def right_adjoint_of_equiv : D ⥤ C :=
 { obj := G_obj,
   map := λ Y Y' g, (e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 _) ≫ g),
   map_comp' := λ Y Y' Y'' g g', begin
-    rw [← equiv.eq_symm_apply, ← he' e he, equiv.inverse_apply_apply],
-    conv { to_rhs, rw [← assoc, he' e he, comp_id, equiv.inverse_apply_apply] },
+    rw [← equiv.eq_symm_apply, ← he' e he, equiv.symm_apply_apply],
+    conv { to_rhs, rw [← assoc, he' e he, comp_id, equiv.symm_apply_apply] },
     simp
   end }
 
@@ -259,7 +259,7 @@ mk_of_hom_equiv F (right_adjoint_of_equiv e he)
   hom_equiv_naturality_right' :=
   begin
     intros X Y Y' g h,
-    erw [←he, equiv.apply_eq_iff_eq, ←assoc, he' e he, comp_id, equiv.inverse_apply_apply]
+    erw [←he, equiv.apply_eq_iff_eq, ←assoc, he' e he, comp_id, equiv.symm_apply_apply]
   end }
 
 end construct_right
diff --git a/src/data/equiv/basic.lean b/src/data/equiv/basic.lean
index c6619b8dc28d8..bcb1f0fd075fd 100644
--- a/src/data/equiv/basic.lean
+++ b/src/data/equiv/basic.lean
@@ -78,13 +78,13 @@ rfl
 
 @[simp] theorem trans_apply (f : α ≃ β) (g : β ≃ γ) (a : α) : (f.trans g) a = g (f a) := rfl
 
-@[simp] theorem apply_inverse_apply : ∀ (e : α ≃ β) (x : β), e (e.symm x) = x
+@[simp] theorem apply_symm_apply : ∀ (e : α ≃ β) (x : β), e (e.symm x) = x
 | ⟨f₁, g₁, l₁, r₁⟩ x := by simp [equiv.symm]; rw r₁
 
-@[simp] theorem inverse_apply_apply : ∀ (e : α ≃ β) (x : α), e.symm (e x) = x
+@[simp] theorem symm_apply_apply : ∀ (e : α ≃ β) (x : α), e.symm (e x) = x
 | ⟨f₁, g₁, l₁, r₁⟩ x := by simp [equiv.symm]; rw l₁
 
-@[simp] lemma inverse_trans_apply (f : α ≃ β) (g : β ≃ γ) (a : γ) :
+@[simp] lemma symm_trans_apply (f : α ≃ β) (g : β ≃ γ) (a : γ) :
   (f.trans g).symm a = f.symm (g.symm a) := rfl
 
 @[simp] theorem apply_eq_iff_eq : ∀ (f : α ≃ β) (x y : α), f x = f y ↔ x = y
@@ -145,7 +145,7 @@ instance perm_group {α : Type u} : group (perm α) :=
 begin
   refine { mul := λ f g, equiv.trans g f, one := equiv.refl α, inv:= equiv.symm, ..};
   intros; apply equiv.ext; try { apply trans_apply },
-  apply inverse_apply_apply
+  apply symm_apply_apply
 end
 
 @[simp] theorem mul_apply {α : Type u} (f g : perm α) (x) : (f * g) x = f (g x) :=
@@ -154,10 +154,10 @@ equiv.trans_apply _ _ _
 @[simp] theorem one_apply {α : Type u} (x) : (1 : perm α) x = x := rfl
 
 @[simp] lemma inv_apply_self {α : Type u} (f : perm α) (x) :
-  f⁻¹ (f x) = x := equiv.inverse_apply_apply _ _
+  f⁻¹ (f x) = x := equiv.symm_apply_apply _ _
 
 @[simp] lemma apply_inv_self {α : Type u} (f : perm α) (x) :
-  f (f⁻¹ x) = x := equiv.apply_inverse_apply _ _
+  f (f⁻¹ x) = x := equiv.apply_symm_apply _ _
 
 lemma one_def {α : Type u} : (1 : perm α) = equiv.refl α := rfl
 
@@ -233,8 +233,8 @@ end
 
 @[congr] def prod_congr {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ :β₁ ≃ β₂) : (α₁ × β₁) ≃ (α₂ × β₂) :=
 ⟨λp, (e₁ p.1, e₂ p.2), λp, (e₁.symm p.1, e₂.symm p.2),
-   λ ⟨a, b⟩, show (e₁.symm (e₁ a), e₂.symm (e₂ b)) = (a, b), by rw [inverse_apply_apply, inverse_apply_apply],
-   λ ⟨a, b⟩, show (e₁ (e₁.symm a), e₂ (e₂.symm b)) = (a, b), by rw [apply_inverse_apply, apply_inverse_apply]⟩
+   λ ⟨a, b⟩, show (e₁.symm (e₁ a), e₂.symm (e₂ b)) = (a, b), by rw [symm_apply_apply, symm_apply_apply],
+   λ ⟨a, b⟩, show (e₁ (e₁.symm a), e₂ (e₂.symm b)) = (a, b), by rw [apply_symm_apply, apply_symm_apply]⟩
 
 @[simp] theorem prod_congr_apply {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) (a : α₁) (b : β₁) :
   prod_congr e₁ e₂ (a, b) = (e₁ a, e₂ b) :=
@@ -373,8 +373,8 @@ def psigma_equiv_sigma {α} (β : α → Sort*) : psigma β ≃ sigma β :=
 
 def sigma_congr_right {α} {β₁ β₂ : α → Sort*} (F : ∀ a, β₁ a ≃ β₂ a) : sigma β₁ ≃ sigma β₂ :=
 ⟨λ ⟨a, b⟩, ⟨a, F a b⟩, λ ⟨a, b⟩, ⟨a, (F a).symm b⟩,
- λ ⟨a, b⟩, congr_arg (sigma.mk a) $ inverse_apply_apply (F a) b,
- λ ⟨a, b⟩, congr_arg (sigma.mk a) $ apply_inverse_apply (F a) b⟩
+ λ ⟨a, b⟩, congr_arg (sigma.mk a) $ symm_apply_apply (F a) b,
+ λ ⟨a, b⟩, congr_arg (sigma.mk a) $ apply_symm_apply (F a) b⟩
 
 def sigma_congr_left {α₁ α₂} {β : α₂ → Sort*} : ∀ f : α₁ ≃ α₂, (Σ a:α₁, β (f a)) ≃ (Σ a:α₂, β a)
 | ⟨f, g, l, r⟩ :=
diff --git a/src/data/equiv/denumerable.lean b/src/data/equiv/denumerable.lean
index 43baa9b6b217c..d1eb8c2981f73 100644
--- a/src/data/equiv/denumerable.lean
+++ b/src/data/equiv/denumerable.lean
@@ -51,8 +51,8 @@ def eqv (α) [denumerable α] : α ≃ ℕ :=
 def mk' {α} (e : α ≃ ℕ) : denumerable α :=
 { encode := e,
   decode := some ∘ e.symm,
-  encodek := λ a, congr_arg some (e.inverse_apply_apply _),
-  decode_inv := λ n, ⟨_, rfl, e.apply_inverse_apply _⟩ }
+  encodek := λ a, congr_arg some (e.symm_apply_apply _),
+  decode_inv := λ n, ⟨_, rfl, e.apply_symm_apply _⟩ }
 
 def of_equiv (α) {β} [denumerable α] (e : β ≃ α) : denumerable β :=
 { decode_inv := λ n, by simp,
diff --git a/src/data/finsupp.lean b/src/data/finsupp.lean
index 13aa66b0f3c2b..2b4510d485cee 100644
--- a/src/data/finsupp.lean
+++ b/src/data/finsupp.lean
@@ -1163,12 +1163,12 @@ protected def dom_congr [decidable_eq α₁] [decidable_eq α₂] [decidable_eq
 ⟨map_domain e, map_domain e.symm,
   begin
     assume v,
-    simp only [map_domain_comp.symm, (∘), equiv.inverse_apply_apply],
+    simp only [map_domain_comp.symm, (∘), equiv.symm_apply_apply],
     exact map_domain_id
   end,
   begin
     assume v,
-    simp only [map_domain_comp.symm, (∘), equiv.apply_inverse_apply],
+    simp only [map_domain_comp.symm, (∘), equiv.apply_symm_apply],
     exact map_domain_id
   end⟩
 
diff --git a/src/data/multivariate_polynomial.lean b/src/data/multivariate_polynomial.lean
index 17ddb63618baf..864f5aff87047 100644
--- a/src/data/multivariate_polynomial.lean
+++ b/src/data/multivariate_polynomial.lean
@@ -622,8 +622,8 @@ def punit_ring_equiv : mv_polynomial punit α ≃r polynomial α :=
 def ring_equiv_of_equiv (e : β ≃ γ) : mv_polynomial β α ≃r mv_polynomial γ α :=
 { to_fun    := rename e,
   inv_fun   := rename e.symm,
-  left_inv  := λ p, by simp only [rename_rename, (∘), e.inverse_apply_apply]; exact rename_id p,
-  right_inv := λ p, by simp only [rename_rename, (∘), e.apply_inverse_apply]; exact rename_id p,
+  left_inv  := λ p, by simp only [rename_rename, (∘), e.symm_apply_apply]; exact rename_id p,
+  right_inv := λ p, by simp only [rename_rename, (∘), e.apply_symm_apply]; exact rename_id p,
   hom       := rename.is_ring_hom e }
 
 def ring_equiv_congr [comm_ring γ] (e : α ≃r γ) : mv_polynomial β α ≃r mv_polynomial β γ :=
@@ -631,11 +631,11 @@ def ring_equiv_congr [comm_ring γ] (e : α ≃r γ) : mv_polynomial β α ≃r
   inv_fun   := map e.symm.to_fun,
   left_inv  := assume p,
     have (e.symm.to_equiv.to_fun ∘ e.to_equiv.to_fun) = id,
-    { ext a, exact e.to_equiv.inverse_apply_apply a },
+    { ext a, exact e.to_equiv.symm_apply_apply a },
     by simp only [map_map, this, map_id],
   right_inv := assume p,
     have (e.to_equiv.to_fun ∘ e.symm.to_equiv.to_fun) = id,
-    { ext a, exact e.to_equiv.apply_inverse_apply a },
+    { ext a, exact e.to_equiv.apply_symm_apply a },
     by simp only [map_map, this, map_id],
   hom       := map.is_ring_hom e.to_fun }
 
diff --git a/src/order/order_iso.lean b/src/order/order_iso.lean
index 02544e436e616..c18d1ca3b61b2 100644
--- a/src/order/order_iso.lean
+++ b/src/order/order_iso.lean
@@ -224,10 +224,10 @@ rfl
 @[simp] theorem trans_apply : ∀ (f : r ≃o s) (g : s ≃o t) (a : α), (f.trans g) a = g (f a)
 | ⟨f₁, o₁⟩ ⟨f₂, o₂⟩ a := equiv.trans_apply _ _ _
 
-@[simp] theorem apply_inverse_apply : ∀ (e : r ≃o s) (x : β), e (e.symm x) = x
+@[simp] theorem apply_symm_apply : ∀ (e : r ≃o s) (x : β), e (e.symm x) = x
 | ⟨f₁, o₁⟩ x := by simp
 
-@[simp] theorem inverse_apply_apply : ∀ (e : r ≃o s) (x : α), e.symm (e x) = x
+@[simp] theorem symm_apply_apply : ∀ (e : r ≃o s) (x : α), e.symm (e x) = x
 | ⟨f₁, o₁⟩ x := by simp
 
 /-- Any equivalence lifts to an order isomorphism between `s` and its preimage. -/
diff --git a/src/ring_theory/localization.lean b/src/ring_theory/localization.lean
index b3ef40a689e02..5d3282c99a94e 100644
--- a/src/ring_theory/localization.lean
+++ b/src/ring_theory/localization.lean
@@ -347,7 +347,7 @@ def equiv_of_equiv (h₁ : α ≃r β) (h₂ : h₁.to_equiv '' S = T) :
     rw ← h₂ at ht,
     rcases ht with ⟨s,hs⟩,
     rw ← hs.2,
-    erw h₁.to_equiv.inverse_apply_apply,
+    erw h₁.to_equiv.symm_apply_apply,
     exact hs.1,
   end,
   left_inv :=
@@ -357,7 +357,7 @@ def equiv_of_equiv (h₁ : α ≃r β) (h₂ : h₁.to_equiv '' S = T) :
     refine @localization.funext _ _ _ _ _ _ (map _ _ ∘ map _ _) id (is_ring_hom.comp _ _) _ _,
     intro a,
     simp only [function.comp, id.def, localization.map_coe],
-    erw h₁.to_equiv.inverse_apply_apply a,
+    erw h₁.to_equiv.symm_apply_apply a,
   end,
   right_inv :=
   begin
diff --git a/src/set_theory/ordinal.lean b/src/set_theory/ordinal.lean
index a4b6f5a7e2292..6298aa2071b4a 100644
--- a/src/set_theory/ordinal.lean
+++ b/src/set_theory/ordinal.lean
@@ -42,7 +42,7 @@ theorem init_iff (f : r ≼i s) {a : α} {b : β} : s b (f a) ↔ ∃ a', f a' =
 
 /-- An order isomorphism is an initial segment -/
 def of_iso (f : r ≃o s) : r ≼i s :=
-⟨f, λ a b h, ⟨f.symm b, order_iso.apply_inverse_apply f _⟩⟩
+⟨f, λ a b h, ⟨f.symm b, order_iso.apply_symm_apply f _⟩⟩
 
 @[refl] protected def refl (r : α → α → Prop) : r ≼i r :=
 ⟨order_embedding.refl _, λ a b h, ⟨_, rfl⟩⟩
@@ -181,7 +181,7 @@ lt_le_apply _ _ _
 def equiv_lt [is_trans β s] [is_trans γ t] (f : r ≃o s) (g : s ≺i t) : r ≺i t :=
 ⟨@order_embedding.trans _ _ _ r s t f g, g.top, λ c,
  by simp only [g.down', coe_fn_coe_base, order_embedding.trans_apply]; exact
- ⟨λ ⟨b, h⟩, ⟨f.symm b, by simp only [h, order_iso.apply_inverse_apply, order_iso.coe_coe_fn]⟩, λ ⟨a, h⟩, ⟨f a, h⟩⟩⟩
+ ⟨λ ⟨b, h⟩, ⟨f.symm b, by simp only [h, order_iso.apply_symm_apply, order_iso.coe_coe_fn]⟩, λ ⟨a, h⟩, ⟨f a, h⟩⟩⟩
 
 @[simp] theorem equiv_lt_apply [is_trans β s] [is_trans γ t] (f : r ≃o s) (g : s ≺i t) (a : α) : (equiv_lt f g) a = g (f a) :=
 order_embedding.trans_apply _ _ _
@@ -2767,10 +2767,10 @@ aleph'.order_iso.ord'.symm
 le_iff_le_iff_lt_iff_lt.2 aleph'_lt
 
 @[simp] theorem aleph'_aleph_idx (c : cardinal.{u}) : aleph' c.aleph_idx = c :=
-cardinal.aleph_idx.order_iso.to_equiv.inverse_apply_apply c
+cardinal.aleph_idx.order_iso.to_equiv.symm_apply_apply c
 
 @[simp] theorem aleph_idx_aleph' (o : ordinal.{u}) : (aleph' o).aleph_idx = o :=
-cardinal.aleph_idx.order_iso.to_equiv.apply_inverse_apply o
+cardinal.aleph_idx.order_iso.to_equiv.apply_symm_apply o
 
 @[simp] theorem aleph'_zero : aleph' 0 = 0 :=
 by rw [← le_zero, ← aleph'_aleph_idx 0, aleph'_le];