no goals
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A✝ A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ (-J l R) ⬝ Aᵀ ⬝ J l R ⬝ A = 1
simp only [Matrix.neg_mul, inv_left_mul_aux hA]