chore(Submonoid/Subgroup): rename subtype_range to range_subtype (#19518)

This matches the naming convention.

Author: YaelDillies

Mathlib/Algebra/DirectSum/Basic.lean

@@ -375,7 +375,7 @@ def IsInternal {M S : Type*} [DecidableEq ι] [AddCommMonoid M] [SetLike S M]
 
 theorem IsInternal.addSubmonoid_iSup_eq_top {M : Type*} [DecidableEq ι] [AddCommMonoid M]
     (A : ι → AddSubmonoid M) (h : IsInternal A) : iSup A = ⊤ := by
-  rw [AddSubmonoid.iSup_eq_mrange_dfinsupp_sumAddHom, AddMonoidHom.mrange_eq_top_iff_surjective]
+  rw [AddSubmonoid.iSup_eq_mrange_dfinsupp_sumAddHom, AddMonoidHom.mrange_eq_top]
   exact Function.Bijective.surjective h
 
 variable {M S : Type*} [AddCommMonoid M] [SetLike S M] [AddSubmonoidClass S M]

Mathlib/Algebra/Group/Subgroup/Ker.lean

@@ -117,6 +117,9 @@ lemma rangeRestrict_injective_iff {f : G →* N} : Injective f.rangeRestrict ↔
 theorem map_range (g : N →* P) (f : G →* N) : f.range.map g = (g.comp f).range := by
   rw [range_eq_map, range_eq_map]; exact (⊤ : Subgroup G).map_map g f
 
+@[to_additive]
+lemma range_comp (g : N →* P) (f : G →* N) : (g.comp f).range = f.range.map g := (map_range ..).symm
+
 @[to_additive]
 theorem range_eq_top {N} [Group N] {f : G →* N} :
     f.range = (⊤ : Subgroup N) ↔ Function.Surjective f :=
@@ -138,10 +141,11 @@ theorem range_one : (1 : G →* N).range = ⊥ :=
   SetLike.ext fun x => by simpa using @comm _ (· = ·) _ 1 x
 
 @[to_additive (attr := simp)]
-theorem _root_.Subgroup.subtype_range (H : Subgroup G) : H.subtype.range = H := by
-  rw [range_eq_map, ← SetLike.coe_set_eq, coe_map, Subgroup.coeSubtype]
-  ext
-  simp
+theorem _root_.Subgroup.range_subtype (H : Subgroup G) : H.subtype.range = H :=
+  SetLike.coe_injective <| (coe_range _).trans <| Subtype.range_coe
+
+@[to_additive (attr := deprecated (since := "2024-11-26"))]
+alias _root_.Subgroup.subtype_range := Subgroup.range_subtype
 
 @[to_additive (attr := simp)]
 theorem _root_.Subgroup.inclusion_range {H K : Subgroup G} (h_le : H ≤ K) :
@@ -368,7 +372,7 @@ theorem map_le_range (H : Subgroup G) : map f H ≤ f.range :=
 
 @[to_additive]
 theorem map_subtype_le {H : Subgroup G} (K : Subgroup H) : K.map H.subtype ≤ H :=
-  (K.map_le_range H.subtype).trans (le_of_eq H.subtype_range)
+  (K.map_le_range H.subtype).trans_eq H.range_subtype
 
 @[to_additive]
 theorem ker_le_comap (H : Subgroup N) : f.ker ≤ comap f H :=
@@ -466,7 +470,7 @@ theorem map_injective_of_ker_le {H K : Subgroup G} (hH : f.ker ≤ H) (hK : f.ke
 @[to_additive]
 theorem closure_preimage_eq_top (s : Set G) : closure ((closure s).subtype ⁻¹' s) = ⊤ := by
   apply map_injective (closure s).subtype_injective
-  rw [MonoidHom.map_closure, ← MonoidHom.range_eq_map, subtype_range,
+  rw [MonoidHom.map_closure, ← MonoidHom.range_eq_map, range_subtype,
     Set.image_preimage_eq_of_subset]
   rw [coeSubtype, Subtype.range_coe_subtype]
   exact subset_closure
@@ -487,7 +491,8 @@ theorem comap_sup_eq (H K : Subgroup N) (hf : Function.Surjective f) :
 @[to_additive]
 theorem sup_subgroupOf_eq {H K L : Subgroup G} (hH : H ≤ L) (hK : K ≤ L) :
     H.subgroupOf L ⊔ K.subgroupOf L = (H ⊔ K).subgroupOf L :=
-  comap_sup_eq_of_le_range L.subtype (hH.trans L.subtype_range.ge) (hK.trans L.subtype_range.ge)
+  comap_sup_eq_of_le_range L.subtype (hH.trans_eq L.range_subtype.symm)
+     (hK.trans_eq L.range_subtype.symm)
 
 @[to_additive]
 theorem codisjoint_subgroupOf_sup (H K : Subgroup G) :
@@ -501,7 +506,7 @@ theorem subgroupOf_sup (A A' B : Subgroup G) (hA : A ≤ B) (hA' : A' ≤ B) :
   refine
     map_injective_of_ker_le B.subtype (ker_le_comap _ _)
       (le_trans (ker_le_comap B.subtype _) le_sup_left) ?_
-  simp only [subgroupOf, map_comap_eq, map_sup, subtype_range]
+  simp only [subgroupOf, map_comap_eq, map_sup, range_subtype]
   rw [inf_of_le_right (sup_le hA hA'), inf_of_le_right hA', inf_of_le_right hA]
 
 end Subgroup

Mathlib/Algebra/Group/Submonoid/Membership.lean

@@ -543,7 +543,7 @@ open MonoidHom
 @[to_additive]
 theorem sup_eq_range (s t : Submonoid N) : s ⊔ t = mrange (s.subtype.coprod t.subtype) := by
   rw [mrange_eq_map, ← mrange_inl_sup_mrange_inr, map_sup, map_mrange, coprod_comp_inl, map_mrange,
-    coprod_comp_inr, range_subtype, range_subtype]
+    coprod_comp_inr, mrange_subtype, mrange_subtype]
 
 @[to_additive]
 theorem mem_sup {s t : Submonoid N} {x : N} : x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x := by

Mathlib/Algebra/Group/Submonoid/Operations.lean

@@ -628,6 +628,10 @@ theorem coe_mrange (f : F) : (mrange f : Set N) = Set.range f :=
 theorem mem_mrange {f : F} {y : N} : y ∈ mrange f ↔ ∃ x, f x = y :=
   Iff.rfl
 
+@[to_additive]
+lemma mrange_comp {O : Type*} [Monoid O] (f : N →* O) (g : M →* N) :
+    mrange (f.comp g) = (mrange g).map f := SetLike.coe_injective <| Set.range_comp f _
+
 @[to_additive]
 theorem mrange_eq_map (f : F) : mrange f = (⊤ : Submonoid M).map f :=
   Submonoid.copy_eq _
@@ -641,18 +645,18 @@ theorem map_mrange (g : N →* P) (f : M →* N) : f.mrange.map g = mrange (comp
   simpa only [mrange_eq_map] using (⊤ : Submonoid M).map_map g f
 
 @[to_additive]
-theorem mrange_eq_top_iff_surjective {f : F} : mrange f = (⊤ : Submonoid N) ↔ Surjective f :=
+theorem mrange_eq_top {f : F} : mrange f = (⊤ : Submonoid N) ↔ Surjective f :=
   SetLike.ext'_iff.trans <| Iff.trans (by rw [coe_mrange, coe_top]) Set.range_eq_univ
 
 @[deprecated (since := "2024-11-11")]
-alias mrange_top_iff_surjective := mrange_eq_top_iff_surjective
+alias mrange_top_iff_surjective := mrange_eq_top
 
 /-- The range of a surjective monoid hom is the whole of the codomain. -/
 @[to_additive (attr := simp)
   "The range of a surjective `AddMonoid` hom is the whole of the codomain."]
 theorem mrange_eq_top_of_surjective (f : F) (hf : Function.Surjective f) :
     mrange f = (⊤ : Submonoid N) :=
-  mrange_eq_top_iff_surjective.2 hf
+  mrange_eq_top.2 hf
 
 @[deprecated (since := "2024-11-11")] alias mrange_top_of_surjective := mrange_eq_top_of_surjective
 
@@ -863,9 +867,11 @@ def inclusion {S T : Submonoid M} (h : S ≤ T) : S →* T :=
   S.subtype.codRestrict _ fun x => h x.2
 
 @[to_additive (attr := simp)]
-theorem range_subtype (s : Submonoid M) : mrange s.subtype = s :=
+theorem mrange_subtype (s : Submonoid M) : mrange s.subtype = s :=
   SetLike.coe_injective <| (coe_mrange _).trans <| Subtype.range_coe
 
+@[to_additive (attr := deprecated (since := "2024-11-25"))] alias range_subtype := mrange_subtype
+
 @[to_additive]
 theorem eq_top_iff' : S = ⊤ ↔ ∀ x : M, x ∈ S :=
   eq_top_iff.trans ⟨fun h m => h <| mem_top m, fun h m _ => h m⟩

Mathlib/GroupTheory/Congruence/Basic.lean

@@ -173,7 +173,7 @@ variable (x y : M)
 @[to_additive (attr := simp)]
 -- Porting note: removed dot notation
 theorem mrange_mk' : MonoidHom.mrange c.mk' = ⊤ :=
-  MonoidHom.mrange_eq_top_iff_surjective.2 mk'_surjective
+  MonoidHom.mrange_eq_top.2 mk'_surjective
 
 variable {f : M →* P}
 

Mathlib/GroupTheory/Finiteness.lean

@@ -138,7 +138,7 @@ theorem Submonoid.FG.map_injective {M' : Type*} [Monoid M'] {P : Submonoid M} (e
 
 @[to_additive (attr := simp)]
 theorem Monoid.fg_iff_submonoid_fg (N : Submonoid M) : Monoid.FG N ↔ N.FG := by
-  conv_rhs => rw [← N.range_subtype, MonoidHom.mrange_eq_map]
+  conv_rhs => rw [← N.mrange_subtype, MonoidHom.mrange_eq_map]
   exact ⟨fun h => h.out.map N.subtype, fun h => ⟨h.map_injective N.subtype Subtype.coe_injective⟩⟩
 
 @[to_additive]
@@ -148,7 +148,7 @@ theorem Monoid.fg_of_surjective {M' : Type*} [Monoid M'] [Monoid.FG M] (f : M 
     obtain ⟨s, hs⟩ := Monoid.fg_def.mp ‹_›
     use s.image f
     rwa [Finset.coe_image, ← MonoidHom.map_mclosure, hs, ← MonoidHom.mrange_eq_map,
-      MonoidHom.mrange_eq_top_iff_surjective]
+      MonoidHom.mrange_eq_top]
 
 @[to_additive]
 instance Monoid.fg_range {M' : Type*} [Monoid M'] [Monoid.FG M] (f : M →* M') :

Mathlib/GroupTheory/Index.lean

@@ -80,7 +80,7 @@ theorem index_comap (f : G' →* G) :
 @[to_additive]
 theorem relindex_comap (f : G' →* G) (K : Subgroup G') :
     relindex (comap f H) K = relindex H (map f K) := by
-  rw [relindex, subgroupOf, comap_comap, index_comap, ← f.map_range, K.subtype_range]
+  rw [relindex, subgroupOf, comap_comap, index_comap, ← f.map_range, K.range_subtype]
 
 variable {H K L}
 
@@ -262,7 +262,7 @@ theorem index_map_of_injective {f : G →* G'} (hf : Function.Injective f) :
 @[to_additive]
 theorem index_map_subtype {H : Subgroup G} (K : Subgroup H) :
     (K.map H.subtype).index = K.index * H.index := by
-  rw [K.index_map_of_injective H.subtype_injective, H.subtype_range]
+  rw [K.index_map_of_injective H.subtype_injective, H.range_subtype]
 
 @[to_additive]
 theorem index_eq_card : H.index = Nat.card (G ⧸ H) :=

Mathlib/GroupTheory/PGroup.lean

@@ -240,7 +240,7 @@ theorem to_inf_right {H K : Subgroup G} (hK : IsPGroup p K) : IsPGroup p (H ⊓
 
 theorem map {H : Subgroup G} (hH : IsPGroup p H) {K : Type*} [Group K] (ϕ : G →* K) :
     IsPGroup p (H.map ϕ) := by
-  rw [← H.subtype_range, MonoidHom.map_range]
+  rw [← H.range_subtype, MonoidHom.map_range]
   exact hH.of_surjective (ϕ.restrict H).rangeRestrict (ϕ.restrict H).rangeRestrict_surjective
 
 theorem comap_of_ker_isPGroup {H : Subgroup G} (hH : IsPGroup p H) {K : Type*} [Group K]

Mathlib/GroupTheory/SchurZassenhaus.lean

@@ -174,7 +174,7 @@ private theorem step1 (K : Subgroup G) (hK : K ⊔ N = ⊤) : K = ⊤ := by
   replace hH : Nat.card (H.map K.subtype) = N.index := by
     rw [← relindex_bot_left, ← relindex_comap, MonoidHom.comap_bot, Subgroup.ker_subtype,
       relindex_bot_left, ← IsComplement'.index_eq_card (IsComplement'.symm hH), index_comap,
-      subtype_range, ← relindex_sup_right, hK, relindex_top_right]
+      range_subtype, ← relindex_sup_right, hK, relindex_top_right]
   have h7 : Nat.card N * Nat.card (H.map K.subtype) = Nat.card G := by
     rw [hH, ← N.index_mul_card, mul_comm]
   have h8 : (Nat.card N).Coprime (Nat.card (H.map K.subtype)) := by
@@ -220,7 +220,7 @@ private theorem step3 (K : Subgroup N) [(K.map N.subtype).Normal] : K = ⊥ ∨
   conv at key =>
     rhs
     rhs
-    rw [← N.subtype_range, N.subtype.range_eq_map]
+    rw [← N.range_subtype, N.subtype.range_eq_map]
   have inj := map_injective N.subtype_injective
   rwa [inj.eq_iff, inj.eq_iff] at key
 
@@ -239,7 +239,7 @@ include h2 in
 private theorem step6 : IsPGroup (Nat.card N).minFac N := by
   haveI : Fact (Nat.card N).minFac.Prime := ⟨step4 h1 h3⟩
   refine Sylow.nonempty.elim fun P => P.2.of_surjective P.1.subtype ?_
-  rw [← MonoidHom.range_eq_top, subtype_range]
+  rw [← MonoidHom.range_eq_top, range_subtype]
   haveI : (P.1.map N.subtype).Normal :=
     normalizer_eq_top.mp (step1 h1 h2 h3 (P.1.map N.subtype).normalizer P.normalizer_sup_eq_top)
   exact (step3 h1 h2 h3 P.1).resolve_left (step5 h1 h3)

Mathlib/GroupTheory/SpecificGroups/Alternating.lean

@@ -168,7 +168,7 @@ theorem IsThreeCycle.alternating_normalClosure (h5 : 5 ≤ Fintype.card α) {f :
     (by
       have hi : Function.Injective (alternatingGroup α).subtype := Subtype.coe_injective
       refine eq_top_iff.1 (map_injective hi (le_antisymm (map_mono le_top) ?_))
-      rw [← MonoidHom.range_eq_map, subtype_range, normalClosure, MonoidHom.map_closure]
+      rw [← MonoidHom.range_eq_map, range_subtype, normalClosure, MonoidHom.map_closure]
       refine (le_of_eq closure_three_cycles_eq_alternating.symm).trans (closure_mono ?_)
       intro g h
       obtain ⟨c, rfl⟩ := isConj_iff.1 (isConj_iff_cycleType_eq.2 (hf.trans h.symm))