awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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
S : Type u_5
inst_5 : CommRing S
inst_6 : LinearOrder S
inst_7 : IsStrictOrderedRing S
inst_8 : Algebra S R
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : P.IsValuedIn S
i j : ι
inst_13 : Finite ι
inst_14 : NeZero.{u_2} (R := R) 2
inst_15 : IsDomain R
inst_16 : IsTorsionFree R M
hij : P.pairingIn S i j ≠ 0
hji : P.pairingIn S j i ≠ 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0
have inr : P.pairingIn S i j < 0 ↔ P.pairingIn S j i < 0
Tactic: rw [le_iff_eq_or_lt, le_iff_eq_or_lt, or_iff_right hij, or_iff_right hji]
-- 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.IsCrystallographic
inst_6 : P.IsReduced
inst_7 : P.IsIrreducible
inst_8 : Finite ι
inst_9 : CharZero R
inst_10 : IsDomain R
⊢ ¬P.IsG2 ↔ P.IsNotG2
have simp : (∀ (x x_1 : ι), ¬P.pairingIn ℤ x x_1 = -3) ↔
  ∀ (i j : ι),
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 0 ∨ P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ i j = 2
Tactic: simp only [isG2_iff, isNotG2_iff, not_exists, Set.mem_insert_iff, mem_singleton_iff]
-- 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.IsCrystallographic
inst_6 : P.IsReduced
inst_7 : P.IsIrreducible
inst_8 : Finite ι
inst_9 : CharZero R
inst_10 : IsDomain R
⊢ (∀ (x x_1 : ι), ¬P.pairingIn ℤ x x_1 = -3) ↔
    ∀ (i j : ι),
      P.pairingIn ℤ i j = -2 ∨
        P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 0 ∨ P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ i j = 2
have refine_1 : ∀ (h : ∀ (x x_1 : ι), ¬P.pairingIn ℤ x x_1 = -3) (i j : ι),
  P.pairingIn ℤ i j = -2 ∨
    P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 0 ∨ P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ i j = 2
Tactic: refine ⟨fun h i j ↦ ?_, fun h i j ↦ ?_⟩
-- 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.IsCrystallographic
inst_6 : P.IsReduced
inst_7 : P.IsIrreducible
inst_8 : Finite ι
inst_9 : CharZero R
inst_10 : IsDomain R
refine_1 :
  ∀ (h : ∀ (x x_1 : ι), ¬P.pairingIn ℤ x x_1 = -3) (i j : ι),
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 0 ∨ P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ i j = 2
⊢ (∀ (x x_1 : ι), ¬P.pairingIn ℤ x x_1 = -3) ↔
    ∀ (i j : ι),
      P.pairingIn ℤ i j = -2 ∨
        P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 0 ∨ P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ i j = 2
have refine_2 : ∀
  (h :
    ∀ (i j : ι),
      P.pairingIn ℤ i j = -2 ∨
        P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 0 ∨ P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ i j = 2)
  (i j : ι), ¬P.pairingIn ℤ i j = -3
Tactic: refine ⟨fun h i j ↦ ?_, fun h i j ↦ ?_⟩
-- 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.IsCrystallographic
inst_6 : P.IsReduced
inst_7 : P.IsIrreducible
inst_8 : Finite ι
inst_9 : CharZero R
inst_10 : IsDomain R
h : ∀ (x x_1 : ι), ¬P.pairingIn ℤ x x_1 = -3
i j : ι
⊢ P.pairingIn ℤ i j = -2 ∨
    P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 0 ∨ P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ i j = 2
have hij : ¬P.pairingIn ℤ ((P.reflectionPerm i : (a : ι) → ι) i) j = -3
Tactic: have hij := h (P.reflectionPerm i i) j
-- 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.IsCrystallographic
inst_6 : P.IsReduced
inst_7 : P.IsIrreducible
inst_8 : Finite ι
inst_9 : CharZero R
inst_10 : IsDomain R
h : ∀ (x x_1 : ι), ¬P.pairingIn ℤ x x_1 = -3
i j : ι
hij : ¬P.pairingIn ℤ ((P.reflectionPerm i : (a : ι) → ι) i) j = -3
⊢ P.pairingIn ℤ i j = -2 ∨
    P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 0 ∨ P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ i j = 2
have this : 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), (2, 2), (-2, -2)}
  (P.pairingIn ℤ i j, P.pairingIn ℤ j i)
Tactic: have := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed i j
-- 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.IsCrystallographic
inst_6 : P.IsReduced
inst_7 : P.IsIrreducible
inst_8 : Finite ι
inst_9 : CharZero R
inst_10 : IsDomain R
h :
  ∀ (i j : ι),
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 0 ∨ P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ i j = 2
i j : ι
⊢ ¬P.pairingIn ℤ i j = -3
have h₁ : P.pairingIn ℤ i j = -2 ∨ P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 0 ∨ P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ i j = 2
Tactic: specialize h i j
Cleared hypotheses: h
-- 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.IsCrystallographic
inst_6 : P.IsReduced
inst_7 : P.IsIrreducible
inst_8 : Finite ι
inst_9 : CharZero R
inst_10 : IsDomain R
inst_11 : P.IsG2
i j : ι
h : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
h' : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
this :
  ¬∀ (i j : ι),
      P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
        P.pairingIn ℤ i j = 2 * P.pairingIn ℤ j i ∨ P.pairingIn ℤ j i = 2 * P.pairingIn ℤ i j
⊢ Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (P.pairingIn ℤ i j)
have aux₁ : P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
  P.pairingIn ℤ i j = 3 * P.pairingIn ℤ j i ∨ P.pairingIn ℤ j i = 3 * P.pairingIn ℤ i j
Tactic: have aux₁ := P.forall_pairingIn_eq_swap_or.resolve_left this i j
-- 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.IsCrystallographic
inst_6 : P.IsReduced
inst_7 : P.IsIrreducible
inst_8 : Finite ι
inst_9 : CharZero R
inst_10 : IsDomain R
inst_11 : P.IsG2
i j : ι
h : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
h' : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
this :
  ¬∀ (i j : ι),
      P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
        P.pairingIn ℤ i j = 2 * P.pairingIn ℤ j i ∨ P.pairingIn ℤ j i = 2 * P.pairingIn ℤ i j
aux₁ :
  P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
    P.pairingIn ℤ i j = 3 * P.pairingIn ℤ j i ∨ P.pairingIn ℤ j i = 3 * P.pairingIn ℤ i j
⊢ Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (P.pairingIn ℤ i j)
have aux₂ : 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 j, P.pairingIn ℤ j i)
Tactic: have aux₂ := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed' i j h h'
-- 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.IsCrystallographic
inst_6 : P.IsReduced
inst_7 : P.IsIrreducible
inst_8 : Finite ι
inst_9 : CharZero R
inst_10 : IsDomain R
inst_11 : P.IsG2
i j : ι
h : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
h' : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
this :
  ¬∀ (i j : ι),
      P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
        P.pairingIn ℤ i j = 2 * P.pairingIn ℤ j i ∨ P.pairingIn ℤ j i = 2 * P.pairingIn ℤ i j
aux₁ :
  P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
    P.pairingIn ℤ i j = 3 * P.pairingIn ℤ j i ∨ P.pairingIn ℤ j i = 3 * P.pairingIn ℤ i j
aux₂ :
  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 j, P.pairingIn ℤ j i)
⊢ Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (P.pairingIn ℤ i j)
have aux₃ : P.pairingIn ℤ i j = 0 ∧ P.pairingIn ℤ j i = 0 ∨
  P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 1 ∨
    P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -1 ∨
      P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 2 ∨
        P.pairingIn ℤ i j = 2 ∧ P.pairingIn ℤ j i = 1 ∨
          P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -2 ∨
            P.pairingIn ℤ i j = -2 ∧ P.pairingIn ℤ j i = -1 ∨
              P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 3 ∨
                P.pairingIn ℤ i j = 3 ∧ P.pairingIn ℤ j i = 1 ∨
                  P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -3 ∨ P.pairingIn ℤ i j = -3 ∧ P.pairingIn ℤ j i = -1
Tactic: simp only [mem_insert_iff, mem_singleton_iff, Prod.mk_zero_zero, Prod.mk_eq_zero,
      Prod.mk_one_one, Prod.mk_eq_one, Prod.mk.injEq] at aux₂ ⊢
Cleared hypotheses: aux₂
-- 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.IsCrystallographic
inst_6 : P.IsReduced
inst_7 : P.IsIrreducible
inst_8 : Finite ι
inst_9 : CharZero R
inst_10 : IsDomain R
inst_11 : P.IsG2
i j : ι
h : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
h' : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
⊢ Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (P.pairingIn ℤ i j)
have suffices : ¬∀ (i j : ι),
    P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
      P.pairingIn ℤ i j = 2 * P.pairingIn ℤ j i ∨ P.pairingIn ℤ j i = 2 * P.pairingIn ℤ i j
Tactic: suffices ¬ (∀ i j, P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
                     P.pairingIn ℤ i j = 2 * P.pairingIn ℤ j i ∨
                     P.pairingIn ℤ j i = 2 * P.pairingIn ℤ i j) by
    have aux₁ := P.forall_pairingIn_eq_swap_or.resolve_left this i j
    have aux₂ := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed' i j h h'
    simp only [mem_insert_iff, mem_singleton_iff, Prod.mk_zero_zero, Prod.mk_eq_zero,
      Prod.mk_one_one, Prod.mk_eq_one, Prod.mk.injEq] at aux₂ ⊢
    lia
-- 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.IsCrystallographic
inst_6 : P.IsReduced
inst_7 : P.IsIrreducible
inst_8 : Finite ι
inst_9 : CharZero R
inst_10 : IsDomain R
inst_11 : P.IsG2
i j : ι
h : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
h' : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
⊢ ¬∀ (i j : ι),
      P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
        P.pairingIn ℤ i j = 2 * P.pairingIn ℤ j i ∨ P.pairingIn ℤ j i = 2 * P.pairingIn ℤ i j
have obtain : ∀ (k l : ι) (hkl : P.pairingIn ℤ k l = -3),
  ¬∀ (i j : ι),
      P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
        P.pairingIn ℤ i j = 2 * P.pairingIn ℤ j i ∨ P.pairingIn ℤ j i = 2 * P.pairingIn ℤ i j
Tactic: obtain ⟨k, l, hkl⟩ := exists_pairingIn_neg_three (P := P)
-- 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.IsCrystallographic
inst_6 : P.IsReduced
inst_7 : P.IsIrreducible
inst_8 : Finite ι
inst_9 : CharZero R
inst_10 : IsDomain R
inst_11 : P.IsG2
i j : ι
h : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
h' : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
k l : ι
hkl : P.pairingIn ℤ k l = -3
⊢ ¬∀ (i j : ι),
      P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
        P.pairingIn ℤ i j = 2 * P.pairingIn ℤ j i ∨ P.pairingIn ℤ j i = 2 * P.pairingIn ℤ i j
have push : ∃ (i : ι) (j : ι),
  P.pairingIn ℤ i j ≠ P.pairingIn ℤ j i ∧
    P.pairingIn ℤ i j ≠ 2 * P.pairingIn ℤ j i ∧ P.pairingIn ℤ j i ≠ 2 * P.pairingIn ℤ i j
Tactic: push Not
-- 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.IsCrystallographic
inst_6 : P.IsReduced
inst_7 : P.IsIrreducible
inst_8 : Finite ι
inst_9 : CharZero R
inst_10 : IsDomain R
inst_11 : P.IsG2
i j : ι
h : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
h' : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
k l : ι
hkl : P.pairingIn ℤ k l = -3
⊢ ∃ (i : ι) (j : ι),
    P.pairingIn ℤ i j ≠ P.pairingIn ℤ j i ∧
      P.pairingIn ℤ i j ≠ 2 * P.pairingIn ℤ j i ∧ P.pairingIn ℤ j i ≠ 2 * P.pairingIn ℤ i j
have refine : P.pairingIn ℤ k l ≠ P.pairingIn ℤ l k ∧
  P.pairingIn ℤ k l ≠ 2 * P.pairingIn ℤ l k ∧ P.pairingIn ℤ l k ≠ 2 * P.pairingIn ℤ k l
Tactic: refine ⟨k, l, ?_⟩
-- 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.IsCrystallographic
inst_6 : P.IsReduced
inst_7 : P.IsIrreducible
inst_8 : Finite ι
inst_9 : CharZero R
inst_10 : IsDomain R
inst_11 : P.IsG2
i j : ι
h : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
h' : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
k l : ι
hkl : P.pairingIn ℤ k l = -3
⊢ P.pairingIn ℤ k l ≠ P.pairingIn ℤ l k ∧
    P.pairingIn ℤ k l ≠ 2 * P.pairingIn ℤ l k ∧ P.pairingIn ℤ l k ≠ 2 * P.pairingIn ℤ k l
have aux : 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), (2, 2), (-2, -2)}
  (P.pairingIn ℤ k l, P.pairingIn ℤ l k)
Tactic: have aux := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed k l
-- 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.IsCrystallographic
inst_6 : P.IsReduced
inst_7 : P.IsIrreducible
inst_8 : Finite ι
inst_9 : CharZero R
inst_10 : IsDomain R
inst_11 : P.IsG2
i j : ι
h : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
h' : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
k l : ι
hkl : P.pairingIn ℤ k l = -3
aux :
  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), (2, 2), (-2, -2)}
    (P.pairingIn ℤ k l, P.pairingIn ℤ l k)
⊢ P.pairingIn ℤ k l ≠ P.pairingIn ℤ l k ∧
    P.pairingIn ℤ k l ≠ 2 * P.pairingIn ℤ l k ∧ P.pairingIn ℤ l k ≠ 2 * P.pairingIn ℤ k l
have aux₁ : P.pairingIn ℤ k l = 0 ∧ P.pairingIn ℤ l k = 0 ∨
  P.pairingIn ℤ k l = 1 ∧ P.pairingIn ℤ l k = 1 ∨
    P.pairingIn ℤ k l = -1 ∧ P.pairingIn ℤ l k = -1 ∨
      P.pairingIn ℤ k l = 1 ∧ P.pairingIn ℤ l k = 2 ∨
        P.pairingIn ℤ k l = 2 ∧ P.pairingIn ℤ l k = 1 ∨
          P.pairingIn ℤ k l = -1 ∧ P.pairingIn ℤ l k = -2 ∨
            P.pairingIn ℤ k l = -2 ∧ P.pairingIn ℤ l k = -1 ∨
              P.pairingIn ℤ k l = 1 ∧ P.pairingIn ℤ l k = 3 ∨
                P.pairingIn ℤ k l = 3 ∧ P.pairingIn ℤ l k = 1 ∨
                  P.pairingIn ℤ k l = -1 ∧ P.pairingIn ℤ l k = -3 ∨
                    P.pairingIn ℤ k l = -3 ∧ P.pairingIn ℤ l k = -1 ∨
                      P.pairingIn ℤ k l = 2 ∧ P.pairingIn ℤ l k = 2 ∨ P.pairingIn ℤ k l = -2 ∧ P.pairingIn ℤ l k = -2
Tactic: simp only [mem_insert_iff, mem_singleton_iff, Prod.mk_zero_zero, Prod.mk_eq_zero,
      Prod.mk_one_one, Prod.mk_eq_one, Prod.mk.injEq] at aux
Cleared hypotheses: aux
-- 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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
i j : ι
inst_8 : P.IsNotG2
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
      chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
    2
have pos : ∀
  (h :
    LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)),
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
      chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
    2
Tactic: by_cases h : LinearIndependent R ![P.root i, P.root j]
-- 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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
i j : ι
inst_8 : P.IsNotG2
pos :
  ∀
    (h :
      LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
        (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)),
    chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
        chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
      2
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
      chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
    2
have neg : ∀
  (h :
    ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
        (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)),
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
      chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
    2
Tactic: by_cases h : LinearIndependent R ![P.root i, P.root j]
-- 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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
i j : ι
inst_8 : P.IsNotG2
h :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
      chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
    2
have pos : P.pairingIn ℤ (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) i ≤ 2
Tactic: rw [← Int.ofNat_le, Nat.cast_add, Nat.cast_ofNat,
    chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx h]
-- 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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
i j : ι
inst_8 : P.IsNotG2
h :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
⊢ P.pairingIn ℤ (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) i ≤ 2
have this : Membership.mem (γ := Set ℤ) {-2, -1, 0, 1, 2}
  (P.pairingIn ℤ (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) i)
Tactic: have := IsNotG2.pairingIn_mem_zero_one_two (P := P) (P.chainTopIdx i j) i
-- 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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
i j : ι
inst_8 : P.IsNotG2
h :
  Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
⊢ P.pairingIn ℤ i j ≤ 0
have aux₁ : LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
  (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
Tactic: have aux₁ := P.linearIndependent_of_add_mem_range_root' <| add_comm (P.root i) (P.root j) ▸ h
-- 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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
i j : ι
inst_8 : P.IsNotG2
h :
  Membership.mem (γ := Set M) (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
aux₁ :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
⊢ P.pairingIn ℤ i j ≤ 0
have aux₂ : chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j i +
    chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j i ≤
  2
Tactic: have aux₂ := P.chainBotCoeff_add_chainTopCoeff_le_two j i