chore(LinearAlgebra/CliffordAlgebra/EvenEquiv): remove erws (leanprover-community#38684)

- rewrites the `toEven` and `toEven_ι` proofs through `even_toSubmodule`, replacing the `erw` steps with `simp` and `rw`

Extracted from leanprover-community#38415

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Author: yuanyi-350

Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean

@@ -113,16 +113,13 @@ def toEven : CliffordAlgebra Q →ₐ[R] CliffordAlgebra.even (Q' Q) := by
     rw [Subtype.coe_mk, pow_two]
     exact Submodule.mul_mem_mul (LinearMap.mem_range_self _ _) (LinearMap.mem_range_self _ _)
   · ext1
-    rw [Subalgebra.coe_mul] -- Porting note: was part of the `dsimp only` below
-    erw [LinearMap.codRestrict_apply] -- Porting note: was part of the `dsimp only` below
-    dsimp only [LinearMap.comp_apply, LinearMap.mulLeft_apply, Subalgebra.coe_algebraMap]
-    rw [← mul_assoc, e0_mul_v_mul_e0, v_sq_scalar]
+    simp only [Subalgebra.coe_mul, ← even_toSubmodule]
+    rw [LinearMap.codRestrict_apply]
+    simp [← mul_assoc, v_sq_scalar]
 
 theorem toEven_ι (m : M) : (toEven Q (ι Q m) : CliffordAlgebra (Q' Q)) = e0 Q * v Q m := by
-  rw [toEven, CliffordAlgebra.lift_ι_apply]
-  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11224): was `rw`
-  erw [LinearMap.codRestrict_apply]
-  rw [LinearMap.coe_comp, Function.comp_apply, LinearMap.mulLeft_apply]
+  simp only [toEven, CliffordAlgebra.lift_ι_apply, ← even_toSubmodule]
+  rw [LinearMap.codRestrict_apply, LinearMap.coe_comp, Function.comp_apply, LinearMap.mulLeft_apply]
 
 /-- The embedding from the even subalgebra with an extra dimension into the original algebra. -/
 def ofEven : CliffordAlgebra.even (Q' Q) →ₐ[R] CliffordAlgebra Q := by