awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basis
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
inst_4 : Free R M
let :
  ∀ (κ : Type uM) (b : Basis κ R M),
    Module.rank R (SymmetricAlgebra R M) = Cardinal.lift.{uR, uM} (max (Module.rank R M) ℵ₀)
⊢ Module.rank R (SymmetricAlgebra R M) = Cardinal.lift.{uR, uM} (max (Module.rank R M) ℵ₀)

Tactic:
let ⟨⟨κ, b⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basis
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
inst_4 : Free R M
κ : Type uM
b : Basis κ R M
⊢ Nonempty κ

Tactic:
have : Nonempty κ := Basis.index_nonempty b
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basis
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
inst_4 : Free R M
κ : Type uM
b : Basis κ R M
this : Nonempty κ
⊢ Nontrivial R

Tactic:
have : Nontrivial R := Module.nontrivial R M
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basis
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
inst_4 : Free R M
κ : Type uM
b : Basis κ R M
this_1 : Nonempty κ
this : Nontrivial R
rw : Module.rank R (MvPolynomial κ R) = Cardinal.lift.{uR, uM} (max (Module.rank R M) ℵ₀)
rw₁ : Cardinal.lift.{uR, uM} #(κ →₀ ℕ) = Cardinal.lift.{uR, uM} (max (Module.rank R M) ℵ₀)
rw₂ : Cardinal.lift.{uR, uM} (max #κ ℵ₀) = Cardinal.lift.{uR, uM} (max (Module.rank R M) ℵ₀)
rw₃ rw₄ : Cardinal.lift.{uR, uM} (max (Module.rank R M) ℵ₀) = Cardinal.lift.{uR, uM} (max (Module.rank R M) ℵ₀)
⊢ Module.rank R (SymmetricAlgebra R M) = Cardinal.lift.{uR, uM} (max (Module.rank R M) ℵ₀)

Tactic:
rw [(equivMvPolynomial b).toLinearEquiv.rank_eq, MvPolynomial.rank_eq_lift,
    Cardinal.mk_finsupp_nat, Basis.mk_eq_rank'' b]

Premises used: Cardinal.mk_finsupp_nat, LinearEquiv.rank_eq, AlgEquiv.toLinearEquiv, SymmetricAlgebra.equivMvPolynomial, Module.Basis.mk_eq_rank'', MvPolynomial.rank_eq_lift
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
rw :
  fromBlocks 0 1 (-1ᵀ) 0 =
    fromBlocks (HSMul.hSMul (α := R) (β := Matrix l l R) (-1) 0) (HSMul.hSMul (α := R) (β := Matrix l l R) (-1) (-1))
      (HSMul.hSMul (α := R) (β := Matrix l l R) (-1) 1) (HSMul.hSMul (α := R) (β := Matrix l l R) (-1) 0)
⊢ (J l R)ᵀ = -J l R

Tactic:
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]

Premises used: Matrix.fromBlocks, neg_one_smul, Matrix.transpose_zero, Matrix.transpose_neg, Matrix.fromBlocks_transpose, Matrix.transpose_one, Matrix.J, Matrix.fromBlocks_smul
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
⊢ fromBlocks 0 1 (-1ᵀ) 0 =
    fromBlocks (HSMul.hSMul (α := R) (β := Matrix l l R) (-1) 0) (HSMul.hSMul (α := R) (β := Matrix l l R) (-1) (-1))
      (HSMul.hSMul (α := R) (β := Matrix l l R) (-1) 1) (HSMul.hSMul (α := R) (β := Matrix l l R) (-1) 0)

Tactic:
simp [fromBlocks]

Premises used: Matrix.fromBlocks
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
rw :
  fromBlocks (HMul.hMul (α := Matrix l l R) 0 0 + HMul.hMul (α := Matrix l l R) (-1) 1)
      (HMul.hMul (α := Matrix l l R) 0 (-1) + HMul.hMul (α := Matrix l l R) (-1) 0)
      (HMul.hMul (α := Matrix l l R) 1 0 + HMul.hMul (α := Matrix l l R) 0 1)
      (HMul.hMul (α := Matrix l l R) 1 (-1) + HMul.hMul (α := Matrix l l R) 0 0) =
    -1
⊢ J l R * J l R = -1

Tactic:
rw [J, fromBlocks_multiply]

Premises used: Matrix.J, Matrix.fromBlocks_multiply
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
simp : Eq (α := Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R) (fromBlocks (-1) 0 0 (-1)) (-1)
⊢ fromBlocks (HMul.hMul (α := Matrix l l R) 0 0 + HMul.hMul (α := Matrix l l R) (-1) 1)
      (HMul.hMul (α := Matrix l l R) 0 (-1) + HMul.hMul (α := Matrix l l R) (-1) 0)
      (HMul.hMul (α := Matrix l l R) 1 0 + HMul.hMul (α := Matrix l l R) 0 1)
      (HMul.hMul (α := Matrix l l R) 1 (-1) + HMul.hMul (α := Matrix l l R) 0 0) =
    -1

Tactic:
simp only [Matrix.zero_mul, Matrix.neg_mul, zero_add, neg_zero, Matrix.one_mul, add_zero]

Premises used: zero_add, Matrix.zero_mul, Matrix.neg_mul, add_zero, neg_zero, Matrix.one_mul
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
rw : Eq (α := Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R) (fromBlocks (-1) (-0) (-0) (-1)) (-1)
rw₁ : Eq (α := Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R) (-fromBlocks 1 0 0 1) (-1)
rw₂ rw₃ : Eq (α := Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R) (-fromBlocks 1 0 0 1) (-fromBlocks 1 0 0 1)
⊢ Eq (α := Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R) (fromBlocks (-1) 0 0 (-1)) (-1)

Tactic:
rw [← neg_zero, ← Matrix.fromBlocks_neg, ← fromBlocks_one]

Premises used: Matrix.fromBlocks_neg, Matrix.fromBlocks_one, neg_zero
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
⊢ (J l R)⁻¹ = -J l R

Tactic:
Matrix.inv_eq_right_inv ?_

Premises used: Matrix.inv_eq_right_inv
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
refine : J l R * -J l R = 1
⊢ (J l R)⁻¹ = -J l R

Tactic:
refine Matrix.inv_eq_right_inv ?_

Premises used: Matrix.inv_eq_right_inv
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
rw : Eq (α := Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R) (- -1) 1
⊢ J l R * -J l R = 1

Tactic:
rw [Matrix.mul_neg, J_squared]

Premises used: Matrix.mul_neg, Matrix.J_squared
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
⊢ Eq (α := Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R) (- -1) 1

Tactic:
neg_neg 1

Premises used: neg_neg, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
⊢ Eq (α := Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R) (- -1) 1

Tactic:
exact neg_neg 1

Premises used: neg_neg, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
rw : HPow.hPow (α := R) (-1) (Fintype.card l + Fintype.card l) = 1
⊢ (J l R).det * (J l R).det = 1

Tactic:
rw [← det_mul, J_squared, ← one_smul R (-1 : Matrix _ _ R), smul_neg, ← neg_smul, det_smul,
    Fintype.card_sum, det_one, mul_one]

Premises used: neg_smul, Matrix.det_smul, Matrix.J_squared, smul_neg, one_smul, Matrix.det_mul, Matrix.det_one, mul_one, OfNat.ofNat, Neg.neg, Fintype.card_sum
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
h : Even (Fintype.card l + Fintype.card l)
⊢ HPow.hPow (α := R) (-1) (Fintype.card l + Fintype.card l) = 1

Tactic:
apply Even.neg_one_pow

Premises used: Even.neg_one_pow
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
⊢ Even (Fintype.card l + Fintype.card l)

Tactic:
Even.add_self _

Premises used: Even.add_self
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
⊢ Even (Fintype.card l + Fintype.card l)

Tactic:
exact Even.add_self _

Premises used: Even.add_self
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
⊢ IsUnit (J l R).det

Tactic:
isUnit_iff_exists_inv.mpr ⟨det (J l R), J_det_mul_J_det _ _⟩

Premises used: Iff.mpr, isUnit_iff_exists_inv, Matrix.J, Exists.intro, Matrix.J_det_mul_J_det, Matrix.det
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
a b : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
ha :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R))
    {A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R | A * J l R * Aᵀ = J l R} a
hb :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R))
    {A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R | A * J l R * Aᵀ = J l R} b
simp : a * b * J l R * (bᵀ * aᵀ) = J l R
⊢ Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R))
    {A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R | A * J l R * Aᵀ = J l R} (a * b)

Tactic:
simp only [Set.mem_setOf_eq, transpose_mul] at *

Premises used: Matrix.transpose_mul, Set.mem_setOf_eq
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
a b : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
ha : a * J l R * aᵀ = J l R
hb : b * J l R * bᵀ = J l R
rw : a * J l R * aᵀ = J l R
⊢ a * b * J l R * (bᵀ * aᵀ) = J l R

Tactic:
rw [← Matrix.mul_assoc, a.mul_assoc, a.mul_assoc, hb]

Premises used: Matrix.mul_assoc
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
a b : Matrix.{u_1, u_1, u_2} (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

Tactic:
ha
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
a b : Matrix.{u_1, u_1, u_2} (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

Tactic:
exact ha
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
⊢ Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R))
    {A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R | A * J l R * Aᵀ = J l R} 1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
⊢ Membership.mem (γ := Submonoid (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R)) (symplecticGroup l R) A ↔
    A * J l R * Aᵀ = J l R

Tactic:
simp [symplecticGroup]

Premises used: Matrix.symplecticGroup
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
rw :
  fromBlocks
      ((HMul.hMul (α := Matrix l l R) 0 0 + HMul.hMul (α := Matrix l l R) (-1) 1) * 0ᵀ +
        (HMul.hMul (α := Matrix l l R) 0 (-1) + HMul.hMul (α := Matrix l l R) (-1) 0) * (-1)ᵀ)
      ((HMul.hMul (α := Matrix l l R) 0 0 + HMul.hMul (α := Matrix l l R) (-1) 1) * 1ᵀ +
        (HMul.hMul (α := Matrix l l R) 0 (-1) + HMul.hMul (α := Matrix l l R) (-1) 0) * 0ᵀ)
      ((HMul.hMul (α := Matrix l l R) 1 0 + HMul.hMul (α := Matrix l l R) 0 1) * 0ᵀ +
        (HMul.hMul (α := Matrix l l R) 1 (-1) + HMul.hMul (α := Matrix l l R) 0 0) * (-1)ᵀ)
      ((HMul.hMul (α := Matrix l l R) 1 0 + HMul.hMul (α := Matrix l l R) 0 1) * 1ᵀ +
        (HMul.hMul (α := Matrix l l R) 1 (-1) + HMul.hMul (α := Matrix l l R) 0 0) * 0ᵀ) =
    fromBlocks 0 (-1) 1 0
⊢ Membership.mem (γ := Submonoid (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R)) (symplecticGroup l R) (J l R)

Tactic:
rw [mem_iff, J, fromBlocks_multiply, fromBlocks_transpose, fromBlocks_multiply]

Premises used: SymplecticGroup.mem_iff, Matrix.fromBlocks_transpose, Matrix.J, Matrix.fromBlocks_multiply
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
⊢ fromBlocks
      ((HMul.hMul (α := Matrix l l R) 0 0 + HMul.hMul (α := Matrix l l R) (-1) 1) * 0ᵀ +
        (HMul.hMul (α := Matrix l l R) 0 (-1) + HMul.hMul (α := Matrix l l R) (-1) 0) * (-1)ᵀ)
      ((HMul.hMul (α := Matrix l l R) 0 0 + HMul.hMul (α := Matrix l l R) (-1) 1) * 1ᵀ +
        (HMul.hMul (α := Matrix l l R) 0 (-1) + HMul.hMul (α := Matrix l l R) (-1) 0) * 0ᵀ)
      ((HMul.hMul (α := Matrix l l R) 1 0 + HMul.hMul (α := Matrix l l R) 0 1) * 0ᵀ +
        (HMul.hMul (α := Matrix l l R) 1 (-1) + HMul.hMul (α := Matrix l l R) 0 0) * (-1)ᵀ)
      ((HMul.hMul (α := Matrix l l R) 1 0 + HMul.hMul (α := Matrix l l R) 0 1) * 1ᵀ +
        (HMul.hMul (α := Matrix l l R) 1 (-1) + HMul.hMul (α := Matrix l l R) 0 0) * 0ᵀ) =
    fromBlocks 0 (-1) 1 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
⊢ (↑(symJ l R) : Matrix (l ⊕ l) (l ⊕ l) R) = J l R

Tactic:
rfl

Premises used: Matrix.fromBlocks, Matrix.J, rfl
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
h : Membership.mem (γ := Submonoid (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R)) (symplecticGroup l R) A
⊢ A * J l R * Aᵀ = J l R

Tactic:
rw [mem_iff] at h ⊢

Premises used: SymplecticGroup.mem_iff
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
h : A * J l R * Aᵀ = J l R
⊢ -A * J l R * (-A)ᵀ = J l R

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : Membership.mem (γ := Submonoid (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R)) (symplecticGroup l R) A
rw : ∃ (b : R), A.det * b = 1
⊢ IsUnit A.det

Tactic:
rw [isUnit_iff_exists_inv]

Premises used: isUnit_iff_exists_inv
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : Membership.mem (γ := Submonoid (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R)) (symplecticGroup l R) A
h : A.det * A.det = 1
⊢ ∃ (b : R), A.det * b = 1

Tactic:
use A.det

Premises used: Matrix.det
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : Membership.mem (γ := Submonoid (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R)) (symplecticGroup l R) A
⊢ A.det * A.det = 1

Tactic:
(isUnit_det_J l R).mul_left_cancel ?_

Premises used: Matrix.isUnit_det_J, IsUnit.mul_left_cancel
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : Membership.mem (γ := Submonoid (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R)) (symplecticGroup l R) A
h : (J l R).det * (A.det * A.det) = (J l R).det * 1
⊢ A.det * A.det = 1

Tactic:
refine (isUnit_det_J l R).mul_left_cancel ?_

Premises used: Matrix.isUnit_det_J, IsUnit.mul_left_cancel
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : Membership.mem (γ := Submonoid (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R)) (symplecticGroup l R) A
h : (J l R).det * (A.det * A.det) = (J l R).det
⊢ (J l R).det * (A.det * A.det) = (J l R).det * 1

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : Membership.mem (γ := Submonoid (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R)) (symplecticGroup l R) A
⊢ A * J l R * Aᵀ = J l R

Tactic:
rw [mem_iff] at hA

Premises used: SymplecticGroup.mem_iff
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
⊢ (A * J l R * Aᵀ).det = (J l R).det

Tactic:
apply_fun det at hA

Premises used: Matrix.det
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : (A * J l R * Aᵀ).det = (J l R).det
⊢ A.det * (J l R).det * A.det = (J l R).det

Tactic:
simp only [det_mul, det_transpose] at hA

Premises used: Matrix.det_transpose, Matrix.det_mul
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : A.det * (J l R).det * A.det = (J l R).det
⊢ (J l R).det * (A.det * A.det) = (J l R).det

Tactic:
rw [mul_comm A.det, mul_assoc] at hA

Premises used: mul_assoc, mul_comm, Matrix.det
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : (J l R).det * (A.det * A.det) = (J l R).det
⊢ (J l R).det * (A.det * A.det) = (J l R).det

Tactic:
hA
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : (J l R).det * (A.det * A.det) = (J l R).det
⊢ (J l R).det * (A.det * A.det) = (J l R).det

Tactic:
exact hA
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : Membership.mem (γ := Submonoid (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R)) (symplecticGroup l R) A
⊢ A * J l R * Aᵀ = J l R

Tactic:
rw [mem_iff] at hA ⊢

Premises used: SymplecticGroup.mem_iff
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
rw : Aᵀ * J l R * A = J l R
⊢ Aᵀ * J l R * Aᵀᵀ = J l R

Tactic:
rw [transpose_transpose]

Premises used: Matrix.transpose_transpose
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
⊢ IsUnit A.det

Tactic:
have huA := symplectic_det hA
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA rw : IsUnit A.det
⊢ IsUnit Aᵀ.det

Tactic:
rw [Matrix.det_transpose]

Premises used: Matrix.det_transpose
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit A.det
⊢ IsUnit A.det

Tactic:
huA
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit A.det
⊢ IsUnit A.det

Tactic:
exact huA
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit A.det
⊢ IsUnit Aᵀ.det

Tactic:
have huAT : IsUnit Aᵀ.det := by
    rw [Matrix.det_transpose]
    exact huA
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit A.det
huAT : IsUnit Aᵀ.det
rw : Aᵀ * J l R * A = -Aᵀ * -J l R * A
⊢ Aᵀ * J l R * A = -Aᵀ * (J l R)⁻¹ * A

Tactic:
rw [J_inv]

Premises used: Matrix.J_inv
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit A.det
huAT : IsUnit Aᵀ.det
⊢ Aᵀ * J l R * A = -Aᵀ * -J l R * A

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit A.det
huAT : IsUnit Aᵀ.det
rw rw₁ : -Aᵀ * (J l R)⁻¹ * A = -Aᵀ * (J l R)⁻¹ * A
⊢ -Aᵀ * (J l R)⁻¹ * A = -Aᵀ * (A * J l R * Aᵀ)⁻¹ * A

Tactic:
rw [hA]
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit A.det
huAT : IsUnit Aᵀ.det
⊢ -Aᵀ * (A * J l R * Aᵀ)⁻¹ * A = -(Aᵀ * (Aᵀ⁻¹ * (J l R)⁻¹)) * A⁻¹ * A

Tactic:
simp only [Matrix.mul_inv_rev, Matrix.mul_assoc, Matrix.neg_mul]

Premises used: Matrix.mul_assoc, Matrix.mul_inv_rev, Matrix.neg_mul
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit A.det
huAT : IsUnit Aᵀ.det
rw : -(J l R)⁻¹ * A⁻¹ * A = -(J l R)⁻¹
rw₁ rw₂ : -(J l R)⁻¹ = -(J l R)⁻¹
⊢ -(Aᵀ * (Aᵀ⁻¹ * (J l R)⁻¹)) * A⁻¹ * A = -(J l R)⁻¹

Tactic:
rw [mul_nonsing_inv_cancel_left _ _ huAT, nonsing_inv_mul_cancel_right _ _ huA]

Premises used: Matrix.nonsing_inv_mul_cancel_right, Matrix.mul_nonsing_inv_cancel_left
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit A.det
huAT : IsUnit Aᵀ.det
⊢ -(J l R)⁻¹ = J l R

Tactic:
simp [J_inv]

Premises used: Matrix.J_inv
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : A * Matrix.J l R * Aᵀ = Matrix.J l R
huA : IsUnit A.det
huAT : IsUnit Aᵀ.det
J : Aᵀ * Matrix.J l R * A = -Aᵀ * (Matrix.J l R)⁻¹ * A
J₁ : -Aᵀ * (Matrix.J l R)⁻¹ * A = -Aᵀ * (A * Matrix.J l R * Aᵀ)⁻¹ * A
J₂ : -Aᵀ * (A * Matrix.J l R * Aᵀ)⁻¹ * A = -(Aᵀ * (Aᵀ⁻¹ * (Matrix.J l R)⁻¹)) * A⁻¹ * A
J₃ : -(Aᵀ * (Aᵀ⁻¹ * (Matrix.J l R)⁻¹)) * A⁻¹ * A = -(Matrix.J l R)⁻¹
J₄ : -(Matrix.J l R)⁻¹ = Matrix.J l R
⊢ Aᵀ * Matrix.J l R * A = Matrix.J l R

Tactic:
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]

Premises used: HMul.hMul, Inv.inv, Matrix.transpose, Matrix.J, Neg.neg
-- Module: Mathlib.LinearAlgebra.SymplecticGroup
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
A : Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R
hA : Membership.mem (γ := Submonoid (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R)) (symplecticGroup l R) Aᵀ
⊢ Membership.mem (γ := Submonoid (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R)) (symplecticGroup l R) A

Tactic:
simpa using transpose_mem hA

Premises used: SymplecticGroup.transpose_mem