awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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
inr : P.pairingIn S i j ≤ 0 ↔ LE.le.{u_5} (α := S) 0 0
inr₁ inr₂ : LE.le.{u_5} (α := S) 0 0 ↔ LE.le.{u_5} (α := S) 0 0
⊢ P.pairingIn S i j ≤ 0 ↔ P.pairingIn S j i ≤ 0

Tactic:
rw [hji, P.pairingIn_eq_zero_iff.mp hji]

Premises used: RootPairing.pairingIn_eq_zero_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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
inr : P.pairingIn S i j < 0 ↔ P.pairingIn S j i < 0
⊢ 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]

Premises used: le_iff_eq_or_lt, or_iff_right
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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

Tactic:
P.pairingIn_lt_zero_iff S

Premises used: RootPairing.pairingIn_lt_zero_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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

Tactic:
exact P.pairingIn_lt_zero_iff S

Premises used: RootPairing.pairingIn_lt_zero_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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.IsG2
⊢ Nonempty ι

Tactic:
⟨(IsG2.exists_pairingIn_neg_three (P := P)).choose⟩

Premises used: Nonempty.intro, Exists.choose, RootPairing.IsG2.exists_pairingIn_neg_three
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
⊢ P.IsG2 ↔ ∃ (i : ι) (j : ι), P.pairingIn ℤ i j = -3

Tactic:
⟨fun _ ↦ IsG2.exists_pairingIn_neg_three, fun h ↦ ⟨h⟩⟩

Premises used: Iff.intro, RootPairing.IsG2.mk, RootPairing.IsG2.exists_pairingIn_neg_three
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
⊢ P.IsNotG2 ↔ ∀ (i j : ι), Membership.mem (γ := Set ℤ) {-2, -1, 0, 1, 2} (P.pairingIn ℤ i j)

Tactic:
⟨fun _ ↦ IsNotG2.pairingIn_mem_zero_one_two, fun h ↦ ⟨h⟩⟩

Premises used: Iff.intro, RootPairing.IsNotG2.mk, RootPairing.IsNotG2.pairingIn_mem_zero_one_two
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
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
⊢ ¬P.IsG2 ↔ P.IsNotG2

Tactic:
simp only [isG2_iff, isNotG2_iff, not_exists, Set.mem_insert_iff, mem_singleton_iff]

Premises used: RootPairing.isG2_iff, not_exists, Set.mem_singleton_iff, RootPairing.isNotG2_iff, Set.mem_insert_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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

Tactic:
⟨fun h i j ↦ ?_, fun h i j ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
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
⊢ (∀ (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 ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 ℤ ((P.reflectionPerm i : (a : ι) → ι) i) j = -3

Tactic:
have hij := h (P.reflectionPerm i i) j
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
⊢ 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
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
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)
⊢ 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:
aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 = -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
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
i j : ι
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
⊢ ¬P.pairingIn ℤ i j = -3

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
⊢ 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
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 (ℤ × ℤ))
    {(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'
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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)
⊢ 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₂ ⊢

Premises used: Prod.mk_zero_zero, Prod.mk_eq_one, Prod.mk_one_one, Set.mem_singleton_iff, Prod.mk_eq_zero, Prod.mk.injEq, Set.mem_insert_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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₂ :
  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
⊢ P.pairingIn ℤ i j = -3 ∨
    P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 0 ∨ P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ i j = 3

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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)
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
⊢ Membership.mem (γ := Set ℤ) {-3, -1, 0, 1, 3} (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
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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)
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
⊢ ¬∀ (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)

Premises used: RootPairing.IsG2.exists_pairingIn_neg_three
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
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
⊢ ¬∀ (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

Premises used: Not
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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

Tactic:
⟨k, l, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
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
⊢ ∃ (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:
refine ⟨k, l, ?_⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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
⊢ 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
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
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 = 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

Premises used: Prod.mk_zero_zero, Prod.mk_eq_one, Prod.mk_one_one, Set.mem_singleton_iff, Prod.mk_eq_zero, Prod.mk.injEq, Set.mem_insert_iff