refactor: rename Submodule.ofLe to Submodule.inclusion (#8470)

This matches `Set.inclusion`, `Subring.inclusion`, `Subalgebra.inclusion`, etc.

Also renames the `homOfLe` spellings in `Algebra/Lie` to match.

Note that we leave `LieSubalgebra.ofLe`, as this is a completely different statement!

As requested by @alreadydone.

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

@@ -792,7 +792,7 @@ theorem range_val : NonUnitalAlgHom.range (NonUnitalSubalgebraClass.subtype S) =
 
 /-- The map `S → T` when `S` is a non-unital subalgebra contained in the non-unital subalgebra `T`.
 
-This is the non-unital subalgebra version of `Submodule.ofLe`, or `Subring.inclusion`  -/
+This is the non-unital subalgebra version of `Submodule.inclusion`, or `Subring.inclusion`  -/
 def inclusion {S T : NonUnitalSubalgebra R A} (h : S ≤ T) : S →ₙₐ[R] T
     where
   toFun := Set.inclusion h

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -1031,7 +1031,7 @@ instance : Unique (Subalgebra R R) :=
 
 /-- The map `S → T` when `S` is a subalgebra contained in the subalgebra `T`.
 
-This is the subalgebra version of `Submodule.ofLe`, or `Subring.inclusion`  -/
+This is the subalgebra version of `Submodule.inclusion`, or `Subring.inclusion`  -/
 def inclusion {S T : Subalgebra R A} (h : S ≤ T) : S →ₐ[R] T
     where
   toFun := Set.inclusion h

Mathlib/Algebra/Category/ModuleCat/Subobject.lean

@@ -67,7 +67,7 @@ noncomputable def subobjectModule : Subobject M ≃o Submodule R M :=
           rw [this, comp_def, LinearEquiv.range_comp]
         · exact (Submodule.range_subtype _).symm
       map_rel_iff' := fun {S T} => by
-        refine' ⟨fun h => _, fun h => mk_le_mk_of_comm (↟(Submodule.ofLe h)) rfl⟩
+        refine' ⟨fun h => _, fun h => mk_le_mk_of_comm (↟(Submodule.inclusion h)) rfl⟩
         convert LinearMap.range_comp_le_range (ofMkLEMk _ _ h) (↾T.subtype)
         · simpa only [← comp_def, ofMkLEMk_comp] using (Submodule.range_subtype _).symm
         · exact (Submodule.range_subtype _).symm }

Mathlib/Algebra/Lie/Semisimple.lean

@@ -111,7 +111,7 @@ theorem abelian_radical_iff_solvable_is_abelian [IsNoetherian R L] :
   constructor
   · rintro h₁ I h₂
     rw [LieIdeal.solvable_iff_le_radical] at h₂
-    exact (LieIdeal.homOfLe_injective h₂).isLieAbelian h₁
+    exact (LieIdeal.inclusion_injective h₂).isLieAbelian h₁
   · intro h; apply h; infer_instance
 #align lie_algebra.abelian_radical_iff_solvable_is_abelian LieAlgebra.abelian_radical_iff_solvable_is_abelian
 

Mathlib/Algebra/Lie/Solvable.lean

@@ -254,7 +254,7 @@ theorem solvable_iff_equiv_solvable (e : L' ≃ₗ⁅R⁆ L) : IsSolvable R L' 
 
 theorem le_solvable_ideal_solvable {I J : LieIdeal R L} (h₁ : I ≤ J) (_ : IsSolvable R J) :
     IsSolvable R I :=
-  (LieIdeal.homOfLe_injective h₁).lieAlgebra_isSolvable
+  (LieIdeal.inclusion_injective h₁).lieAlgebra_isSolvable
 #align lie_algebra.le_solvable_ideal_solvable LieAlgebra.le_solvable_ideal_solvable
 
 variable (R L)

Mathlib/Algebra/Lie/Subalgebra.lean

@@ -594,32 +594,32 @@ variable (h : K ≤ K')
 
 /-- Given two nested Lie subalgebras `K ⊆ K'`, the inclusion `K ↪ K'` is a morphism of Lie
 algebras. -/
-def homOfLe : K →ₗ⁅R⁆ K' :=
-  { Submodule.ofLe h with map_lie' := @fun _ _ ↦ rfl }
-#align lie_subalgebra.hom_of_le LieSubalgebra.homOfLe
+def inclusion : K →ₗ⁅R⁆ K' :=
+  { Submodule.inclusion h with map_lie' := @fun _ _ ↦ rfl }
+#align lie_subalgebra.hom_of_le LieSubalgebra.inclusion
 
 @[simp]
-theorem coe_homOfLe (x : K) : (homOfLe h x : L) = x :=
+theorem coe_inclusion (x : K) : (inclusion h x : L) = x :=
   rfl
-#align lie_subalgebra.coe_hom_of_le LieSubalgebra.coe_homOfLe
+#align lie_subalgebra.coe_hom_of_le LieSubalgebra.coe_inclusion
 
-theorem homOfLe_apply (x : K) : homOfLe h x = ⟨x.1, h x.2⟩ :=
+theorem inclusion_apply (x : K) : inclusion h x = ⟨x.1, h x.2⟩ :=
   rfl
-#align lie_subalgebra.hom_of_le_apply LieSubalgebra.homOfLe_apply
+#align lie_subalgebra.hom_of_le_apply LieSubalgebra.inclusion_apply
 
-theorem homOfLe_injective : Function.Injective (homOfLe h) := fun x y ↦ by
-  simp only [homOfLe_apply, imp_self, Subtype.mk_eq_mk, SetLike.coe_eq_coe]
-#align lie_subalgebra.hom_of_le_injective LieSubalgebra.homOfLe_injective
+theorem inclusion_injective : Function.Injective (inclusion h) := fun x y ↦ by
+  simp only [inclusion_apply, imp_self, Subtype.mk_eq_mk, SetLike.coe_eq_coe]
+#align lie_subalgebra.hom_of_le_injective LieSubalgebra.inclusion_injective
 
 /-- Given two nested Lie subalgebras `K ⊆ K'`, we can view `K` as a Lie subalgebra of `K'`,
 regarded as Lie algebra in its own right. -/
 def ofLe : LieSubalgebra R K' :=
-  (homOfLe h).range
+  (inclusion h).range
 #align lie_subalgebra.of_le LieSubalgebra.ofLe
 
 @[simp]
 theorem mem_ofLe (x : K') : x ∈ ofLe h ↔ (x : L) ∈ K := by
-  simp only [ofLe, homOfLe_apply, LieHom.mem_range]
+  simp only [ofLe, inclusion_apply, LieHom.mem_range]
   constructor
   · rintro ⟨y, rfl⟩
     exact y.property
@@ -634,18 +634,18 @@ theorem ofLe_eq_comap_incl : ofLe h = K.comap K'.incl := by
 #align lie_subalgebra.of_le_eq_comap_incl LieSubalgebra.ofLe_eq_comap_incl
 
 @[simp]
-theorem coe_ofLe : (ofLe h : Submodule R K') = LinearMap.range (Submodule.ofLe h) :=
+theorem coe_ofLe : (ofLe h : Submodule R K') = LinearMap.range (Submodule.inclusion h) :=
   rfl
 #align lie_subalgebra.coe_of_le LieSubalgebra.coe_ofLe
 
 /-- Given nested Lie subalgebras `K ⊆ K'`, there is a natural equivalence from `K` to its image in
 `K'`.  -/
 noncomputable def equivOfLe : K ≃ₗ⁅R⁆ ofLe h :=
-  (homOfLe h).equivRangeOfInjective (homOfLe_injective h)
+  (inclusion h).equivRangeOfInjective (inclusion_injective h)
 #align lie_subalgebra.equiv_of_le LieSubalgebra.equivOfLe
 
 @[simp]
-theorem equivOfLe_apply (x : K) : equivOfLe h x = ⟨homOfLe h x, (homOfLe h).mem_range_self x⟩ :=
+theorem equivOfLe_apply (x : K) : equivOfLe h x = ⟨inclusion h x, (inclusion h).mem_range_self x⟩ :=
   rfl
 #align lie_subalgebra.equiv_of_le_apply LieSubalgebra.equivOfLe_apply
 

Mathlib/Algebra/Lie/Submodule.lean

@@ -658,22 +658,23 @@ theorem injective_incl : Function.Injective N.incl := Subtype.coe_injective
 variable {N N'} (h : N ≤ N')
 
 /-- Given two nested Lie submodules `N ⊆ N'`, the inclusion `N ↪ N'` is a morphism of Lie modules.-/
-def homOfLe : N →ₗ⁅R,L⁆ N' :=
-  { Submodule.ofLe (show N.toSubmodule ≤ N'.toSubmodule from h) with map_lie' := fun {_ _} ↦ rfl }
-#align lie_submodule.hom_of_le LieSubmodule.homOfLe
+def inclusion : N →ₗ⁅R,L⁆ N' where
+  __ := Submodule.inclusion (show N.toSubmodule ≤ N'.toSubmodule from h)
+  map_lie' := rfl
+#align lie_submodule.hom_of_le LieSubmodule.inclusion
 
 @[simp]
-theorem coe_homOfLe (m : N) : (homOfLe h m : M) = m :=
+theorem coe_inclusion (m : N) : (inclusion h m : M) = m :=
   rfl
-#align lie_submodule.coe_hom_of_le LieSubmodule.coe_homOfLe
+#align lie_submodule.coe_hom_of_le LieSubmodule.coe_inclusion
 
-theorem homOfLe_apply (m : N) : homOfLe h m = ⟨m.1, h m.2⟩ :=
+theorem inclusion_apply (m : N) : inclusion h m = ⟨m.1, h m.2⟩ :=
   rfl
-#align lie_submodule.hom_of_le_apply LieSubmodule.homOfLe_apply
+#align lie_submodule.hom_of_le_apply LieSubmodule.inclusion_apply
 
-theorem homOfLe_injective : Function.Injective (homOfLe h) := fun x y ↦ by
-  simp only [homOfLe_apply, imp_self, Subtype.mk_eq_mk, SetLike.coe_eq_coe]
-#align lie_submodule.hom_of_le_injective LieSubmodule.homOfLe_injective
+theorem inclusion_injective : Function.Injective (inclusion h) := fun x y ↦ by
+  simp only [inclusion_apply, imp_self, Subtype.mk_eq_mk, SetLike.coe_eq_coe]
+#align lie_submodule.hom_of_le_injective LieSubmodule.inclusion_injective
 
 end InclusionMaps
 
@@ -1232,23 +1233,26 @@ theorem bot_of_map_eq_bot {I : LieIdeal R L} (h₁ : Function.Injective f) (h₂
 #align lie_ideal.bot_of_map_eq_bot LieIdeal.bot_of_map_eq_bot
 
 /-- Given two nested Lie ideals `I₁ ⊆ I₂`, the inclusion `I₁ ↪ I₂` is a morphism of Lie algebras. -/
-def homOfLe {I₁ I₂ : LieIdeal R L} (h : I₁ ≤ I₂) : I₁ →ₗ⁅R⁆ I₂ :=
-  { Submodule.ofLe (show I₁.toSubmodule ≤ I₂.toSubmodule from h) with map_lie' := fun {_ _} ↦ rfl }
-#align lie_ideal.hom_of_le LieIdeal.homOfLe
+def inclusion {I₁ I₂ : LieIdeal R L} (h : I₁ ≤ I₂) : I₁ →ₗ⁅R⁆ I₂ where
+  __ := Submodule.inclusion (show I₁.toSubmodule ≤ I₂.toSubmodule from h)
+  map_lie' := rfl
+#align lie_ideal.hom_of_le LieIdeal.inclusion
 
 @[simp]
-theorem coe_homOfLe {I₁ I₂ : LieIdeal R L} (h : I₁ ≤ I₂) (x : I₁) : (homOfLe h x : L) = x :=
+theorem coe_inclusion {I₁ I₂ : LieIdeal R L} (h : I₁ ≤ I₂) (x : I₁) : (inclusion h x : L) = x :=
   rfl
-#align lie_ideal.coe_hom_of_le LieIdeal.coe_homOfLe
+#align lie_ideal.coe_hom_of_le LieIdeal.coe_inclusion
 
-theorem homOfLe_apply {I₁ I₂ : LieIdeal R L} (h : I₁ ≤ I₂) (x : I₁) : homOfLe h x = ⟨x.1, h x.2⟩ :=
+theorem inclusion_apply {I₁ I₂ : LieIdeal R L} (h : I₁ ≤ I₂) (x : I₁) :
+    inclusion h x = ⟨x.1, h x.2⟩ :=
   rfl
-#align lie_ideal.hom_of_le_apply LieIdeal.homOfLe_apply
+#align lie_ideal.hom_of_le_apply LieIdeal.inclusion_apply
 
-theorem homOfLe_injective {I₁ I₂ : LieIdeal R L} (h : I₁ ≤ I₂) : Function.Injective (homOfLe h) :=
+theorem inclusion_injective {I₁ I₂ : LieIdeal R L} (h : I₁ ≤ I₂) :
+    Function.Injective (inclusion h) :=
   fun x y ↦ by
-  simp only [homOfLe_apply, imp_self, Subtype.mk_eq_mk, SetLike.coe_eq_coe]
-#align lie_ideal.hom_of_le_injective LieIdeal.homOfLe_injective
+  simp only [inclusion_apply, imp_self, Subtype.mk_eq_mk, SetLike.coe_eq_coe]
+#align lie_ideal.hom_of_le_injective LieIdeal.inclusion_injective
 
 -- Porting note: LHS simplifies, so moved @[simp] to new theorem `map_sup_ker_eq_map'`
 theorem map_sup_ker_eq_map : LieIdeal.map f (I ⊔ f.ker) = LieIdeal.map f I := by

Mathlib/Algebra/Module/Submodule/LinearMap.lean

@@ -22,7 +22,7 @@ In this file we define a number of linear maps involving submodules of a module.
   as a semilinear map `p → M₂`.
 * `LinearMap.restrict`: The restriction of a linear map `f : M → M₁` to a submodule `p ⊆ M` and
   `q ⊆ M₁` (if `q` contains the codomain).
-* `Submodule.ofLe`: the inclusion `p ⊆ p'` of submodules `p` and `p'` as a linear map.
+* `Submodule.inclusion`: the inclusion `p ⊆ p'` of submodules `p` and `p'` as a linear map.
 
 ## Tags
 
@@ -323,32 +323,32 @@ section AddCommMonoid
 
 variable {R : Type*} {M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] {p p' : Submodule R M}
 
-/-- If two submodules `p` and `p'` satisfy `p ⊆ p'`, then `ofLe p p'` is the linear map version of
-this inclusion. -/
-def ofLe (h : p ≤ p') : p →ₗ[R] p' :=
+/-- If two submodules `p` and `p'` satisfy `p ⊆ p'`, then `inclusion p p'` is the linear map version
+of this inclusion. -/
+def inclusion (h : p ≤ p') : p →ₗ[R] p' :=
   p.subtype.codRestrict p' fun ⟨_, hx⟩ => h hx
-#align submodule.of_le Submodule.ofLe
+#align submodule.of_le Submodule.inclusion
 
 @[simp]
-theorem coe_ofLe (h : p ≤ p') (x : p) : (ofLe h x : M) = x :=
+theorem coe_inclusion (h : p ≤ p') (x : p) : (inclusion h x : M) = x :=
   rfl
-#align submodule.coe_of_le Submodule.coe_ofLe
+#align submodule.coe_of_le Submodule.coe_inclusion
 
-theorem ofLe_apply (h : p ≤ p') (x : p) : ofLe h x = ⟨x, h x.2⟩ :=
+theorem inclusion_apply (h : p ≤ p') (x : p) : inclusion h x = ⟨x, h x.2⟩ :=
   rfl
-#align submodule.of_le_apply Submodule.ofLe_apply
+#align submodule.of_le_apply Submodule.inclusion_apply
 
-theorem ofLe_injective (h : p ≤ p') : Function.Injective (ofLe h) := fun _ _ h =>
+theorem inclusion_injective (h : p ≤ p') : Function.Injective (inclusion h) := fun _ _ h =>
   Subtype.val_injective (Subtype.mk.inj h)
-#align submodule.of_le_injective Submodule.ofLe_injective
+#align submodule.of_le_injective Submodule.inclusion_injective
 
 variable (p p')
 
-theorem subtype_comp_ofLe (p q : Submodule R M) (h : p ≤ q) :
-    q.subtype.comp (ofLe h) = p.subtype := by
+theorem subtype_comp_inclusion (p q : Submodule R M) (h : p ≤ q) :
+    q.subtype.comp (inclusion h) = p.subtype := by
   ext ⟨b, hb⟩
   rfl
-#align submodule.subtype_comp_of_le Submodule.subtype_comp_ofLe
+#align submodule.subtype_comp_of_le Submodule.subtype_comp_inclusion
 
 end AddCommMonoid
 

Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

@@ -823,7 +823,7 @@ theorem range_val : NonUnitalStarAlgHom.range (NonUnitalStarSubalgebraClass.subt
 The map `S → T` when `S` is a non-unital star subalgebra contained in the non-unital star
 algebra `T`.
 
-This is the non-unital star subalgebra version of `Submodule.ofLe`, or
+This is the non-unital star subalgebra version of `Submodule.inclusion`, or
 `NonUnitalSubalgebra.inclusion`  -/
 def inclusion {S T : NonUnitalStarSubalgebra R A} (h : S ≤ T) : S →⋆ₙₐ[R] T where
   toNonUnitalAlgHom := NonUnitalSubalgebra.inclusion h

Mathlib/Analysis/Convex/Cone/Extension.lean

@@ -135,7 +135,7 @@ theorem exists_top (p : E →ₗ.[ℝ] ℝ) (hp_nonneg : ∀ x : p.domain, (x :
     contrapose! hq
     have hqd : ∀ y, ∃ x : q.domain, (x : E) + y ∈ s := fun y ↦
       let ⟨x, hx⟩ := hp_dense y
-      ⟨ofLe hpq.left x, hx⟩
+      ⟨Submodule.inclusion hpq.left x, hx⟩
     rcases step s q hqs hqd hq with ⟨r, hqr, hr⟩
     exact ⟨r, hr, hqr.le, hqr.ne'⟩
 #align riesz_extension.exists_top RieszExtension.exists_top

Mathlib/LinearAlgebra/Basic.lean

@@ -640,18 +640,19 @@ theorem comap_subtype_self : comap p.subtype p = ⊤ :=
 #align submodule.comap_subtype_self Submodule.comap_subtype_self
 
 @[simp]
-theorem ker_ofLe (p p' : Submodule R M) (h : p ≤ p') : ker (ofLe h) = ⊥ := by
-  rw [ofLe, ker_codRestrict, ker_subtype]
-#align submodule.ker_of_le Submodule.ker_ofLe
+theorem ker_inclusion (p p' : Submodule R M) (h : p ≤ p') : ker (inclusion h) = ⊥ := by
+  rw [inclusion, ker_codRestrict, ker_subtype]
+#align submodule.ker_of_le Submodule.ker_inclusion
 
-theorem range_ofLe (p q : Submodule R M) (h : p ≤ q) : range (ofLe h) = comap q.subtype p := by
-  rw [← map_top, ofLe, LinearMap.map_codRestrict, map_top, range_subtype]
-#align submodule.range_of_le Submodule.range_ofLe
+theorem range_inclusion (p q : Submodule R M) (h : p ≤ q) :
+    range (inclusion h) = comap q.subtype p := by
+  rw [← map_top, inclusion, LinearMap.map_codRestrict, map_top, range_subtype]
+#align submodule.range_of_le Submodule.range_inclusion
 
 @[simp]
-theorem map_subtype_range_ofLe {p p' : Submodule R M} (h : p ≤ p') :
-    map p'.subtype (range $ ofLe h) = p := by simp [range_ofLe, map_comap_eq, h]
-#align submodule.map_subtype_range_of_le Submodule.map_subtype_range_ofLe
+theorem map_subtype_range_inclusion {p p' : Submodule R M} (h : p ≤ p') :
+    map p'.subtype (range $ inclusion h) = p := by simp [range_inclusion, map_comap_eq, h]
+#align submodule.map_subtype_range_of_le Submodule.map_subtype_range_inclusion
 
 theorem disjoint_iff_comap_eq_bot {p q : Submodule R M} : Disjoint p q ↔ comap p.subtype q = ⊥ := by
   rw [← (map_injective_of_injective (show Injective p.subtype from Subtype.coe_injective)).eq_iff,
@@ -749,11 +750,11 @@ theorem mem_submoduleImage_of_le {M' : Type*} [AddCommMonoid M'] [Module R M'] {
     exact ⟨y, hNO yN, yN, h⟩
 #align linear_map.mem_submodule_image_of_le LinearMap.mem_submoduleImage_of_le
 
-theorem submoduleImage_apply_ofLe {M' : Type*} [AddCommGroup M'] [Module R M'] {O : Submodule R M}
-    (ϕ : O →ₗ[R] M') (N : Submodule R M) (hNO : N ≤ O) :
-    ϕ.submoduleImage N = range (ϕ.comp (Submodule.ofLe hNO)) := by
-  rw [submoduleImage, range_comp, Submodule.range_ofLe]
-#align linear_map.submodule_image_apply_of_le LinearMap.submoduleImage_apply_ofLe
+theorem submoduleImage_apply_of_le {M' : Type*} [AddCommGroup M'] [Module R M']
+    {O : Submodule R M} (ϕ : O →ₗ[R] M') (N : Submodule R M) (hNO : N ≤ O) :
+    ϕ.submoduleImage N = range (ϕ.comp (Submodule.inclusion hNO)) := by
+  rw [submoduleImage, range_comp, Submodule.range_inclusion]
+#align linear_map.submodule_image_apply_of_le LinearMap.submoduleImage_apply_of_le
 
 end Image
 

Mathlib/LinearAlgebra/Basis.lean

@@ -1324,7 +1324,7 @@ theorem coe_mkFinConsOfLE {n : ℕ} {N O : Submodule R M} (y : M) (yO : y ∈ O)
     (hNO : N ≤ O) (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0)
     (hsp : ∀ z ∈ O, ∃ c : R, z + c • y ∈ N) :
     (mkFinConsOfLE y yO b hNO hli hsp : Fin (n + 1) → O) =
-      Fin.cons ⟨y, yO⟩ (Submodule.ofLe hNO ∘ b) :=
+      Fin.cons ⟨y, yO⟩ (Submodule.inclusion hNO ∘ b) :=
   coe_mkFinCons _ _ _ _
 #align basis.coe_mk_fin_cons_of_le Basis.coe_mkFinConsOfLE
 

Mathlib/LinearAlgebra/Dimension.lean

@@ -181,7 +181,7 @@ theorem rank_map_le (f : M →ₗ[R] M₁) (p : Submodule R M) :
 
 theorem rank_le_of_submodule (s t : Submodule R M) (h : s ≤ t) :
     Module.rank R s ≤ Module.rank R t :=
-  (ofLe h).rank_le_of_injective fun ⟨x, _⟩ ⟨y, _⟩ eq =>
+  (Submodule.inclusion h).rank_le_of_injective fun ⟨x, _⟩ ⟨y, _⟩ eq =>
     Subtype.eq <| show x = y from Subtype.ext_iff_val.1 eq
 #align rank_le_of_submodule rank_le_of_submodule
 
@@ -830,7 +830,7 @@ theorem Basis.card_le_card_of_submodule (N : Submodule R M) [Fintype ι] (b : Ba
 theorem Basis.card_le_card_of_le {N O : Submodule R M} (hNO : N ≤ O) [Fintype ι] (b : Basis ι R O)
     [Fintype ι'] (b' : Basis ι' R N) : Fintype.card ι' ≤ Fintype.card ι :=
   b.card_le_card_of_linearIndependent
-    (b'.linearIndependent.map' (Submodule.ofLe hNO) (N.ker_ofLe O _))
+    (b'.linearIndependent.map' (Submodule.inclusion hNO) (N.ker_inclusion O _))
 #align basis.card_le_card_of_le Basis.card_le_card_of_le
 
 theorem Basis.mk_eq_rank (v : Basis ι R M) :
@@ -1198,12 +1198,14 @@ theorem rank_add_rank_split (db : V₂ →ₗ[K] V) (eb : V₃ →ₗ[K] V) (cd
 theorem Submodule.rank_sup_add_rank_inf_eq (s t : Submodule K V) :
     Module.rank K (s ⊔ t : Submodule K V) + Module.rank K (s ⊓ t : Submodule K V) =
     Module.rank K s + Module.rank K t :=
-  rank_add_rank_split (ofLe le_sup_left) (ofLe le_sup_right) (ofLe inf_le_left) (ofLe inf_le_right)
+  rank_add_rank_split
+    (inclusion le_sup_left) (inclusion le_sup_right)
+    (inclusion inf_le_left) (inclusion inf_le_right)
     (by
       rw [← map_le_map_iff' (ker_subtype <| s ⊔ t), Submodule.map_sup, Submodule.map_top, ←
-        LinearMap.range_comp, ← LinearMap.range_comp, subtype_comp_ofLe, subtype_comp_ofLe,
-        range_subtype, range_subtype, range_subtype])
-    (ker_ofLe _ _ _) (by ext ⟨x, hx⟩; rfl)
+        LinearMap.range_comp, ← LinearMap.range_comp, subtype_comp_inclusion,
+        subtype_comp_inclusion, range_subtype, range_subtype, range_subtype])
+    (ker_inclusion _ _ _) (by ext ⟨x, hx⟩; rfl)
     (by
       rintro ⟨b₁, hb₁⟩ ⟨b₂, hb₂⟩ eq
       obtain rfl : b₁ = b₂ := congr_arg Subtype.val eq

Mathlib/LinearAlgebra/FreeModule/PID.lean

@@ -231,14 +231,14 @@ theorem Submodule.basis_of_pid_aux [Finite ι] {O : Type*} [AddCommGroup O] [Mod
   have ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0 := by simpa only [ϕy'_eq] using one_ne_zero
   -- `M' := ker (ϕ : M → R)` is smaller than `M` and `N' := ker (ϕ : N → R)` is smaller than `N`.
   let M' : Submodule R O := ϕ.ker.map M.subtype
-  let N' : Submodule R O := (ϕ.comp (ofLe N_le_M)).ker.map N.subtype
+  let N' : Submodule R O := (ϕ.comp (inclusion N_le_M)).ker.map N.subtype
   have M'_le_M : M' ≤ M := M.map_subtype_le (LinearMap.ker ϕ)
   have N'_le_M' : N' ≤ M' := by
     intro x hx
     simp only [mem_map, LinearMap.mem_ker] at hx ⊢
     obtain ⟨⟨x, xN⟩, hx, rfl⟩ := hx
     exact ⟨⟨x, N_le_M xN⟩, hx, rfl⟩
-  have N'_le_N : N' ≤ N := N.map_subtype_le (LinearMap.ker (ϕ.comp (ofLe N_le_M)))
+  have N'_le_N : N' ≤ N := N.map_subtype_le (LinearMap.ker (ϕ.comp (inclusion N_le_M)))
   -- So fill in those results as well.
   refine' ⟨M', M'_le_M, N', N'_le_N, N'_le_M', _⟩
   -- Note that `y'` is orthogonal to `M'`.
@@ -284,7 +284,7 @@ theorem Submodule.basis_of_pid_aux [Finite ι] {O : Type*} [AddCommGroup O] [Mod
   · simp only [Fin.cons_zero, Fin.castLE_zero]
     exact a_smul_y'.symm
   · rw [Fin.castLE_succ]
-    simp only [Fin.cons_succ, Function.comp_apply, coe_ofLe, map_coe, coeSubtype, h i]
+    simp only [Fin.cons_succ, Function.comp_apply, coe_inclusion, map_coe, coeSubtype, h i]
 #align submodule.basis_of_pid_aux Submodule.basis_of_pid_aux
 
 /-- A submodule of a free `R`-module of finite rank is also a free `R`-module of finite rank,