diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean
index 7a89455eb57e99..9917233aedbacd 100644
--- a/Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean
+++ b/Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean
@@ -136,7 +136,7 @@ theorem conjAct_smul_range_ι {x : (CliffordAlgebra Q)ˣ} (hx : x ∈ lipschitzG
       refine Eq.trans_le ?_ this
       simp only [map_inv, smul_inv_smul]
   intro x hx
-  erw [Submodule.map_le_iff_le_comap]
+  rw [Submodule.pointwise_smul_def, Submodule.map_le_iff_le_comap]
   rintro _ ⟨m, rfl⟩
   exact conjAct_smul_ι_mem_range_ι hx _