chore(GroupTheory): erw cleanup (#23406)

Some more proof refactoring so that we can get rid of `erw`s. One issue appearing in a few places is `SetLike.coeSort_coe` (saying coercing to a set, then to a sort is the same as the generic `SetLike` coercion to sort) making it impossible to apply lemmas involving elements of subgroups coerced to sets coerced to types. Maybe remove it from the `dsimp` set?

Author: Vierkantor

Mathlib/GroupTheory/CoprodI.lean

@@ -134,9 +134,9 @@ variable {N : Type*} [Monoid N]
 theorem ext_hom (f g : CoprodI M →* N) (h : ∀ i, f.comp (of : M i →* _) = g.comp of) : f = g :=
   (MonoidHom.cancel_right Con.mk'_surjective).mp <|
     FreeMonoid.hom_eq fun ⟨i, x⟩ => by
-      -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
-      erw [MonoidHom.comp_apply, MonoidHom.comp_apply, ← of_apply, ← MonoidHom.comp_apply, ←
-        MonoidHom.comp_apply, h]; rfl
+      rw [MonoidHom.comp_apply, MonoidHom.comp_apply, ← of_apply]
+      unfold CoprodI
+      rw [← MonoidHom.comp_apply, ← MonoidHom.comp_apply, h]
 
 /-- A map out of the free product corresponds to a family of maps out of the summands. This is the
 universal property of the free product, characterizing it as a categorical coproduct. -/
@@ -151,8 +151,7 @@ def lift : (∀ i, M i →* N) ≃ (CoprodI M →* N) where
   left_inv := by
     intro fi
     ext i x
-    -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
-    erw [MonoidHom.comp_apply, of_apply, Con.lift_mk', FreeMonoid.lift_eval_of]
+    rfl
   right_inv := by
     intro f
     ext i x

Mathlib/GroupTheory/FreeGroup/NielsenSchreier.lean

@@ -219,7 +219,9 @@ lemma endIsFree : IsFreeGroup (End (root' T)) :=
       refine ⟨F'.mapEnd _, ?_, ?_⟩
       · suffices ∀ {x y} (q : x ⟶ y), F'.map (loopOfHom T q) = (F'.map q : X) by
           rintro ⟨⟨a, b, e⟩, h⟩
-          erw [Functor.mapEnd_apply, this, hF']
+          -- Work around the defeq `X = End (F'.obj (IsFreeGroupoid.SpanningTree.root' T))`
+          erw [Functor.mapEnd_apply]
+          rw [this, hF']
           exact dif_neg h
         intros x y q
         suffices ∀ {a} (p : Path (root T) a), F'.map (homOfPath T p) = 1 by

Mathlib/GroupTheory/GroupAction/Defs.lean

@@ -237,6 +237,9 @@ theorem smul_mem_orbit_smul (g h : G) (a : α) : g • a ∈ orbit G (h • a) :
 instance instMulAction (H : Subgroup G) : MulAction H α :=
   inferInstanceAs (MulAction H.toSubmonoid α)
 
+@[to_additive]
+lemma subgroup_smul_def {H : Subgroup G} (a : H) (b : α) : a • b = (a : G) • b := rfl
+
 @[to_additive]
 lemma orbit_subgroup_subset (H : Subgroup G) (a : α) : orbit H a ⊆ orbit G a :=
   orbit_submonoid_subset H.toSubmonoid a
@@ -258,7 +261,7 @@ lemma mem_subgroup_orbit_iff {H : Subgroup G} {x : α} {a b : orbit G x} :
     exact MulAction.mem_orbit _ g
   · rcases h with ⟨g, h⟩
     dsimp at h
-    erw [← orbit.coe_smul, ← Subtype.ext_iff] at h
+    rw [subgroup_smul_def, ← orbit.coe_smul, ← Subtype.ext_iff] at h
     subst h
     exact MulAction.mem_orbit _ g
 
@@ -422,7 +425,7 @@ lemma orbitRel.Quotient.mem_subgroup_orbit_iff {H : Subgroup G} {x : orbitRel.Qu
   refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
   · rcases h with ⟨g, h⟩
     dsimp at h
-    erw [← orbit.coe_smul, ← Subtype.ext_iff] at h
+    rw [subgroup_smul_def, ← orbit.coe_smul, ← Subtype.ext_iff] at h
     subst h
     exact MulAction.mem_orbit _ g
   · rcases h with ⟨g, rfl⟩

Mathlib/GroupTheory/HNNExtension.lean

@@ -167,8 +167,7 @@ theorem toSubgroupEquiv_neg_one : toSubgroupEquiv φ (-1) = φ.symm := rfl
 theorem toSubgroupEquiv_neg_apply (u : ℤˣ) (a : toSubgroup A B u) :
     (toSubgroupEquiv φ (-u) (toSubgroupEquiv φ u a) : G) = a := by
   rcases Int.units_eq_one_or u with rfl | rfl
-  · -- This used to be `simp` before https://github.com/leanprover/lean4/pull/2644
-    simp; erw [MulEquiv.symm_apply_apply]
+  · simp [toSubgroup]
   · simp only [toSubgroup_neg_one, toSubgroupEquiv_neg_one, SetLike.coe_eq_coe]
     exact φ.apply_symm_apply a
 
@@ -419,10 +418,8 @@ theorem unitsSMul_neg (u : ℤˣ) (w : NormalWord d) :
   · have hncan : ¬ Cancels u w := (unitsSMul_cancels_iff _ _ _).1 hcan
     unfold unitsSMul
     simp only [dif_neg hncan]
-    simp [unitsSMulWithCancel, unitsSMulGroup, (d.compl u).equiv_snd_eq_inv_mul]
-    -- This used to be the end of the proof before https://github.com/leanprover/lean4/pull/2644
-    erw [(d.compl u).equiv_snd_eq_inv_mul]
-    simp
+    simp [unitsSMulWithCancel, unitsSMulGroup, (d.compl u).equiv_snd_eq_inv_mul,
+      -SetLike.coe_sort_coe]
   · have hcan2 : Cancels u w := not_not.1 (mt (unitsSMul_cancels_iff _ _ _).2 hcan)
     unfold unitsSMul at hcan ⊢
     simp only [dif_pos hcan2] at hcan ⊢
@@ -445,10 +442,8 @@ theorem unitsSMul_neg (u : ℤˣ) (w : NormalWord d) :
       · -- The next two lines were not needed before https://github.com/leanprover/lean4/pull/2644
         dsimp
         conv_lhs => erw [IsComplement.equiv_mul_left]
-        simp [mul_assoc, Units.ext_iff, (d.compl (-u)).equiv_snd_eq_inv_mul, this]
-        -- The next two lines were not needed before https://github.com/leanprover/lean4/pull/2644
-        erw [(d.compl (-u)).equiv_snd_eq_inv_mul, this]
-        simp
+        simp [mul_assoc, Units.ext_iff, (d.compl (-u)).equiv_snd_eq_inv_mul, this,
+          -SetLike.coe_sort_coe]
 
 /-- the equivalence given by multiplication on the left by `t` -/
 @[simps]
@@ -562,15 +557,12 @@ theorem prod_smul_empty (w : NormalWord d) :
     rw [prod_cons, ← mul_assoc, mul_smul, ih, mul_smul, t_pow_smul_eq_unitsSMul,
       of_smul_eq_smul, unitsSMul]
     rw [dif_neg (not_cancels_of_cons_hyp u w h2)]
-    -- The next 3 lines were a single `simp [...]` before https://github.com/leanprover/lean4/pull/2644
-    simp only [unitsSMulGroup]
-    simp_rw [SetLike.coe_sort_coe]
-    erw [(d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1]
-    ext <;> simp
-    -- The next 4 were not needed before https://github.com/leanprover/lean4/pull/2644
-    erw [(d.compl _).equiv_snd_eq_inv_mul]
-    simp_rw [SetLike.coe_sort_coe]
-    erw [(d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1]
+    simp [unitsSMulGroup, (d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1,
+      -SetLike.coe_sort_coe]
+    ext <;> simp [-SetLike.coe_sort_coe]
+    -- The next 3 lines were not needed before https://github.com/leanprover/lean4/pull/2644
+    rw [(d.compl _).equiv_snd_eq_inv_mul,
+      (d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1]
     simp
 
 variable (d)
@@ -650,8 +642,10 @@ theorem exists_normalWord_prod_eq
             (List.head?_eq_head _) hS
           rwa [List.head?_eq_head hl, Option.map_some', ← this, Option.some_inj] at hx'
         simp at this
-      erw [List.map_cons, mul_smul, of_smul_eq_smul, NormalWord.group_smul_def,
-        t_pow_smul_eq_unitsSMul, unitsSMul, dif_neg this, ← hw'2]
+      rw [List.map_cons, mul_smul, of_smul_eq_smul, NormalWord.group_smul_def,
+        t_pow_smul_eq_unitsSMul, unitsSMul]
+      erw [dif_neg this]
+      rw [← hw'2]
       simp [mul_assoc, unitsSMulGroup, (d.compl _).coe_equiv_snd_eq_one_iff_mem]
 
 /-- Two reduced words representing the same element of the `HNNExtension G A B φ` have the same

Mathlib/GroupTheory/Perm/Cycle/Basic.lean

@@ -314,7 +314,7 @@ noncomputable def IsCycle.zpowersEquivSupport {σ : Perm α} (hσ : IsCycle σ)
     (fun (τ : ↥ ((Subgroup.zpowers σ) : Set (Perm α))) =>
       ⟨(τ : Perm α) (Classical.choose hσ), by
         obtain ⟨τ, n, rfl⟩ := τ
-        erw [Finset.mem_coe, Subtype.coe_mk, zpow_apply_mem_support, mem_support]
+        rw [Subtype.coe_mk, zpow_apply_mem_support, mem_support]
         exact (Classical.choose_spec hσ).1⟩)
     (by
       constructor
@@ -326,7 +326,7 @@ noncomputable def IsCycle.zpowersEquivSupport {σ : Perm α} (hσ : IsCycle σ)
           rw [Subtype.coe_mk, Subtype.coe_mk, zpow_apply_comm σ m i, zpow_apply_comm σ n i]
           exact congr_arg _ (Subtype.ext_iff.mp h)
       · rintro ⟨y, hy⟩
-        erw [Finset.mem_coe, mem_support] at hy
+        rw [mem_support] at hy
         obtain ⟨n, rfl⟩ := (Classical.choose_spec hσ).2 hy
         exact ⟨⟨σ ^ n, n, rfl⟩, rfl⟩)
 
@@ -647,14 +647,7 @@ theorem IsCycle.isConj (hσ : IsCycle σ) (hτ : IsCycle τ) (h : #σ.support =
   intro x hx
   simp only [Perm.mul_apply, Equiv.trans_apply, Equiv.sumCongr_apply]
   obtain ⟨n, rfl⟩ := hσ.exists_pow_eq (Classical.choose_spec hσ).1 (mem_support.1 hx)
-  erw [hσ.zpowersEquivSupport_symm_apply n]
-  simp only [← Perm.mul_apply, ← pow_succ']
-  erw [hσ.zpowersEquivSupport_symm_apply (n + 1)]
-  -- This used to be a `simp only` before https://github.com/leanprover/lean4/pull/2644
-  erw [zpowersEquivZPowers_apply, zpowersEquivZPowers_apply, zpowersEquivSupport_apply]
-  -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
-  simp_rw [pow_succ', Perm.mul_apply]
-  rfl
+  simp [← Perm.mul_apply, ← pow_succ']
 
 theorem IsCycle.isConj_iff (hσ : IsCycle σ) (hτ : IsCycle τ) :
     IsConj σ τ ↔ #σ.support = #τ.support where
@@ -774,10 +767,7 @@ theorem IsCycleOn.pow_apply_eq {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈
     rw [← this, orderOf_dvd_iff_pow_eq_one,
       (hf.isCycle_subtypePerm hs).pow_eq_one_iff'
         (ne_of_apply_ne ((↑) : s → α) <| hf.apply_ne hs (⟨a, ha⟩ : s).2)]
-    simp
-    -- This used to be the end of the proof before https://github.com/leanprover/lean4/pull/2644
-    erw [subtypePerm_apply]
-    simp
+    simp [-coe_sort_coe]
 
 theorem IsCycleOn.zpow_apply_eq {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) :
     ∀ {n : ℤ}, (f ^ n) a = a ↔ (#s : ℤ) ∣ n

Mathlib/GroupTheory/Perm/Fin.lean

@@ -153,10 +153,9 @@ theorem cycleRange_of_le {n : ℕ} [NeZero n] {i j : Fin n} (h : j ≤ i) :
   have : j = (Fin.castLE (Nat.succ_le_of_lt i.is_lt))
     ⟨j, lt_of_le_of_lt h (Nat.lt_succ_self i)⟩ := by simp
   ext
-  erw [this, cycleRange, ofLeftInverse'_eq_ofInjective, ←
-    Function.Embedding.toEquivRange_eq_ofInjective, ← viaFintypeEmbedding,
-    viaFintypeEmbedding_apply_image, Function.Embedding.coeFn_mk,
-    coe_castLE, coe_finRotate]
+  rw [this, cycleRange, ofLeftInverse'_eq_ofInjective, ←
+    Function.Embedding.toEquivRange_eq_ofInjective, ← viaFintypeEmbedding, ← coe_castLEEmb,
+    viaFintypeEmbedding_apply_image, coe_castLEEmb, coe_castLE, coe_finRotate]
   simp only [Fin.ext_iff, val_last, val_mk, val_zero, Fin.eta, castLE_mk]
   split_ifs with heq
   · rfl

Mathlib/GroupTheory/Perm/Finite.lean

@@ -142,12 +142,12 @@ theorem mem_sumCongrHom_range_of_perm_mapsTo_inl {m n : Type*} [Finite m] [Finit
     · rw [Equiv.sumCongr_apply, Sum.map_inl, permCongr_apply, Equiv.symm_symm,
         apply_ofInjective_symm Sum.inl_injective]
       rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk]
-      -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
-      erw [subtypePerm_apply]
+      dsimp [Set.range]
+      rw [subtypePerm_apply]
     · rw [Equiv.sumCongr_apply, Sum.map_inr, permCongr_apply, Equiv.symm_symm,
-        apply_ofInjective_symm Sum.inr_injective]
-      erw [subtypePerm_apply]
-      rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk]
+        apply_ofInjective_symm Sum.inr_injective, ofInjective_apply]
+      dsimp [Set.range]
+      rw [subtypePerm_apply]
 
 nonrec theorem Disjoint.orderOf {σ τ : Perm α} (hστ : Disjoint σ τ) :
     orderOf (σ * τ) = Nat.lcm (orderOf σ) (orderOf τ) :=

Mathlib/GroupTheory/Torsion.lean

@@ -66,7 +66,8 @@ noncomputable def IsTorsion.group [Monoid G] (tG : IsTorsion G) : Group G :=
   { ‹Monoid G› with
     inv := fun g => g ^ (orderOf g - 1)
     inv_mul_cancel := fun g => by
-      erw [← pow_succ, tsub_add_cancel_of_le, pow_orderOf_eq_one]
+      dsimp only
+      rw [← pow_succ, tsub_add_cancel_of_le, pow_orderOf_eq_one]
       exact (tG g).orderOf_pos }
 
 section Group