diff --git a/Mathlib/Algebra/Lie/Classical.lean b/Mathlib/Algebra/Lie/Classical.lean
index c318f18543c6ba..f90a39f51fc2f2 100644
--- a/Mathlib/Algebra/Lie/Classical.lean
+++ b/Mathlib/Algebra/Lie/Classical.lean
@@ -232,7 +232,8 @@ 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]
-  erw [skewAdjointMatricesLieSubalgebraEquiv_apply]
+  simp only [so']
+  rw [skewAdjointMatricesLieSubalgebraEquiv_apply]
 
 /-- A matrix defining a canonical even-rank symmetric bilinear form.