[GOAL]
l : Type u_1
R : Type u_2
inst✝¹ : DecidableEq l
inst✝ : CommRing R
⊢ (J l R)ᵀ = -J l R
[PROOFSTEP]
rw [J, fromBlocks_transpose, ← neg_one_smul R (fromBlocks _ _ _ _ : Matrix (l ⊕ l) (l ⊕ l) R), fromBlocks_smul,
  Matrix.transpose_zero, Matrix.transpose_one, transpose_neg]
[GOAL]
l : Type u_1
R : Type u_2
inst✝¹ : DecidableEq l
inst✝ : CommRing R
⊢ fromBlocks 0 1 (-1ᵀ) 0 = fromBlocks (-1 • 0) (-1 • -1) (-1 • 1) (-1 • 0)
[PROOFSTEP]
simp [fromBlocks]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ J l R * J l R = -1
[PROOFSTEP]
rw [J, fromBlocks_multiply]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ fromBlocks (0 * 0 + -1 * 1) (0 * -1 + -1 * 0) (1 * 0 + 0 * 1) (1 * -1 + 0 * 0) = -1
[PROOFSTEP]
simp only [Matrix.zero_mul, Matrix.neg_mul, zero_add, neg_zero, Matrix.one_mul, add_zero]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ fromBlocks (-1) 0 0 (-1) = -1
[PROOFSTEP]
rw [← neg_zero, ← Matrix.fromBlocks_neg, ← fromBlocks_one]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ (J l R)⁻¹ = -J l R
[PROOFSTEP]
refine' Matrix.inv_eq_right_inv _
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ J l R * -J l R = 1
[PROOFSTEP]
rw [Matrix.mul_neg, J_squared]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ - -1 = 1
[PROOFSTEP]
exact neg_neg 1
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ det (J l R) * det (J l R) = 1
[PROOFSTEP]
rw [← det_mul, J_squared, ← one_smul R (-1 : Matrix _ _ R), smul_neg, ← neg_smul, det_smul, Fintype.card_sum, det_one,
  mul_one]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ (-1) ^ (Fintype.card l + Fintype.card l) = 1
[PROOFSTEP]
apply Even.neg_one_pow
[GOAL]
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ Even (Fintype.card l + Fintype.card l)
[PROOFSTEP]
exact even_add_self _
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
a b : Matrix (l ⊕ l) (l ⊕ l) R
ha : a ∈ {A | A * J l R * Aᵀ = J l R}
hb : b ∈ {A | A * J l R * Aᵀ = J l R}
⊢ a * b ∈ {A | A * J l R * Aᵀ = J l R}
[PROOFSTEP]
simp only [Set.mem_setOf_eq, transpose_mul] at *
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
a b : Matrix (l ⊕ l) (l ⊕ l) R
ha : a * J l R * aᵀ = J l R
hb : b * J l R * bᵀ = J l R
⊢ a * b * J l R * (bᵀ * aᵀ) = J l R
[PROOFSTEP]
rw [← Matrix.mul_assoc, a.mul_assoc, a.mul_assoc, hb]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
a b : Matrix (l ⊕ l) (l ⊕ l) R
ha : a * J l R * aᵀ = J l R
hb : b * J l R * bᵀ = J l R
⊢ a * J l R * aᵀ = J l R
[PROOFSTEP]
exact ha
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ 1 ∈
    { carrier := {A | A * J l R * Aᵀ = J l R},
        mul_mem' :=
          (_ :
            ∀ {a b : Matrix (l ⊕ l) (l ⊕ l) R},
              a ∈ {A | A * J l R * Aᵀ = J l R} →
                b ∈ {A | A * J l R * Aᵀ = J l R} → a * b ∈ {A | A * J l R * Aᵀ = J l R}) }.carrier
[PROOFSTEP]
simp
[GOAL]
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 ∈ symplecticGroup l R ↔ A * J l R * Aᵀ = J l R
[PROOFSTEP]
simp [symplecticGroup]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
⊢ J l R ∈ symplecticGroup l R
[PROOFSTEP]
rw [mem_iff, J, fromBlocks_multiply, fromBlocks_transpose, fromBlocks_multiply]
[GOAL]
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
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
h : A ∈ symplecticGroup l R
⊢ -A ∈ symplecticGroup l R
[PROOFSTEP]
rw [mem_iff] at h ⊢
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
h : A * J l R * Aᵀ = J l R
⊢ -A * J l R * (-A)ᵀ = J l R
[PROOFSTEP]
simp [h]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ IsUnit (det A)
[PROOFSTEP]
rw [isUnit_iff_exists_inv]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ ∃ b, det A * b = 1
[PROOFSTEP]
use A.det
[GOAL]
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ det A * det A = 1
[PROOFSTEP]
refine' (isUnit_det_J l R).mul_left_cancel _
[GOAL]
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ det (J l R) * (det A * det A) = det (J l R) * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ det (J l R) * (det A * det A) = det (J l R)
[PROOFSTEP]
rw [mem_iff] at hA 
[GOAL]
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
⊢ det (J l R) * (det A * det A) = det (J l R)
[PROOFSTEP]
apply_fun det at hA 
[GOAL]
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : det (A * J l R * Aᵀ) = det (J l R)
⊢ det (J l R) * (det A * det A) = det (J l R)
[PROOFSTEP]
simp only [det_mul, det_transpose] at hA 
[GOAL]
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : det A * det (J l R) * det A = det (J l R)
⊢ det (J l R) * (det A * det A) = det (J l R)
[PROOFSTEP]
rw [mul_comm A.det, mul_assoc] at hA 
[GOAL]
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : det (J l R) * (det A * det A) = det (J l R)
⊢ det (J l R) * (det A * det A) = det (J l R)
[PROOFSTEP]
exact hA
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ Aᵀ ∈ symplecticGroup l R
[PROOFSTEP]
rw [mem_iff] at hA ⊢
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
⊢ Aᵀ * J l R * Aᵀᵀ = J l R
[PROOFSTEP]
rw [transpose_transpose]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
⊢ Aᵀ * J l R * A = J l R
[PROOFSTEP]
have huA := symplectic_det hA
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit (det A)
⊢ Aᵀ * J l R * A = J l R
[PROOFSTEP]
have huAT : IsUnit Aᵀ.det := by
  rw [Matrix.det_transpose]
  exact huA
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit (det A)
⊢ IsUnit (det Aᵀ)
[PROOFSTEP]
rw [Matrix.det_transpose]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit (det A)
⊢ IsUnit (det A)
[PROOFSTEP]
exact huA
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit (det A)
huAT : IsUnit (det Aᵀ)
⊢ Aᵀ * J l R * A = J l R
[PROOFSTEP]
calc
  Aᵀ * J l R * A = (-Aᵀ) * (J l R)⁻¹ * A := by
    rw [J_inv]
    simp
  _ = (-Aᵀ) * (A * J l R * Aᵀ)⁻¹ * A := by rw [hA]
  _ = -(Aᵀ * (Aᵀ⁻¹ * (J l R)⁻¹)) * A⁻¹ * A := by simp only [Matrix.mul_inv_rev, Matrix.mul_assoc, Matrix.neg_mul]
  _ = -(J l R)⁻¹ := by rw [mul_nonsing_inv_cancel_left _ _ huAT, nonsing_inv_mul_cancel_right _ _ huA]
  _ = J l R := by simp [J_inv]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit (det A)
huAT : IsUnit (det Aᵀ)
⊢ Aᵀ * J l R * A = -Aᵀ * (J l R)⁻¹ * A
[PROOFSTEP]
rw [J_inv]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit (det A)
huAT : IsUnit (det Aᵀ)
⊢ Aᵀ * J l R * A = -Aᵀ * -J l R * A
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit (det A)
huAT : IsUnit (det Aᵀ)
⊢ -Aᵀ * (J l R)⁻¹ * A = -Aᵀ * (A * J l R * Aᵀ)⁻¹ * A
[PROOFSTEP]
rw [hA]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit (det A)
huAT : IsUnit (det Aᵀ)
⊢ -Aᵀ * (A * J l R * Aᵀ)⁻¹ * A = -(Aᵀ * (Aᵀ⁻¹ * (J l R)⁻¹)) * A⁻¹ * A
[PROOFSTEP]
simp only [Matrix.mul_inv_rev, Matrix.mul_assoc, Matrix.neg_mul]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit (det A)
huAT : IsUnit (det Aᵀ)
⊢ -(Aᵀ * (Aᵀ⁻¹ * (J l R)⁻¹)) * A⁻¹ * A = -(J l R)⁻¹
[PROOFSTEP]
rw [mul_nonsing_inv_cancel_left _ _ huAT, nonsing_inv_mul_cancel_right _ _ huA]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit (det A)
huAT : IsUnit (det Aᵀ)
⊢ -(J l R)⁻¹ = J l R
[PROOFSTEP]
simp [J_inv]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : Aᵀ ∈ symplecticGroup l R
⊢ A ∈ symplecticGroup l R
[PROOFSTEP]
simpa using transpose_mem hA
[GOAL]
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 ∈ symplecticGroup l R ↔ Aᵀ * J l R * A = J l R
[PROOFSTEP]
rw [← transpose_mem_iff, mem_iff, transpose_transpose]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -(J l R * Aᵀ * J l R * A) = -J l R * (Aᵀ * J l R * A)
[PROOFSTEP]
simp only [Matrix.mul_assoc, Matrix.neg_mul]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -J l R * (Aᵀ * J l R * A) = -J l R * J l R
[PROOFSTEP]
rw [mem_iff'] at hA 
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : Aᵀ * J l R * A = J l R
⊢ -J l R * (Aᵀ * J l R * A) = -J l R * J l R
[PROOFSTEP]
rw [hA]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -J l R * J l R = -1 • (J l R * J l R)
[PROOFSTEP]
simp only [Matrix.neg_mul, neg_smul, one_smul]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -1 • (J l R * J l R) = -1 • -1
[PROOFSTEP]
rw [J_squared]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -1 • -1 = 1
[PROOFSTEP]
simp only [neg_smul_neg, one_smul]
[GOAL]
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)⁻¹
[PROOFSTEP]
refine' (coe_inv A).trans (inv_eq_left_inv _).symm
[GOAL]
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
[PROOFSTEP]
simp [inv_left_mul_aux, coe_inv]
[GOAL]
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
[PROOFSTEP]
simp only [Matrix.neg_mul, inv_left_mul_aux hA]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A✝ : Matrix (l ⊕ l) (l ⊕ l) R
src✝¹ : Inv { x // x ∈ symplecticGroup l R } := hasInv
src✝ : Monoid { x // x ∈ symplecticGroup l R } := Submonoid.toMonoid (symplecticGroup l R)
A : { x // x ∈ symplecticGroup l R }
⊢ A⁻¹ * A = 1
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case a
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A✝ : Matrix (l ⊕ l) (l ⊕ l) R
src✝¹ : Inv { x // x ∈ symplecticGroup l R } := hasInv
src✝ : Monoid { x // x ∈ symplecticGroup l R } := Submonoid.toMonoid (symplecticGroup l R)
A : { x // x ∈ symplecticGroup l R }
⊢ ↑(A⁻¹ * A) = ↑1
[PROOFSTEP]
simp only [Submonoid.coe_one, Submonoid.coe_mul, Matrix.neg_mul, coe_inv]
[GOAL]
case a
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A✝ : Matrix (l ⊕ l) (l ⊕ l) R
src✝¹ : Inv { x // x ∈ symplecticGroup l R } := hasInv
src✝ : Monoid { x // x ∈ symplecticGroup l R } := Submonoid.toMonoid (symplecticGroup l R)
A : { x // x ∈ symplecticGroup l R }
⊢ -(J l R * (↑A)ᵀ * J l R * ↑A) = 1
[PROOFSTEP]
exact inv_left_mul_aux A.2
