l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A✝ : Matrix (l ⊕ l) (l ⊕ l) R
A : { x // x ∈ symplecticGroup l R }
⊢ (-J l R) ⬝ (↑A)ᵀ ⬝ J l R ⬝ ↑A = 1
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A✝ : Matrix (l ⊕ l) (l ⊕ l) R
A : { x // x ∈ symplecticGroup l R }
⊢ ↑A⁻¹ = (↑A)⁻¹
refine' (coe_inv A).trans (inv_eq_left_inv _).symm
no goals
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A✝ : Matrix (l ⊕ l) (l ⊕ l) R
A : { x // x ∈ symplecticGroup l R }
⊢ (-J l R) ⬝ (↑A)ᵀ ⬝ J l R ⬝ ↑A = 1
simp [inv_left_mul_aux, coe_inv]