chore: cleanup more erw (#20601)

Mathlib/Algebra/Algebra/Operations.lean

@@ -388,7 +388,8 @@ variable {R} (P Q)
 
 protected theorem mul_one : M * 1 = M := by
   conv_lhs => rw [one_eq_span, ← span_eq M]
-  erw [span_mul_span, mul_one, span_eq]
+  rw [span_mul_span]
+  simp
 
 protected theorem map_mul {A'} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') :
     map f.toLinearMap (M * N) = map f.toLinearMap M * map f.toLinearMap N :=
@@ -832,7 +833,9 @@ protected theorem map_div {B : Type*} [CommSemiring B] [Algebra R B] (I J : Subm
     obtain ⟨xz, xz_mem, hxz⟩ := hx (h z) ⟨z, hz, rfl⟩
     convert xz_mem
     apply h.injective
-    erw [map_mul, h.apply_symm_apply, hxz]
+    rw [map_mul, h.apply_symm_apply]
+    simp only [AlgEquiv.toLinearMap_apply] at hxz
+    rw [hxz]
 
 end Quotient
 

Mathlib/Algebra/BigOperators/Finprod.lean

@@ -376,11 +376,12 @@ theorem finprod_eq_prod_of_fintype [Fintype α] (f : α → M) : ∏ᶠ i : α,
 theorem finprod_cond_eq_prod_of_cond_iff (f : α → M) {p : α → Prop} {t : Finset α}
     (h : ∀ {x}, f x ≠ 1 → (p x ↔ x ∈ t)) : (∏ᶠ (i) (_ : p i), f i) = ∏ i ∈ t, f i := by
   set s := { x | p x }
+  change ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ i ∈ t, f i
   have : mulSupport (s.mulIndicator f) ⊆ t := by
     rw [Set.mulSupport_mulIndicator]
     intro x hx
     exact (h hx.2).1 hx.1
-  erw [finprod_mem_def, finprod_eq_prod_of_mulSupport_subset _ this]
+  rw [finprod_mem_def, finprod_eq_prod_of_mulSupport_subset _ this]
   refine Finset.prod_congr rfl fun x hx => mulIndicator_apply_eq_self.2 fun hxs => ?_
   contrapose! hxs
   exact (h hxs).2 hx

Mathlib/Algebra/BigOperators/Group/Finset.lean

@@ -952,8 +952,8 @@ theorem prod_eq_mul {s : Finset α} {f : α → β} (a b : α) (hn : a ≠ b)
 "A sum over `s.subtype p` equals one over `{x ∈ s | p x}`."]
 theorem prod_subtype_eq_prod_filter (f : α → β) {p : α → Prop} [DecidablePred p] :
     ∏ x ∈ s.subtype p, f x = ∏ x ∈ s with p x, f x := by
-  conv_lhs => erw [← prod_map (s.subtype p) (Function.Embedding.subtype _) f]
-  exact prod_congr (subtype_map _) fun x _hx => rfl
+  have := prod_map (s.subtype p) (Function.Embedding.subtype _) f
+  simp_all
 
 /-- If all elements of a `Finset` satisfy the predicate `p`, a product
 over `s.subtype p` equals that product over `s`. -/

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -1136,7 +1136,8 @@ noncomputable def normalizedGCDMonoidOfLCM [NormalizationMonoid α] [DecidableEq
       conv_lhs =>
         congr
         rw [← normalize_lcm a b]
-      erw [← normalize.map_mul, ← Classical.choose_spec (exists_gcd a b), normalize_idem]
+      rw [← normalize_apply, ← normalize.map_mul,
+        ← Classical.choose_spec (exists_gcd a b), normalize_idem]
     lcm_zero_left := fun _ => eq_zero_of_zero_dvd (dvd_lcm_left _ _)
     lcm_zero_right := fun _ => eq_zero_of_zero_dvd (dvd_lcm_right _ _)
     gcd_dvd_left := fun a b => by

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -414,7 +414,8 @@ def conjugatesOfSet (s : Set G) : Set G :=
   ⋃ a ∈ s, conjugatesOf a
 
 theorem mem_conjugatesOfSet_iff {x : G} : x ∈ conjugatesOfSet s ↔ ∃ a ∈ s, IsConj a x := by
-  erw [Set.mem_iUnion₂]; simp only [conjugatesOf, isConj_iff, Set.mem_setOf_eq, exists_prop]
+  rw [conjugatesOfSet, Set.mem_iUnion₂]
+  simp only [conjugatesOf, isConj_iff, Set.mem_setOf_eq, exists_prop]
 
 theorem subset_conjugatesOfSet : s ⊆ conjugatesOfSet s := fun (x : G) (h : x ∈ s) =>
   mem_conjugatesOfSet_iff.2 ⟨x, h, IsConj.refl _⟩

Mathlib/Algebra/GroupWithZero/Basic.lean

@@ -397,7 +397,7 @@ lemma zero_zpow_eq_one₀ {n : ℤ} : (0 : G₀) ^ n = 1 ↔ n = 0 := by
 
 lemma zpow_add_one₀ (ha : a ≠ 0) : ∀ n : ℤ, a ^ (n + 1) = a ^ n * a
   | (n : ℕ) => by simp only [← Int.ofNat_succ, zpow_natCast, pow_succ]
-  | .negSucc 0 => by erw [zpow_zero, zpow_negSucc, pow_one, inv_mul_cancel₀ ha]
+  | .negSucc 0 => by simp [ha]
   | .negSucc (n + 1) => by
     rw [Int.negSucc_eq, zpow_neg, Int.neg_add, Int.neg_add_cancel_right, zpow_neg, ← Int.ofNat_succ,
       zpow_natCast, zpow_natCast, pow_succ' _ (n + 1), mul_inv_rev, mul_assoc, inv_mul_cancel₀ ha,

Mathlib/Algebra/Module/Hom.lean

@@ -69,7 +69,9 @@ instance instDomMulActModule
   add_smul s s' f := AddMonoidHom.ext fun m ↦ by
     simp_rw [AddMonoidHom.add_apply, DomMulAct.smul_addMonoidHom_apply, ← map_add, ← add_smul]; rfl
   zero_smul _ := AddMonoidHom.ext fun _ ↦ by
-    erw [DomMulAct.smul_addMonoidHom_apply, zero_smul, map_zero]; rfl
+    rw [DomMulAct.smul_addMonoidHom_apply]
+    -- TODO there should be a simp lemma for `DomMulAct.mk.symm 0`
+    simp [DomMulAct.mk, MulOpposite.opEquiv]
 
 end AddMonoidHom
 

Mathlib/Algebra/Ring/Subsemiring/Basic.lean

@@ -793,12 +793,18 @@ theorem ofLeftInverseS_symm_apply {g : S → R} {f : R →+* S} (h : Function.Le
 
 /-- Given an equivalence `e : R ≃+* S` of semirings and a subsemiring `s` of `R`,
 `subsemiring_map e s` is the induced equivalence between `s` and `s.map e` -/
-@[simps!]
-def subsemiringMap (e : R ≃+* S) (s : Subsemiring R) : s ≃+* s.map e.toRingHom :=
+def subsemiringMap (e : R ≃+* S) (s : Subsemiring R) : s ≃+* s.map (e : R →+* S) :=
   { e.toAddEquiv.addSubmonoidMap s.toAddSubmonoid, e.toMulEquiv.submonoidMap s.toSubmonoid with }
 
--- These lemmas have always been bad (https://github.com/leanprover-community/mathlib4/issues/7657), but https://github.com/leanprover/lean4/pull/2644 made `simp` start noticing
-attribute [nolint simpNF] RingEquiv.subsemiringMap_symm_apply_coe RingEquiv.subsemiringMap_apply_coe
+@[simp]
+theorem subsemiringMap_apply_coe (e : R ≃+* S) (s : Subsemiring R) (x : s) :
+    ((subsemiringMap e s) x : S) = e x :=
+  rfl
+
+@[simp]
+theorem subsemiringMap_symm_apply_coe (e : R ≃+* S) (s : Subsemiring R) (x : s.map e.toRingHom) :
+    ((subsemiringMap e s).symm x : R) = e.symm x :=
+  rfl
 
 end RingEquiv
 

Mathlib/GroupTheory/GroupAction/DomAct/Basic.lean

@@ -112,7 +112,7 @@ run_cmd
     `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
     `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
     `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
-    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `NonAssocSemiring, `Semiring,
+    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
     `Ring, `CommRing].map Lean.mkIdent do
   Lean.Elab.Command.elabCommand (← `(
     @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›