awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
hi : ((P.root : (a : ι) → M) i : M) ∉ allRoots P
this : P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0
⊢ P.IsOrthogonal i (short P) ∧ P.IsOrthogonal i (long P)
have this₁ : Module.IsReflexive R M
Tactic: have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
hi : ((P.root : (a : ι) → M) i : M) ∉ allRoots P
⊢ P.IsOrthogonal i (short P) ∧ P.IsOrthogonal i (long P)
have suffices : P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0
Tactic: suffices P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0 by
    have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
    simpa [isOrthogonal_iff_pairing_eq_zero, ← P.algebraMap_pairingIn ℤ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
hi : ((P.root : (a : ι) → M) i : M) ∉ allRoots P
⊢ P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0
have hi₁ : ¬(P.root : (a : ι) → M) i = longRoot P ∧
  ¬(P.root : (a : ι) → M) i = -longRoot P ∧
    ¬(P.root : (a : ι) → M) i = shortRoot P ∧
      ¬(P.root : (a : ι) → M) i = -shortRoot P ∧
        ¬(P.root : (a : ι) → M) i = shortAddLongRoot P ∧
          ¬(P.root : (a : ι) → M) i = -shortAddLongRoot P ∧
            ¬(P.root : (a : ι) → M) i = twoShortAddLongRoot P ∧
              ¬(P.root : (a : ι) → M) i = -twoShortAddLongRoot P ∧
                ¬(P.root : (a : ι) → M) i = threeShortAddLongRoot P ∧
                  ¬(P.root : (a : ι) → M) i = -threeShortAddLongRoot P ∧
                    ¬(P.root : (a : ι) → M) i = threeShortAddTwoLongRoot P ∧
                      ¬(P.root : (a : ι) → M) i = -threeShortAddTwoLongRoot P
Tactic: simp only [mem_cons, not_mem_nil, or_false, not_or] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
hi :
  ¬(P.root : (a : ι) → M) i = longRoot P ∧
    ¬(P.root : (a : ι) → M) i = -longRoot P ∧
      ¬(P.root : (a : ι) → M) i = shortRoot P ∧
        ¬(P.root : (a : ι) → M) i = -shortRoot P ∧
          ¬(P.root : (a : ι) → M) i = shortAddLongRoot P ∧
            ¬(P.root : (a : ι) → M) i = -shortAddLongRoot P ∧
              ¬(P.root : (a : ι) → M) i = twoShortAddLongRoot P ∧
                ¬(P.root : (a : ι) → M) i = -twoShortAddLongRoot P ∧
                  ¬(P.root : (a : ι) → M) i = threeShortAddLongRoot P ∧
                    ¬(P.root : (a : ι) → M) i = -threeShortAddLongRoot P ∧
                      ¬(P.root : (a : ι) → M) i = threeShortAddTwoLongRoot P ∧
                        ¬(P.root : (a : ι) → M) i = -threeShortAddTwoLongRoot P
⊢ P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0
have h₁ : ¬(P.root : (a : ι) → M) i = longRoot P
Tactic: obtain ⟨h₁, h₂, h₃, h₄, h₅, h₆, h₇, h₈, h₉, h₁₀, h₁₁, h₁₂⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
hi :
  ¬(P.root : (a : ι) → M) i = longRoot P ∧
    ¬(P.root : (a : ι) → M) i = -longRoot P ∧
      ¬(P.root : (a : ι) → M) i = shortRoot P ∧
        ¬(P.root : (a : ι) → M) i = -shortRoot P ∧
          ¬(P.root : (a : ι) → M) i = shortAddLongRoot P ∧
            ¬(P.root : (a : ι) → M) i = -shortAddLongRoot P ∧
              ¬(P.root : (a : ι) → M) i = twoShortAddLongRoot P ∧
                ¬(P.root : (a : ι) → M) i = -twoShortAddLongRoot P ∧
                  ¬(P.root : (a : ι) → M) i = threeShortAddLongRoot P ∧
                    ¬(P.root : (a : ι) → M) i = -threeShortAddLongRoot P ∧
                      ¬(P.root : (a : ι) → M) i = threeShortAddTwoLongRoot P ∧
                        ¬(P.root : (a : ι) → M) i = -threeShortAddTwoLongRoot P
h₁ : ¬(P.root : (a : ι) → M) i = longRoot P
⊢ P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0
have h₂ : ¬(P.root : (a : ι) → M) i = -longRoot P
Tactic: obtain ⟨h₁, h₂, h₃, h₄, h₅, h₆, h₇, h₈, h₉, h₁₀, h₁₁, h₁₂⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
hi :
  ¬(P.root : (a : ι) → M) i = longRoot P ∧
    ¬(P.root : (a : ι) → M) i = -longRoot P ∧
      ¬(P.root : (a : ι) → M) i = shortRoot P ∧
        ¬(P.root : (a : ι) → M) i = -shortRoot P ∧
          ¬(P.root : (a : ι) → M) i = shortAddLongRoot P ∧
            ¬(P.root : (a : ι) → M) i = -shortAddLongRoot P ∧
              ¬(P.root : (a : ι) → M) i = twoShortAddLongRoot P ∧
                ¬(P.root : (a : ι) → M) i = -twoShortAddLongRoot P ∧
                  ¬(P.root : (a : ι) → M) i = threeShortAddLongRoot P ∧
                    ¬(P.root : (a : ι) → M) i = -threeShortAddLongRoot P ∧
                      ¬(P.root : (a : ι) → M) i = threeShortAddTwoLongRoot P ∧
                        ¬(P.root : (a : ι) → M) i = -threeShortAddTwoLongRoot P
h₁ : ¬(P.root : (a : ι) → M) i = longRoot P
h₂ : ¬(P.root : (a : ι) → M) i = -longRoot P
⊢ P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0
have h₃ : ¬(P.root : (a : ι) → M) i = shortRoot P
Tactic: obtain ⟨h₁, h₂, h₃, h₄, h₅, h₆, h₇, h₈, h₉, h₁₀, h₁₁, h₁₂⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
hi :
  ¬(P.root : (a : ι) → M) i = longRoot P ∧
    ¬(P.root : (a : ι) → M) i = -longRoot P ∧
      ¬(P.root : (a : ι) → M) i = shortRoot P ∧
        ¬(P.root : (a : ι) → M) i = -shortRoot P ∧
          ¬(P.root : (a : ι) → M) i = shortAddLongRoot P ∧
            ¬(P.root : (a : ι) → M) i = -shortAddLongRoot P ∧
              ¬(P.root : (a : ι) → M) i = twoShortAddLongRoot P ∧
                ¬(P.root : (a : ι) → M) i = -twoShortAddLongRoot P ∧
                  ¬(P.root : (a : ι) → M) i = threeShortAddLongRoot P ∧
                    ¬(P.root : (a : ι) → M) i = -threeShortAddLongRoot P ∧
                      ¬(P.root : (a : ι) → M) i = threeShortAddTwoLongRoot P ∧
                        ¬(P.root : (a : ι) → M) i = -threeShortAddTwoLongRoot P
h₁ : ¬(P.root : (a : ι) → M) i = longRoot P
h₂ : ¬(P.root : (a : ι) → M) i = -longRoot P
h₃ : ¬(P.root : (a : ι) → M) i = shortRoot P
⊢ P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0
have h₄ : ¬(P.root : (a : ι) → M) i = -shortRoot P
Tactic: obtain ⟨h₁, h₂, h₃, h₄, h₅, h₆, h₇, h₈, h₉, h₁₀, h₁₁, h₁₂⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
hi :
  ¬(P.root : (a : ι) → M) i = longRoot P ∧
    ¬(P.root : (a : ι) → M) i = -longRoot P ∧
      ¬(P.root : (a : ι) → M) i = shortRoot P ∧
        ¬(P.root : (a : ι) → M) i = -shortRoot P ∧
          ¬(P.root : (a : ι) → M) i = shortAddLongRoot P ∧
            ¬(P.root : (a : ι) → M) i = -shortAddLongRoot P ∧
              ¬(P.root : (a : ι) → M) i = twoShortAddLongRoot P ∧
                ¬(P.root : (a : ι) → M) i = -twoShortAddLongRoot P ∧
                  ¬(P.root : (a : ι) → M) i = threeShortAddLongRoot P ∧
                    ¬(P.root : (a : ι) → M) i = -threeShortAddLongRoot P ∧
                      ¬(P.root : (a : ι) → M) i = threeShortAddTwoLongRoot P ∧
                        ¬(P.root : (a : ι) → M) i = -threeShortAddTwoLongRoot P
h₁ : ¬(P.root : (a : ι) → M) i = longRoot P
h₂ : ¬(P.root : (a : ι) → M) i = -longRoot P
h₃ : ¬(P.root : (a : ι) → M) i = shortRoot P
h₄ : ¬(P.root : (a : ι) → M) i = -shortRoot P
⊢ P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0
have h₅ : ¬(P.root : (a : ι) → M) i = shortAddLongRoot P
Tactic: obtain ⟨h₁, h₂, h₃, h₄, h₅, h₆, h₇, h₈, h₉, h₁₀, h₁₁, h₁₂⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
hi :
  ¬(P.root : (a : ι) → M) i = longRoot P ∧
    ¬(P.root : (a : ι) → M) i = -longRoot P ∧
      ¬(P.root : (a : ι) → M) i = shortRoot P ∧
        ¬(P.root : (a : ι) → M) i = -shortRoot P ∧
          ¬(P.root : (a : ι) → M) i = shortAddLongRoot P ∧
            ¬(P.root : (a : ι) → M) i = -shortAddLongRoot P ∧
              ¬(P.root : (a : ι) → M) i = twoShortAddLongRoot P ∧
                ¬(P.root : (a : ι) → M) i = -twoShortAddLongRoot P ∧
                  ¬(P.root : (a : ι) → M) i = threeShortAddLongRoot P ∧
                    ¬(P.root : (a : ι) → M) i = -threeShortAddLongRoot P ∧
                      ¬(P.root : (a : ι) → M) i = threeShortAddTwoLongRoot P ∧
                        ¬(P.root : (a : ι) → M) i = -threeShortAddTwoLongRoot P
h₁ : ¬(P.root : (a : ι) → M) i = longRoot P
h₂ : ¬(P.root : (a : ι) → M) i = -longRoot P
h₃ : ¬(P.root : (a : ι) → M) i = shortRoot P
h₄ : ¬(P.root : (a : ι) → M) i = -shortRoot P
h₅ : ¬(P.root : (a : ι) → M) i = shortAddLongRoot P
⊢ P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0
have h₆ : ¬(P.root : (a : ι) → M) i = -shortAddLongRoot P
Tactic: obtain ⟨h₁, h₂, h₃, h₄, h₅, h₆, h₇, h₈, h₉, h₁₀, h₁₁, h₁₂⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
hi :
  ¬(P.root : (a : ι) → M) i = longRoot P ∧
    ¬(P.root : (a : ι) → M) i = -longRoot P ∧
      ¬(P.root : (a : ι) → M) i = shortRoot P ∧
        ¬(P.root : (a : ι) → M) i = -shortRoot P ∧
          ¬(P.root : (a : ι) → M) i = shortAddLongRoot P ∧
            ¬(P.root : (a : ι) → M) i = -shortAddLongRoot P ∧
              ¬(P.root : (a : ι) → M) i = twoShortAddLongRoot P ∧
                ¬(P.root : (a : ι) → M) i = -twoShortAddLongRoot P ∧
                  ¬(P.root : (a : ι) → M) i = threeShortAddLongRoot P ∧
                    ¬(P.root : (a : ι) → M) i = -threeShortAddLongRoot P ∧
                      ¬(P.root : (a : ι) → M) i = threeShortAddTwoLongRoot P ∧
                        ¬(P.root : (a : ι) → M) i = -threeShortAddTwoLongRoot P
h₁ : ¬(P.root : (a : ι) → M) i = longRoot P
h₂ : ¬(P.root : (a : ι) → M) i = -longRoot P
h₃ : ¬(P.root : (a : ι) → M) i = shortRoot P
h₄ : ¬(P.root : (a : ι) → M) i = -shortRoot P
h₅ : ¬(P.root : (a : ι) → M) i = shortAddLongRoot P
h₆ : ¬(P.root : (a : ι) → M) i = -shortAddLongRoot P
⊢ P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0
have h₇ : ¬(P.root : (a : ι) → M) i = twoShortAddLongRoot P
Tactic: obtain ⟨h₁, h₂, h₃, h₄, h₅, h₆, h₇, h₈, h₉, h₁₀, h₁₁, h₁₂⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
hi :
  ¬(P.root : (a : ι) → M) i = longRoot P ∧
    ¬(P.root : (a : ι) → M) i = -longRoot P ∧
      ¬(P.root : (a : ι) → M) i = shortRoot P ∧
        ¬(P.root : (a : ι) → M) i = -shortRoot P ∧
          ¬(P.root : (a : ι) → M) i = shortAddLongRoot P ∧
            ¬(P.root : (a : ι) → M) i = -shortAddLongRoot P ∧
              ¬(P.root : (a : ι) → M) i = twoShortAddLongRoot P ∧
                ¬(P.root : (a : ι) → M) i = -twoShortAddLongRoot P ∧
                  ¬(P.root : (a : ι) → M) i = threeShortAddLongRoot P ∧
                    ¬(P.root : (a : ι) → M) i = -threeShortAddLongRoot P ∧
                      ¬(P.root : (a : ι) → M) i = threeShortAddTwoLongRoot P ∧
                        ¬(P.root : (a : ι) → M) i = -threeShortAddTwoLongRoot P
h₁ : ¬(P.root : (a : ι) → M) i = longRoot P
h₂ : ¬(P.root : (a : ι) → M) i = -longRoot P
h₃ : ¬(P.root : (a : ι) → M) i = shortRoot P
h₄ : ¬(P.root : (a : ι) → M) i = -shortRoot P
h₅ : ¬(P.root : (a : ι) → M) i = shortAddLongRoot P
h₆ : ¬(P.root : (a : ι) → M) i = -shortAddLongRoot P
h₇ : ¬(P.root : (a : ι) → M) i = twoShortAddLongRoot P
⊢ P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0
have h₈ : ¬(P.root : (a : ι) → M) i = -twoShortAddLongRoot P
Tactic: obtain ⟨h₁, h₂, h₃, h₄, h₅, h₆, h₇, h₈, h₉, h₁₀, h₁₁, h₁₂⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
hi :
  ¬(P.root : (a : ι) → M) i = longRoot P ∧
    ¬(P.root : (a : ι) → M) i = -longRoot P ∧
      ¬(P.root : (a : ι) → M) i = shortRoot P ∧
        ¬(P.root : (a : ι) → M) i = -shortRoot P ∧
          ¬(P.root : (a : ι) → M) i = shortAddLongRoot P ∧
            ¬(P.root : (a : ι) → M) i = -shortAddLongRoot P ∧
              ¬(P.root : (a : ι) → M) i = twoShortAddLongRoot P ∧
                ¬(P.root : (a : ι) → M) i = -twoShortAddLongRoot P ∧
                  ¬(P.root : (a : ι) → M) i = threeShortAddLongRoot P ∧
                    ¬(P.root : (a : ι) → M) i = -threeShortAddLongRoot P ∧
                      ¬(P.root : (a : ι) → M) i = threeShortAddTwoLongRoot P ∧
                        ¬(P.root : (a : ι) → M) i = -threeShortAddTwoLongRoot P
h₁ : ¬(P.root : (a : ι) → M) i = longRoot P
h₂ : ¬(P.root : (a : ι) → M) i = -longRoot P
h₃ : ¬(P.root : (a : ι) → M) i = shortRoot P
h₄ : ¬(P.root : (a : ι) → M) i = -shortRoot P
h₅ : ¬(P.root : (a : ι) → M) i = shortAddLongRoot P
h₆ : ¬(P.root : (a : ι) → M) i = -shortAddLongRoot P
h₇ : ¬(P.root : (a : ι) → M) i = twoShortAddLongRoot P
h₈ : ¬(P.root : (a : ι) → M) i = -twoShortAddLongRoot P
⊢ P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0
have h₉ : ¬(P.root : (a : ι) → M) i = threeShortAddLongRoot P
Tactic: obtain ⟨h₁, h₂, h₃, h₄, h₅, h₆, h₇, h₈, h₉, h₁₀, h₁₁, h₁₂⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
hi :
  ¬(P.root : (a : ι) → M) i = longRoot P ∧
    ¬(P.root : (a : ι) → M) i = -longRoot P ∧
      ¬(P.root : (a : ι) → M) i = shortRoot P ∧
        ¬(P.root : (a : ι) → M) i = -shortRoot P ∧
          ¬(P.root : (a : ι) → M) i = shortAddLongRoot P ∧
            ¬(P.root : (a : ι) → M) i = -shortAddLongRoot P ∧
              ¬(P.root : (a : ι) → M) i = twoShortAddLongRoot P ∧
                ¬(P.root : (a : ι) → M) i = -twoShortAddLongRoot P ∧
                  ¬(P.root : (a : ι) → M) i = threeShortAddLongRoot P ∧
                    ¬(P.root : (a : ι) → M) i = -threeShortAddLongRoot P ∧
                      ¬(P.root : (a : ι) → M) i = threeShortAddTwoLongRoot P ∧
                        ¬(P.root : (a : ι) → M) i = -threeShortAddTwoLongRoot P
h₁ : ¬(P.root : (a : ι) → M) i = longRoot P
h₂ : ¬(P.root : (a : ι) → M) i = -longRoot P
h₃ : ¬(P.root : (a : ι) → M) i = shortRoot P
h₄ : ¬(P.root : (a : ι) → M) i = -shortRoot P
h₅ : ¬(P.root : (a : ι) → M) i = shortAddLongRoot P
h₆ : ¬(P.root : (a : ι) → M) i = -shortAddLongRoot P
h₇ : ¬(P.root : (a : ι) → M) i = twoShortAddLongRoot P
h₈ : ¬(P.root : (a : ι) → M) i = -twoShortAddLongRoot P
h₉ : ¬(P.root : (a : ι) → M) i = threeShortAddLongRoot P
⊢ P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0
have h₁₀ : ¬(P.root : (a : ι) → M) i = -threeShortAddLongRoot P
Tactic: obtain ⟨h₁, h₂, h₃, h₄, h₅, h₆, h₇, h₈, h₉, h₁₀, h₁₁, h₁₂⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
hi :
  ¬(P.root : (a : ι) → M) i = longRoot P ∧
    ¬(P.root : (a : ι) → M) i = -longRoot P ∧
      ¬(P.root : (a : ι) → M) i = shortRoot P ∧
        ¬(P.root : (a : ι) → M) i = -shortRoot P ∧
          ¬(P.root : (a : ι) → M) i = shortAddLongRoot P ∧
            ¬(P.root : (a : ι) → M) i = -shortAddLongRoot P ∧
              ¬(P.root : (a : ι) → M) i = twoShortAddLongRoot P ∧
                ¬(P.root : (a : ι) → M) i = -twoShortAddLongRoot P ∧
                  ¬(P.root : (a : ι) → M) i = threeShortAddLongRoot P ∧
                    ¬(P.root : (a : ι) → M) i = -threeShortAddLongRoot P ∧
                      ¬(P.root : (a : ι) → M) i = threeShortAddTwoLongRoot P ∧
                        ¬(P.root : (a : ι) → M) i = -threeShortAddTwoLongRoot P
h₁ : ¬(P.root : (a : ι) → M) i = longRoot P
h₂ : ¬(P.root : (a : ι) → M) i = -longRoot P
h₃ : ¬(P.root : (a : ι) → M) i = shortRoot P
h₄ : ¬(P.root : (a : ι) → M) i = -shortRoot P
h₅ : ¬(P.root : (a : ι) → M) i = shortAddLongRoot P
h₆ : ¬(P.root : (a : ι) → M) i = -shortAddLongRoot P
h₇ : ¬(P.root : (a : ι) → M) i = twoShortAddLongRoot P
h₈ : ¬(P.root : (a : ι) → M) i = -twoShortAddLongRoot P
h₉ : ¬(P.root : (a : ι) → M) i = threeShortAddLongRoot P
h₁₀ : ¬(P.root : (a : ι) → M) i = -threeShortAddLongRoot P
⊢ P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0
have h₁₁ : ¬(P.root : (a : ι) → M) i = threeShortAddTwoLongRoot P
Tactic: obtain ⟨h₁, h₂, h₃, h₄, h₅, h₆, h₇, h₈, h₉, h₁₀, h₁₁, h₁₂⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
hi :
  ¬(P.root : (a : ι) → M) i = longRoot P ∧
    ¬(P.root : (a : ι) → M) i = -longRoot P ∧
      ¬(P.root : (a : ι) → M) i = shortRoot P ∧
        ¬(P.root : (a : ι) → M) i = -shortRoot P ∧
          ¬(P.root : (a : ι) → M) i = shortAddLongRoot P ∧
            ¬(P.root : (a : ι) → M) i = -shortAddLongRoot P ∧
              ¬(P.root : (a : ι) → M) i = twoShortAddLongRoot P ∧
                ¬(P.root : (a : ι) → M) i = -twoShortAddLongRoot P ∧
                  ¬(P.root : (a : ι) → M) i = threeShortAddLongRoot P ∧
                    ¬(P.root : (a : ι) → M) i = -threeShortAddLongRoot P ∧
                      ¬(P.root : (a : ι) → M) i = threeShortAddTwoLongRoot P ∧
                        ¬(P.root : (a : ι) → M) i = -threeShortAddTwoLongRoot P
h₁ : ¬(P.root : (a : ι) → M) i = longRoot P
h₂ : ¬(P.root : (a : ι) → M) i = -longRoot P
h₃ : ¬(P.root : (a : ι) → M) i = shortRoot P
h₄ : ¬(P.root : (a : ι) → M) i = -shortRoot P
h₅ : ¬(P.root : (a : ι) → M) i = shortAddLongRoot P
h₆ : ¬(P.root : (a : ι) → M) i = -shortAddLongRoot P
h₇ : ¬(P.root : (a : ι) → M) i = twoShortAddLongRoot P
h₈ : ¬(P.root : (a : ι) → M) i = -twoShortAddLongRoot P
h₉ : ¬(P.root : (a : ι) → M) i = threeShortAddLongRoot P
h₁₀ : ¬(P.root : (a : ι) → M) i = -threeShortAddLongRoot P
h₁₁ : ¬(P.root : (a : ι) → M) i = threeShortAddTwoLongRoot P
⊢ P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0
have h₁₂ : ¬(P.root : (a : ι) → M) i = -threeShortAddTwoLongRoot P
Tactic: obtain ⟨h₁, h₂, h₃, h₄, h₅, h₆, h₇, h₈, h₉, h₁₀, h₁₁, h₁₂⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
h₁ : ¬(P.root : (a : ι) → M) i = longRoot P
h₂ : ¬(P.root : (a : ι) → M) i = -longRoot P
h₃ : ¬(P.root : (a : ι) → M) i = shortRoot P
h₄ : ¬(P.root : (a : ι) → M) i = -shortRoot P
h₅ : ¬(P.root : (a : ι) → M) i = shortAddLongRoot P
h₆ : ¬(P.root : (a : ι) → M) i = -shortAddLongRoot P
h₇ : ¬(P.root : (a : ι) → M) i = twoShortAddLongRoot P
h₈ : ¬(P.root : (a : ι) → M) i = -twoShortAddLongRoot P
h₉ : ¬(P.root : (a : ι) → M) i = threeShortAddLongRoot P
h₁₀ : ¬(P.root : (a : ι) → M) i = -threeShortAddLongRoot P
h₁₁ : ¬(P.root : (a : ι) → M) i = threeShortAddTwoLongRoot P
h₁₂ : ¬(P.root : (a : ι) → M) i = -threeShortAddTwoLongRoot P
⊢ P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0
have ha : Membership.mem (γ := Set (ℤ × ℤ))
  {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
  (P.pairingIn ℤ i (short P), P.pairingIn ℤ (short P) i)
Tactic: have ha := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed' i (short P) ‹_› ‹_›