awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basis (goal)
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
⊢ Module.rank R (SymmetricAlgebra R M) = Cardinal.lift.{uR, uM} (max (Module.rank R M) ℵ₀)
have rw : Module.rank R (MvPolynomial κ R) = 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basis (goal)
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) ℵ₀)
⊢ Module.rank R (SymmetricAlgebra R M) = Cardinal.lift.{uR, uM} (max (Module.rank R M) ℵ₀)
have rw₁ : Cardinal.lift.{uR, uM} #(κ →₀ ℕ) = 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basis (goal)
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) ℵ₀)
⊢ Module.rank R (SymmetricAlgebra R M) = Cardinal.lift.{uR, uM} (max (Module.rank R M) ℵ₀)
have rw₂ : Cardinal.lift.{uR, uM} (max #κ ℵ₀) = 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basis (goal)
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) ℵ₀)
⊢ Module.rank R (SymmetricAlgebra R M) = Cardinal.lift.{uR, uM} (max (Module.rank R M) ℵ₀)
have rw₃ : Cardinal.lift.{uR, uM} (max (Module.rank 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
⊢ (J l R)ᵀ = -J l R
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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 = -1
have 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
Tactic: rw [J, fromBlocks_multiply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
⊢ 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
have simp : Eq (α := Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R) (fromBlocks (-1) 0 0 (-1)) (-1)
Tactic: simp only [Matrix.zero_mul, Matrix.neg_mul, zero_add, neg_zero, Matrix.one_mul, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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) (fromBlocks (-1) 0 0 (-1)) (-1)
have rw : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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)
⊢ Eq (α := Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R) (fromBlocks (-1) 0 0 (-1)) (-1)
have rw₁ : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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)
⊢ Eq (α := Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R) (fromBlocks (-1) 0 0 (-1)) (-1)
have rw₂ : Eq (α := Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R) (-fromBlocks 1 0 0 1) (-fromBlocks 1 0 0 1)
Tactic: rw [← neg_zero, ← Matrix.fromBlocks_neg, ← fromBlocks_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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
have refine : J l R * -J l R = 1
Tactic: refine Matrix.inv_eq_right_inv ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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 = 1
have rw : Eq (α := Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R) (- -1) 1
Tactic: rw [Matrix.mul_neg, J_squared]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
⊢ (J l R).det * (J l R).det = 1
have rw : HPow.hPow (α := R) (-1) (Fintype.card l + Fintype.card l) = 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
⊢ HPow.hPow (α := R) (-1) (Fintype.card l + Fintype.card l) = 1
have h : Even (Fintype.card l + Fintype.card l)
Tactic: apply Even.neg_one_pow
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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
⊢ 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)
have simp : a * b * J l R * (bᵀ * aᵀ) = J l R
Tactic: simp only [Set.mem_setOf_eq, transpose_mul] at *
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
Goal:
l : Type u_1
R : Type u_2
inst : DecidableEq l
inst_1 : Fintype l
inst_2 : CommRing R
⊢ Membership.mem (γ := Submonoid (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R)) (symplecticGroup l R) (J l R)
have 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
Tactic: rw [mem_iff, J, fromBlocks_multiply, fromBlocks_transpose, fromBlocks_multiply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (hypothesis)
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
⊢ Membership.mem (γ := Submonoid (Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R)) (symplecticGroup l R) (-A)
have h₁ : A * J l R * Aᵀ = J l R
Tactic: rw [mem_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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
⊢ IsUnit A.det
have rw : ∃ (b : R), A.det * b = 1
Tactic: rw [isUnit_iff_exists_inv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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
⊢ ∃ (b : R), A.det * b = 1
have h : A.det * A.det = 1
Tactic: use A.det
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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
have h : (J l R).det * (A.det * A.det) = (J l R).det * 1
Tactic: refine (isUnit_det_J l R).mul_left_cancel ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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
⊢ (J l R).det * (A.det * A.det) = (J l R).det * 1
have h : (J l R).det * (A.det * A.det) = (J l R).det
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (hypothesis)
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
⊢ (J l R).det * (A.det * A.det) = (J l R).det
have hA₁ : A * J l R * Aᵀ = J l R
Tactic: rw [mem_iff] at hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (hypothesis)
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
⊢ (J l R).det * (A.det * A.det) = (J l R).det
have hA₁ : (A * J l R * Aᵀ).det = (J l R).det
Tactic: apply_fun det at hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (hypothesis)
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
⊢ (J l R).det * (A.det * A.det) = (J l R).det
have hA₁ : A.det * (J l R).det * A.det = (J l R).det
Tactic: simp only [det_mul, det_transpose] at hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (hypothesis)
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ᵀ
have hA₁ : A * J l R * Aᵀ = J l R
Tactic: rw [mem_iff] at hA ⊢
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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ᵀᵀ = J l R
have rw : Aᵀ * J l R * A = J l R
Tactic: rw [transpose_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (hypothesis)
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 = J l R
have huA : IsUnit A.det
Tactic: have huA := symplectic_det hA
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (hypothesis)
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
⊢ Aᵀ * J l R * A = J l R
have huAT : IsUnit Aᵀ.det
Tactic: have huAT : IsUnit Aᵀ.det := by
    rw [Matrix.det_transpose]
    exact huA
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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
have rw : Aᵀ * J l R * A = -Aᵀ * -J l R * A
Tactic: rw [J_inv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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ᵀ * (A * J l R * Aᵀ)⁻¹ * A
have rw : -Aᵀ * (J l R)⁻¹ * A = -Aᵀ * (J l R)⁻¹ * A
Tactic: rw [hA]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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 = -(J l R)⁻¹
have rw : -(J l R)⁻¹ * A⁻¹ * A = -(J l R)⁻¹
Tactic: rw [mul_nonsing_inv_cancel_left _ _ huAT, nonsing_inv_mul_cancel_right _ _ huA]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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)⁻¹
⊢ -(Aᵀ * (Aᵀ⁻¹ * (J l R)⁻¹)) * A⁻¹ * A = -(J l R)⁻¹
have rw₁ : -(J l R)⁻¹ = -(J l R)⁻¹
Tactic: rw [mul_nonsing_inv_cancel_left _ _ huAT, nonsing_inv_mul_cancel_right _ _ huA]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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 = J l R
have J : Aᵀ * J l R * A = -Aᵀ * (J l R)⁻¹ * A
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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
⊢ Aᵀ * Matrix.J l R * A = Matrix.J l R
have J₁ : -Aᵀ * (Matrix.J l R)⁻¹ * A = -Aᵀ * (A * Matrix.J l R * Aᵀ)⁻¹ * A
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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
⊢ Aᵀ * Matrix.J l R * A = Matrix.J l R
have J₂ : -Aᵀ * (A * Matrix.J l R * Aᵀ)⁻¹ * A = -(Aᵀ * (Aᵀ⁻¹ * (Matrix.J l R)⁻¹)) * A⁻¹ * A
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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
⊢ Aᵀ * Matrix.J l R * A = Matrix.J l R
have J₃ : -(Aᵀ * (Aᵀ⁻¹ * (Matrix.J l R)⁻¹)) * A⁻¹ * 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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)⁻¹
⊢ Aᵀ * Matrix.J l R * A = Matrix.J l R
have J₄ : -(Matrix.J l R)⁻¹ = 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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
have rw : 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 [← transpose_mem_iff, mem_iff, transpose_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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
rw :
  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
⊢ 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
have rw₁ : Aᵀ * J l R * Aᵀᵀ = J l R ↔ Aᵀ * J l R * A = J l R
Tactic: rw [← transpose_mem_iff, mem_iff, transpose_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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
rw :
  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
rw₁ : Aᵀ * J l R * Aᵀᵀ = J l R ↔ Aᵀ * J l R * A = J 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
have rw₂ : Aᵀ * J l R * A = J l R ↔ Aᵀ * J l R * A = J l R
Tactic: rw [← transpose_mem_iff, mem_iff, transpose_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (hypothesis)
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
⊢ -J l R * (Aᵀ * J l R * A) = -J l R * J l R
have hA₁ : Aᵀ * J l R * A = J l R
Tactic: rw [mem_iff'] at hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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
⊢ -J l R * (Aᵀ * J l R * A) = -J l R * J l R
have rw : -J l R * J l R = -J l R * J l R
Tactic: rw [hA]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymplecticGroup (goal)
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
⊢ HSMul.hSMul (α := R) (-1) (J l R * J l R) =
    HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R) (-1) (-1)
have rw : HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R) (-1) (-1) =
  HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (l ⊕ l) (l ⊕ l) R) (-1) (-1)
Tactic: rw [J_squared]