chore(*): update injective lemma names to match the naming guide (#…

…6740)

In `src/algebra/group_ring_action.lean`:
- `injective_to_semiring_hom` -> `to_semiring_hom_injective`

In `src/algebra/module/linear_map.lean`:
- `linear_equiv.injective_to_equiv` -> `linear_equiv.to_equiv_injective`
- `linear_equiv.injective_to_linear_map` -> `linear_equiv.to_linear_map_injective`

In `src/analysis/normed_space/enorm.lean`:
- `enorm.injective_coe_fn` -> `enorm.coe_fn_injective`

In `src/data/equiv/basic.lean`:
- `equiv.injective_coe_fn` -> `equiv.coe_fn_injective`

In `src/data/real/nnreal.lean`:
- `nnreal.injective_coe` -> `nnreal.coe_injective`

In `src/data/sum.lean`:
- `sum.injective_inl` -> `sum.inl_injective`
- `sum.injective_inr` -> `sum.inr_injective`

In `src/linear_algebra/affine_space/affine_equiv.lean`:
- `affine_equiv.injective_to_affine_map` -> `affine_equiv.to_affine_map_injective`
- `affine_equiv.injective_coe_fn` -> `affine_equiv.coe_fn_injective`
- `affine_equiv.injective_to_equiv` -> `affine_equiv.to_equiv_injective`

In `src/linear_algebra/affine_space/affine_map.lean`:
- `affine_map.injective_coe_fn` -> `affine_map.coe_fn_injective`

In `src/measure_theory/outer_measure.lean`:
- `measure_theory.outer_measure.injective_coe_fn` -> `measure_theory.outer_measure.coe_fn_injective`

In `src/order/rel_iso.lean`:
- `rel_iso.injective_to_equiv` -> `rel_iso.to_equiv_injective`
- `rel_iso.injective_coe_fn` -> `rel_iso.coe_fn_injective`

In `src/topology/algebra/module.lean`:
- `continuous_linear_map.injective_coe_fn` -> `continuous_linear_map.coe_fn_injective`

src/algebra/group_ring_action.lean

@@ -83,7 +83,7 @@ def mul_semiring_action.to_semiring_hom [mul_semiring_action M R] (x : M) : R 
   map_mul' := smul_mul' x,
   .. distrib_mul_action.to_add_monoid_hom M R x }
 
-theorem injective_to_semiring_hom [faithful_mul_semiring_action M R] :
+theorem to_semiring_hom_injective [faithful_mul_semiring_action M R] :
   function.injective (mul_semiring_action.to_semiring_hom M R) :=
 λ m₁ m₂ h, eq_of_smul_eq_smul R $ λ r, ring_hom.ext_iff.1 h r
 

src/algebra/module/linear_map.lean

@@ -369,18 +369,18 @@ rfl
 @[nolint doc_blame]
 def to_equiv : (M ≃ₗ[R] M₂) → M ≃ M₂ := λ f, f.to_add_equiv.to_equiv
 
-lemma injective_to_equiv : function.injective (to_equiv : (M ≃ₗ[R] M₂) → M ≃ M₂) :=
+lemma to_equiv_injective : function.injective (to_equiv : (M ≃ₗ[R] M₂) → M ≃ M₂) :=
 λ ⟨_, _, _, _, _, _⟩ ⟨_, _, _, _, _, _⟩ h, linear_equiv.mk.inj_eq.mpr (equiv.mk.inj h)
 
 @[simp] lemma to_equiv_inj {e₁ e₂ : M ≃ₗ[R] M₂} : e₁.to_equiv = e₂.to_equiv ↔ e₁ = e₂ :=
-injective_to_equiv.eq_iff
+to_equiv_injective.eq_iff
 
-lemma injective_to_linear_map : function.injective (coe : (M ≃ₗ[R] M₂) → (M →ₗ[R] M₂)) :=
-λ e₁ e₂ H, injective_to_equiv $ equiv.ext $ linear_map.congr_fun H
+lemma to_linear_map_injective : function.injective (coe : (M ≃ₗ[R] M₂) → (M →ₗ[R] M₂)) :=
+λ e₁ e₂ H, to_equiv_injective $ equiv.ext $ linear_map.congr_fun H
 
 @[simp, norm_cast] lemma to_linear_map_inj {e₁ e₂ : M ≃ₗ[R] M₂} :
   (e₁ : M →ₗ[R] M₂) = e₂ ↔ e₁ = e₂ :=
-injective_to_linear_map.eq_iff
+to_linear_map_injective.eq_iff
 
 end
 
@@ -401,7 +401,7 @@ lemma to_linear_map_eq_coe : e.to_linear_map = ↑e := rfl
 section
 variables {e e'}
 @[ext] lemma ext (h : ∀ x, e x = e' x) : e = e' :=
-injective_to_equiv (equiv.ext h)
+to_equiv_injective (equiv.ext h)
 
 protected lemma congr_arg : Π {x x' : M}, x = x' → e x = e x'
 | _ _ rfl := rfl
@@ -457,8 +457,8 @@ rfl
 @[simp] theorem symm_apply_apply (b : M) : e.symm (e b) = b := e.5 b
 @[simp] lemma symm_trans_apply (c : M₃) : (e₁.trans e₂).symm c = e₁.symm (e₂.symm c) := rfl
 
-@[simp] lemma trans_refl : e.trans (refl R M₂) = e := injective_to_equiv e.to_equiv.trans_refl
-@[simp] lemma refl_trans : (refl R M).trans e = e := injective_to_equiv e.to_equiv.refl_trans
+@[simp] lemma trans_refl : e.trans (refl R M₂) = e := to_equiv_injective e.to_equiv.trans_refl
+@[simp] lemma refl_trans : (refl R M).trans e = e := to_equiv_injective e.to_equiv.refl_trans
 
 lemma symm_apply_eq {x y} : e.symm x = y ↔ x = e y := e.to_equiv.symm_apply_eq
 

src/analysis/normed_space/enorm.lean

@@ -48,17 +48,17 @@ variables {𝕜 : Type*} {V : Type*} [normed_field 𝕜] [add_comm_group V] [vec
 
 instance : has_coe_to_fun (enorm 𝕜 V) := ⟨_, enorm.to_fun⟩
 
-lemma injective_coe_fn : function.injective (λ (e : enorm 𝕜 V) (x : V), e x) :=
+lemma coe_fn_injective : function.injective (λ (e : enorm 𝕜 V) (x : V), e x) :=
 λ e₁ e₂ h, by cases e₁; cases e₂; congr; exact h
 
 @[ext] lemma ext {e₁ e₂ : enorm 𝕜 V} (h : ∀ x, e₁ x = e₂ x) : e₁ = e₂ :=
-injective_coe_fn $ funext h
+coe_fn_injective $ funext h
 
 lemma ext_iff {e₁ e₂ : enorm 𝕜 V} : e₁ = e₂ ↔ ∀ x, e₁ x = e₂ x :=
 ⟨λ h x, h ▸ rfl, ext⟩
 
 @[simp, norm_cast] lemma coe_inj {e₁ e₂ : enorm 𝕜 V} : ⇑e₁ = e₂ ↔ e₁ = e₂ :=
-injective_coe_fn.eq_iff
+coe_fn_injective.eq_iff
 
 @[simp] lemma map_smul (c : 𝕜) (x : V) : e (c • x) = nnnorm c * e x :=
 le_antisymm (e.map_smul_le' c x) $

src/analysis/normed_space/operator_norm.lean

@@ -591,7 +591,7 @@ have eq : _ := uniformly_extend_of_ind h_e h_dense f.uniform_continuous,
 }
 
 lemma extend_unique (g : G →L[𝕜] F) (H : g.comp e = f) : extend f e h_dense h_e = g :=
-continuous_linear_map.injective_coe_fn $
+continuous_linear_map.coe_fn_injective $
   uniformly_extend_unique h_e h_dense (continuous_linear_map.ext_iff.1 H) g.continuous
 
 @[simp] lemma extend_zero : extend (0 : E →L[𝕜] F) e h_dense h_e = 0 :=

src/data/equiv/basic.lean

@@ -84,17 +84,17 @@ instance : has_coe_to_fun (α ≃ β) :=
 rfl
 
 /-- The map `coe_fn : (r ≃ s) → (r → s)` is injective. -/
-theorem injective_coe_fn : function.injective (λ (e : α ≃ β) (x : α), e x)
+theorem coe_fn_injective : function.injective (λ (e : α ≃ β) (x : α), e x)
 | ⟨f₁, g₁, l₁, r₁⟩ ⟨f₂, g₂, l₂, r₂⟩ h :=
   have f₁ = f₂, from h,
   have g₁ = g₂, from l₁.eq_right_inverse (this.symm ▸ r₂),
   by simp *
 
 @[simp, norm_cast] protected lemma coe_inj {e₁ e₂ : α ≃ β} : ⇑e₁ = e₂ ↔ e₁ = e₂ :=
-injective_coe_fn.eq_iff
+coe_fn_injective.eq_iff
 
 @[ext] lemma ext {f g : equiv α β} (H : ∀ x, f x = g x) : f = g :=
-injective_coe_fn (funext H)
+coe_fn_injective (funext H)
 
 protected lemma congr_arg {f : equiv α β} : Π {x x' : α}, x = x' → f x = f x'
 | _ _ rfl := rfl

src/data/real/nnreal.lean

@@ -93,9 +93,9 @@ instance : has_le ℝ≥0    := ⟨λ r s, (r:ℝ) ≤ s⟩
 instance : has_bot ℝ≥0   := ⟨0⟩
 instance : inhabited ℝ≥0 := ⟨0⟩
 
-protected lemma injective_coe : function.injective (coe : ℝ≥0 → ℝ) := subtype.coe_injective
+protected lemma coe_injective : function.injective (coe : ℝ≥0 → ℝ) := subtype.coe_injective
 @[simp, norm_cast] protected lemma coe_eq {r₁ r₂ : ℝ≥0} : (r₁ : ℝ) = r₂ ↔ r₁ = r₂ :=
-nnreal.injective_coe.eq_iff
+nnreal.coe_injective.eq_iff
 @[simp, norm_cast] protected lemma coe_zero : ((0 : ℝ≥0) : ℝ) = 0 := rfl
 @[simp, norm_cast] protected lemma coe_one  : ((1 : ℝ≥0) : ℝ) = 1 := rfl
 @[simp, norm_cast] protected lemma coe_add (r₁ r₂ : ℝ≥0) : ((r₁ + r₂ : ℝ≥0) : ℝ) = r₁ + r₂ := rfl
@@ -191,7 +191,7 @@ to_real_hom.to_add_monoid_hom.map_nsmul _ _
 to_real_hom.map_nat_cast n
 
 instance : linear_order ℝ≥0 :=
-linear_order.lift (coe : ℝ≥0 → ℝ) nnreal.injective_coe
+linear_order.lift (coe : ℝ≥0 → ℝ) nnreal.coe_injective
 
 @[simp, norm_cast] protected lemma coe_le_coe {r₁ r₂ : ℝ≥0} : (r₁ : ℝ) ≤ r₂ ↔ r₁ ≤ r₂ := iff.rfl
 @[simp, norm_cast] protected lemma coe_lt_coe {r₁ r₂ : ℝ≥0} : (r₁ : ℝ) < r₂ ↔ r₁ < r₂ := iff.rfl

src/data/sum.lean

@@ -49,10 +49,10 @@ end⟩
 
 namespace sum
 
-lemma injective_inl : function.injective (sum.inl : α → α ⊕ β) :=
+lemma inl_injective : function.injective (sum.inl : α → α ⊕ β) :=
 λ x y, sum.inl.inj
 
-lemma injective_inr : function.injective (sum.inr : β → α ⊕ β) :=
+lemma inr_injective : function.injective (sum.inr : β → α ⊕ β) :=
 λ x y, sum.inr.inj
 
 /-- Map `α ⊕ β` to `α' ⊕ β'` sending `α` to `α'` and `β` to `β'`. -/
@@ -127,7 +127,7 @@ update_eq_iff.2 ⟨by simp, by simp { contextual := tt }⟩
 @[simp] lemma update_inl_comp_inl {α β γ} [decidable_eq α] [decidable_eq (α ⊕ β)]
   {f : α ⊕ β → γ} {i : α} {x : γ} :
   update f (inl i) x ∘ inl = update (f ∘ inl) i x :=
-update_comp_eq_of_injective _ injective_inl _ _
+update_comp_eq_of_injective _ inl_injective _ _
 
 @[simp] lemma update_inl_apply_inl {α β γ} [decidable_eq α] [decidable_eq (α ⊕ β)]
   {f : α ⊕ β → γ} {i j : α} {x : γ} :
@@ -157,7 +157,7 @@ function.update_noteq inl_ne_inr _ _
 @[simp] lemma update_inr_comp_inr {α β γ} [decidable_eq β] [decidable_eq (α ⊕ β)]
   {f : α ⊕ β → γ} {i : β} {x : γ} :
   update f (inr i) x ∘ inr = update (f ∘ inr) i x :=
-update_comp_eq_of_injective _ injective_inr _ _
+update_comp_eq_of_injective _ inr_injective _ _
 
 @[simp] lemma update_inr_apply_inr {α β γ} [decidable_eq β] [decidable_eq (α ⊕ β)]
   {f : α ⊕ β → γ} {i j : β} {x : γ} :

src/field_theory/fixed.lean

@@ -252,7 +252,7 @@ def to_alg_hom (G : Type u) (F : Type v) [group G] [field F]
   [faithful_mul_semiring_action G F] : G ↪ (F →ₐ[fixed_points G F] F) :=
 { to_fun := λ g, { commutes' := λ x, x.2 g,
     .. mul_semiring_action.to_semiring_hom G F g },
-  inj' := λ g₁ g₂ hg, injective_to_semiring_hom G F $ ring_hom.ext $ λ x, alg_hom.ext_iff.1 hg x, }
+  inj' := λ g₁ g₂ hg, to_semiring_hom_injective G F $ ring_hom.ext $ λ x, alg_hom.ext_iff.1 hg x, }
 
 lemma to_alg_hom_apply_apply {G : Type u} {F : Type v} [group G] [field F]
   [faithful_mul_semiring_action G F] (g : G) (x : F) :

src/geometry/manifold/diffeomorph.lean

@@ -116,7 +116,7 @@ to_equiv_injective.eq_iff
 
 /-- Coercion to function `λ h : M ≃ₘ^n⟮I, I'⟯ M', (h : M → M')` is injective. -/
 lemma coe_fn_injective : injective (λ (h : M ≃ₘ^n⟮I, I'⟯ M') (x : M), h x) :=
-equiv.injective_coe_fn.comp to_equiv_injective
+equiv.coe_fn_injective.comp to_equiv_injective
 
 @[ext] lemma ext {h h' : M ≃ₘ^n⟮I, I'⟯ M'} (Heq : ∀ x, h x = h' x) : h = h' :=
 coe_fn_injective $ funext Heq

src/group_theory/perm/sign.lean

@@ -122,8 +122,8 @@ begin
     rw ← hb, exact ⟨b, rfl⟩ },
   let σ₁' := subtype_perm_of_fintype σ h1,
   let σ₂' := subtype_perm_of_fintype σ h3,
-  let σ₁ := perm_congr (equiv.set.range (@sum.inl m n) sum.injective_inl).symm σ₁',
-  let σ₂ := perm_congr (equiv.set.range (@sum.inr m n) sum.injective_inr).symm σ₂',
+  let σ₁ := perm_congr (equiv.set.range (@sum.inl m n) sum.inl_injective).symm σ₁',
+  let σ₂ := perm_congr (equiv.set.range (@sum.inr m n) sum.inr_injective).symm σ₂',
   rw [monoid_hom.mem_range, prod.exists],
   use [σ₁, σ₂],
   rw [perm.sum_congr_hom_apply],
@@ -740,11 +740,11 @@ begin
   { apply σa.swap_induction_on _ (λ σa' a₁ a₂ ha ih, _),
     { simp },
     { rw [←one_mul (1 : perm β), ←sum_congr_mul, sign_mul, sign_mul, ih, sum_congr_swap_one,
-          sign_swap ha, sign_swap (sum.injective_inl.ne_iff.mpr ha)], }, },
+          sign_swap ha, sign_swap (sum.inl_injective.ne_iff.mpr ha)], }, },
   { apply σb.swap_induction_on _ (λ σb' b₁ b₂ hb ih, _),
     { simp },
     { rw [←one_mul (1 : perm α), ←sum_congr_mul, sign_mul, sign_mul, ih, sum_congr_one_swap,
-          sign_swap hb, sign_swap (sum.injective_inr.ne_iff.mpr hb)], }, }
+          sign_swap hb, sign_swap (sum.inr_injective.ne_iff.mpr hb)], }, }
 end
 
 @[simp] lemma sign_subtype_congr {p : α → Prop} [decidable_pred p]

src/linear_algebra/affine_space/affine_equiv.lean

@@ -112,7 +112,7 @@ rfl
 
 @[simp] lemma linear_to_affine_map (e : P₁ ≃ᵃ[k] P₂) : e.to_affine_map.linear = e.linear := rfl
 
-lemma injective_to_affine_map : injective (to_affine_map : (P₁ ≃ᵃ[k] P₂) → (P₁ →ᵃ[k] P₂)) :=
+lemma to_affine_map_injective : injective (to_affine_map : (P₁ ≃ᵃ[k] P₂) → (P₁ →ᵃ[k] P₂)) :=
 begin
   rintros ⟨e, el, h⟩ ⟨e', el', h'⟩ H,
   simp only [to_affine_map_mk, equiv.coe_inj, linear_equiv.to_linear_map_inj] at H,
@@ -122,22 +122,22 @@ end
 
 @[simp] lemma to_affine_map_inj {e e' : P₁ ≃ᵃ[k] P₂} :
   e.to_affine_map = e'.to_affine_map ↔ e = e' :=
-injective_to_affine_map.eq_iff
+to_affine_map_injective.eq_iff
 
 @[ext] lemma ext {e e' : P₁ ≃ᵃ[k] P₂} (h : ∀ x, e x = e' x) : e = e' :=
-injective_to_affine_map $ affine_map.ext h
+to_affine_map_injective $ affine_map.ext h
 
-lemma injective_coe_fn : injective (λ (e : P₁ ≃ᵃ[k] P₂) (x : P₁), e x) :=
+lemma coe_fn_injective : injective (λ (e : P₁ ≃ᵃ[k] P₂) (x : P₁), e x) :=
 λ e e' H, ext $ congr_fun H
 
 @[simp, norm_cast] lemma coe_fn_inj {e e' : P₁ ≃ᵃ[k] P₂} : ⇑e = e' ↔ e = e' :=
-injective_coe_fn.eq_iff
+coe_fn_injective.eq_iff
 
-lemma injective_to_equiv : injective (to_equiv : (P₁ ≃ᵃ[k] P₂) → (P₁ ≃ P₂)) :=
+lemma to_equiv_injective : injective (to_equiv : (P₁ ≃ᵃ[k] P₂) → (P₁ ≃ P₂)) :=
 λ e e' H, ext $ equiv.ext_iff.1 H
 
 @[simp] lemma to_equiv_inj {e e' : P₁ ≃ᵃ[k] P₂} : e.to_equiv = e'.to_equiv ↔ e = e' :=
-injective_to_equiv.eq_iff
+to_equiv_injective.eq_iff
 
 /-- Construct an affine equivalence by verifying the relation between the map and its linear part at
 one base point. Namely, this function takes an equivalence `e : P₁ ≃ P₂`, a linear equivalece
@@ -294,7 +294,7 @@ def point_reflection (x : P₁) : P₁ ≃ᵃ[k] P₁ := (const_vsub k x).trans
 lemma point_reflection_apply (x y : P₁) : point_reflection k x y = x -ᵥ y +ᵥ x := rfl
 
 @[simp] lemma point_reflection_symm (x : P₁) : (point_reflection k x).symm = point_reflection k x :=
-injective_to_equiv $ equiv.point_reflection_symm x
+to_equiv_injective $ equiv.point_reflection_symm x
 
 @[simp] lemma to_equiv_point_reflection (x : P₁) :
   (point_reflection k x).to_equiv = equiv.point_reflection x :=

src/linear_algebra/affine_space/affine_map.lean

@@ -125,7 +125,7 @@ end
 
 lemma ext_iff {f g : P1 →ᵃ[k] P2} : f = g ↔ ∀ p, f p = g p := ⟨λ h p, h ▸ rfl, ext⟩
 
-lemma injective_coe_fn : function.injective (λ (f : P1 →ᵃ[k] P2) (x : P1), f x) :=
+lemma coe_fn_injective : function.injective (λ (f : P1 →ᵃ[k] P2) (x : P1), f x) :=
 λ f g H, ext $ congr_fun H
 
 protected lemma congr_arg (f : P1 →ᵃ[k] P2) {x y : P1} (h : x = y) : f x = f y :=

src/linear_algebra/basis.lean

@@ -274,7 +274,7 @@ def linear_equiv_of_is_basis' {v : ι → M} {v' : ι' → M'} (f : M → M') (g
   (linear_equiv_of_is_basis hv hv' e).trans (linear_equiv_of_is_basis hv' hv'' f) =
   linear_equiv_of_is_basis hv hv'' (e.trans f) :=
 begin
-  apply linear_equiv.injective_to_linear_map,
+  apply linear_equiv.to_linear_map_injective,
   apply hv.ext,
   intros i,
   simp [linear_equiv_of_is_basis]
@@ -283,7 +283,7 @@ end
 @[simp] lemma linear_equiv_of_is_basis_refl :
   linear_equiv_of_is_basis hv hv (equiv.refl ι) = linear_equiv.refl R M :=
 begin
-  apply linear_equiv.injective_to_linear_map,
+  apply linear_equiv.to_linear_map_injective,
   apply hv.ext,
   intros i,
   simp [linear_equiv_of_is_basis]

src/linear_algebra/determinant.lean

@@ -146,7 +146,7 @@ calc det (M ⬝ N) = ∑ p : n → n, ∑ σ : perm n, ε σ * ∏ i, (M (σ i)
 ... = ∑ τ : perm n, ∑ σ : perm n, ε σ * ∏ i, (M (σ i) (τ i) * N (τ i) i) :
   sum_bij (λ p h, equiv.of_bijective p (mem_filter.1 h).2) (λ _ _, mem_univ _)
     (λ _ _, rfl) (λ _ _ _ _ h, by injection h)
-    (λ b _, ⟨b, mem_filter.2 ⟨mem_univ _, b.bijective⟩, injective_coe_fn rfl⟩)
+    (λ b _, ⟨b, mem_filter.2 ⟨mem_univ _, b.bijective⟩, coe_fn_injective rfl⟩)
 ... = ∑ σ : perm n, ∑ τ : perm n, (∏ i, N (σ i) i) * ε τ * (∏ j, M (τ j) (σ j)) :
   by simp [mul_sum, det_apply', mul_comm, mul_left_comm, prod_mul_distrib, mul_assoc]
 ... = ∑ σ : perm n, ∑ τ : perm n, (((∏ i, N (σ i) i) * (ε σ * ε τ)) * ∏ i, M (τ i) i) :

src/linear_algebra/linear_independent.lean

@@ -423,13 +423,13 @@ lemma linear_independent_sum {v : ι ⊕ ι' → M} :
       disjoint (submodule.span R (range (v ∘ sum.inl))) (submodule.span R (range (v ∘ sum.inr))) :=
 begin
   rw [range_comp v, range_comp v],
-  refine ⟨λ h, ⟨h.comp _ sum.injective_inl, h.comp _ sum.injective_inr,
+  refine ⟨λ h, ⟨h.comp _ sum.inl_injective, h.comp _ sum.inr_injective,
     h.disjoint_span_image is_compl_range_inl_range_inr.1⟩, _⟩,
   rintro ⟨hl, hr, hlr⟩,
   rw [linear_independent_iff'] at *,
   intros s g hg i hi,
-  have : ∑ i in s.preimage sum.inl (sum.injective_inl.inj_on _), (λ x, g x • v x) (sum.inl i) +
-    ∑ i in s.preimage sum.inr (sum.injective_inr.inj_on _), (λ x, g x • v x) (sum.inr i) = 0,
+  have : ∑ i in s.preimage sum.inl (sum.inl_injective.inj_on _), (λ x, g x • v x) (sum.inl i) +
+    ∑ i in s.preimage sum.inr (sum.inr_injective.inj_on _), (λ x, g x • v x) (sum.inr i) = 0,
   { rw [finset.sum_preimage', finset.sum_preimage', ← finset.sum_union, ← finset.filter_or],
     { simpa only [← mem_union, range_inl_union_range_inr, mem_univ, finset.filter_true] },
     { exact finset.disjoint_filter.2 (λ x hx, disjoint_left.1 is_compl_range_inl_range_inr.1) } },

src/linear_algebra/pi_tensor_product.lean

@@ -408,7 +408,7 @@ linear_map.congr_fun (lift_comp_reindex e φ) x
 @[simp] lemma reindex_trans (e : ι ≃ ι₂) (e' : ι₂ ≃ ι₃) :
   (reindex R M e).trans (reindex R M e') = reindex R M (e.trans e') :=
 begin
-  apply linear_equiv.injective_to_linear_map,
+  apply linear_equiv.to_linear_map_injective,
   ext f,
   simp only [linear_equiv.trans_apply, linear_equiv.coe_coe, reindex_tprod,
     linear_map.coe_comp_multilinear_map, function.comp_app, multilinear_map.dom_dom_congr_apply,
@@ -421,7 +421,7 @@ end
 
 @[simp] lemma reindex_refl : reindex R M (equiv.refl ι) = linear_equiv.refl R _ :=
 begin
-  apply linear_equiv.injective_to_linear_map,
+  apply linear_equiv.to_linear_map_injective,
   ext1,
   rw [reindex_comp_tprod, linear_equiv.refl_to_linear_map, equiv.refl_symm],
   refl,

src/measure_theory/outer_measure.lean

@@ -155,11 +155,11 @@ lemma union_null (m : outer_measure α) {s₁ s₂ : set α}
   (h₁ : m s₁ = 0) (h₂ : m s₂ = 0) : m (s₁ ∪ s₂) = 0 :=
 by simpa [h₁, h₂] using m.union s₁ s₂
 
-lemma injective_coe_fn : injective (λ (μ : outer_measure α) (s : set α), μ s) :=
+lemma coe_fn_injective : injective (λ (μ : outer_measure α) (s : set α), μ s) :=
 λ μ₁ μ₂ h, by { cases μ₁, cases μ₂, congr, exact h }
 
 @[ext] lemma ext {μ₁ μ₂ : outer_measure α} (h : ∀ s, μ₁ s = μ₂ s) : μ₁ = μ₂ :=
-injective_coe_fn $ funext h
+coe_fn_injective $ funext h
 
 /-- A version of `measure_theory.outer_measure.ext` that assumes `μ₁ s = μ₂ s` on all *nonempty*
 sets `s`, and gets `μ₁ ∅ = μ₂ ∅` from `measure_theory.outer_measure.empty'`. -/
@@ -196,7 +196,7 @@ instance add_comm_monoid : add_comm_monoid (outer_measure α) :=
 { zero      := 0,
   add       := (+),
   .. injective.add_comm_monoid (show outer_measure α → set α → ℝ≥0∞, from coe_fn)
-    injective_coe_fn rfl (λ _ _, rfl) }
+    coe_fn_injective rfl (λ _ _, rfl) }
 
 instance : has_scalar ℝ≥0∞ (outer_measure α) :=
 ⟨λ c m,
@@ -212,7 +212,7 @@ lemma smul_apply (c : ℝ≥0∞) (m : outer_measure α) (s : set α) : (c • m
 instance : semimodule ℝ≥0∞ (outer_measure α) :=
 { smul := (•),
   .. injective.semimodule ℝ≥0∞ ⟨show outer_measure α → set α → ℝ≥0∞, from coe_fn, coe_zero,
-    coe_add⟩ injective_coe_fn coe_smul }
+    coe_add⟩ coe_fn_injective coe_smul }
 
 instance : has_bot (outer_measure α) := ⟨0⟩
 
@@ -274,8 +274,8 @@ def map {β} (f : α → β) : outer_measure α →ₗ[ℝ≥0∞] outer_measure
       mono := λ s t h, m.mono (preimage_mono h),
       Union_nat := λ s, by rw [preimage_Union]; exact
         m.Union_nat (λ i, f ⁻¹' s i) },
-  map_add' := λ m₁ m₂, injective_coe_fn rfl,
-  map_smul' := λ c m, injective_coe_fn rfl }
+  map_add' := λ m₁ m₂, coe_fn_injective rfl,
+  map_smul' := λ c m, coe_fn_injective rfl }
 
 @[simp] theorem map_apply {β} (f : α → β)
   (m : outer_measure α) (s : set β) : map f m s = m (f ⁻¹' s) := rfl

src/order/rel_iso.lean

@@ -379,16 +379,16 @@ theorem map_rel_iff (f : r ≃r s) : ∀ {a b}, s (f a) (f b) ↔ r a b := f.map
 
 @[simp] theorem coe_fn_to_equiv (f : r ≃r s) : (f.to_equiv : α → β) = f := rfl
 
-theorem injective_to_equiv : injective (to_equiv : (r ≃r s) → α ≃ β)
+theorem to_equiv_injective : injective (to_equiv : (r ≃r s) → α ≃ β)
 | ⟨e₁, o₁⟩ ⟨e₂, o₂⟩ h := by { congr, exact h }
 
 /-- The map `coe_fn : (r ≃r s) → (α → β)` is injective. Lean fails to parse
 `function.injective (λ e : r ≃r s, (e : α → β))`, so we use a trick to say the same. -/
-theorem injective_coe_fn : function.injective (λ (e : r ≃r s) (x : α), e x) :=
-equiv.injective_coe_fn.comp injective_to_equiv
+theorem coe_fn_injective : function.injective (λ (e : r ≃r s) (x : α), e x) :=
+equiv.coe_fn_injective.comp to_equiv_injective
 
 @[ext] theorem ext ⦃f g : r ≃r s⦄ (h : ∀ x, f x = g x) : f = g :=
-injective_coe_fn (funext h)
+coe_fn_injective (funext h)
 
 theorem ext_iff {f g : r ≃r s} : f = g ↔ ∀ x, f x = g x :=
 ⟨λ h x, h ▸ rfl, λ h, ext h⟩

src/set_theory/ordinal.lean

@@ -154,7 +154,7 @@ by haveI := f.to_rel_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 :=
-rel_iso.injective_coe_fn rfl
+rel_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 :=