chore: remove some uses of erw introduced in relation to lean4 PR leanprover-community#2644 (leanprover-community#31680)

Author: euprunin

Mathlib/Algebra/Category/ModuleCat/Kernels.lean

@@ -33,11 +33,7 @@ def kernelIsLimit : IsLimit (kernelCone f) :=
     (fun s => ofHom <|
     -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11036): broken dot notation on LinearMap.ker
       LinearMap.codRestrict (LinearMap.ker f.hom) (Fork.ι s).hom fun c =>
-        LinearMap.mem_ker.2 <| by
-          -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
-          erw [← ConcreteCategory.comp_apply]
-          rw [Fork.condition, HasZeroMorphisms.comp_zero (Fork.ι s) N]
-          rfl)
+        LinearMap.mem_ker.2 <| by simp [← ConcreteCategory.comp_apply])
     (fun _ => hom_ext <| LinearMap.subtype_comp_codRestrict _ _ _) fun s m h =>
       hom_ext <| LinearMap.ext fun x => Subtype.ext_iff.2 (by simp [← h]; rfl)
 

Mathlib/Algebra/Lie/Classical.lean

@@ -233,8 +233,7 @@ theorem soIndefiniteEquiv_apply {i : R} (hi : i * i = -1) (A : so' p q R) :
     (soIndefiniteEquiv p q R hi A : Matrix (p ⊕ q) (p ⊕ q) R) =
       (Pso p q R i)⁻¹ * (A : Matrix (p ⊕ q) (p ⊕ q) R) * Pso p q R i := by
   rw [soIndefiniteEquiv, LieEquiv.trans_apply, LieEquiv.ofEq_apply]
-  -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
-  erw [skewAdjointMatricesLieSubalgebraEquiv_apply]
+  grind [skewAdjointMatricesLieSubalgebraEquiv_apply]
 
 /-- A matrix defining a canonical even-rank symmetric bilinear form.
 

Mathlib/Data/Matrix/Reflection.lean

@@ -213,8 +213,7 @@ example (A : Matrix (Fin 2) (Fin 2) α) :
 -/
 theorem etaExpand_eq {m n} (A : Matrix (Fin m) (Fin n) α) : etaExpand A = A := by
   simp_rw [etaExpand, FinVec.etaExpand_eq, Matrix.of]
-  -- This to be in the above `simp_rw` before https://github.com/leanprover/lean4/pull/2644
-  erw [Equiv.refl_apply]
+  grind
 
 example (A : Matrix (Fin 2) (Fin 2) α) : A = !![A 0 0, A 0 1; A 1 0, A 1 1] :=
   (etaExpand_eq _).symm

Mathlib/GroupTheory/HNNExtension.lean

@@ -526,8 +526,7 @@ theorem prod_unitsSMul (u : ℤˣ) (w : NormalWord d) :
         -- simp [equiv_symm_eq_conj, mul_assoc].
         simp only [toSubgroup_neg_one, toSubgroupEquiv_neg_one, Units.val_neg, Units.val_one,
           Int.reduceNeg, zpow_neg, zpow_one, inv_inv]
-        erw [equiv_symm_eq_conj]
-        simp [mul_assoc]
+        grind [equiv_symm_eq_conj, mul_assoc]
   · simp only [unitsSMulGroup, SetLike.coe_sort_coe, prod_cons, prod_group_smul, map_mul, map_inv]
     rcases Int.units_eq_one_or u with (rfl | rfl)
     · -- Before https://github.com/leanprover/lean4/pull/2644, this proof was just

Mathlib/LinearAlgebra/AffineSpace/Independent.lean

@@ -402,8 +402,7 @@ theorem AffineEquiv.affineIndependent_iff {p : ι → P} (e : P ≃ᵃ[k] P₂)
 theorem AffineEquiv.affineIndependent_set_of_eq_iff {s : Set P} (e : P ≃ᵃ[k] P₂) :
     AffineIndependent k ((↑) : e '' s → P₂) ↔ AffineIndependent k ((↑) : s → P) := by
   have : e ∘ ((↑) : s → P) = ((↑) : e '' s → P₂) ∘ (e : P ≃ P₂).image s := rfl
-  -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
-  erw [← e.affineIndependent_iff, this, affineIndependent_equiv]
+  simp [← e.affineIndependent_iff, this, affineIndependent_equiv]
 
 end Composition
 

Mathlib/LinearAlgebra/FreeModule/Norm.lean

@@ -42,10 +42,7 @@ theorem associated_norm_prod_smith [Fintype ι] (b : Basis ι R S) {f : S} (hf :
     zero_smul, Finset.sum_ite_eq', mul_one, if_pos (Finset.mem_univ _), b'.equiv_apply]
   change _ = f * _
   rw [mul_comm, ← smul_eq_mul, LinearEquiv.restrictScalars_apply]
-  -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
-  erw [LinearEquiv.coord_apply_smul]
-  rw [Ideal.selfBasis_def]
-  rfl
+  grind [LinearEquiv.coord_apply_smul, Ideal.selfBasis_def]
 
 end CommRing
 

Mathlib/ModelTheory/DirectLimit.lean

@@ -58,9 +58,7 @@ theorem coe_natLERec (m n : ℕ) (h : m ≤ n) :
   obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
   ext x
   induction k with
-  | zero =>
-    -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
-    erw [natLERec, Nat.leRecOn_self, Embedding.refl_apply, Nat.leRecOn_self]
+  | zero => simp [natLERec, Nat.leRecOn_self]
   | succ k ih =>
     -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
     erw [Nat.leRecOn_succ le_self_add, natLERec, Nat.leRecOn_succ le_self_add, ← natLERec,