l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
⊢ fromBlocks ((0 ⬝ 0 + (-1) ⬝ 1) ⬝ 0ᵀ + (0 ⬝ (-1) + (-1) ⬝ 0) ⬝ (-1)ᵀ)
      ((0 ⬝ 0 + (-1) ⬝ 1) ⬝ 1ᵀ + (0 ⬝ (-1) + (-1) ⬝ 0) ⬝ 0ᵀ) ((1 ⬝ 0 + 0 ⬝ 1) ⬝ 0ᵀ + (1 ⬝ (-1) + 0 ⬝ 0) ⬝ (-1)ᵀ)
      ((1 ⬝ 0 + 0 ⬝ 1) ⬝ 1ᵀ + (1 ⬝ (-1) + 0 ⬝ 0) ⬝ 0ᵀ) =
    fromBlocks 0 (-1) 1 0
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
⊢ J l R ∈ symplecticGroup l R
rw [mem_iff, J, fromBlocks_multiply, fromBlocks_transpose, fromBlocks_multiply]
no goals
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
⊢ fromBlocks ((0 ⬝ 0 + (-1) ⬝ 1) ⬝ 0ᵀ + (0 ⬝ (-1) + (-1) ⬝ 0) ⬝ (-1)ᵀ)
      ((0 ⬝ 0 + (-1) ⬝ 1) ⬝ 1ᵀ + (0 ⬝ (-1) + (-1) ⬝ 0) ⬝ 0ᵀ) ((1 ⬝ 0 + 0 ⬝ 1) ⬝ 0ᵀ + (1 ⬝ (-1) + 0 ⬝ 0) ⬝ (-1)ᵀ)
      ((1 ⬝ 0 + 0 ⬝ 1) ⬝ 1ᵀ + (1 ⬝ (-1) + 0 ⬝ 0) ⬝ 0ᵀ) =
    fromBlocks 0 (-1) 1 0
simp