From d529964daa5c1ffbdfb9e6cbe21e9d4fa858941c Mon Sep 17 00:00:00 2001
From: yuanyi-350 <kysyy1@126.com>
Date: Sat, 25 Apr 2026 19:54:48 +0800
Subject: [PATCH] chore(Algebra/Lie/Classical): remove an erw

---
 Mathlib/Algebra/Lie/Classical.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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.