no goals
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : BilinForm R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : N ≃ₗ[R] M
f : { x // x ∈ skewAdjointLieSubalgebra B }
⊢ ↑(↑(LieEquiv.symm (skewAdjointLieSubalgebraEquiv B e)) f) = ↑(LinearEquiv.lieConj (LinearEquiv.symm e)) ↑f
simp [skewAdjointLieSubalgebraEquiv]