awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ HMul.hMul (β := R) (P.pairing i (short P))
        ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R) +
      HMul.hMul (β := R) (2 * P.pairing i (long P))
        ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R) =
    HMul.hMul (β := R) (P.pairing i (short P) + 2 * P.pairing i (long P))
      ((((B.form : (a : M) → M →ₗ[R] R) (threeShortAddTwoLongRoot P) : M →ₗ[R] R) : (a : M) → R)
          (threeShortAddTwoLongRoot P) :
        R)

Tactic:
?_
-- 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.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
calc_1 calc_1₁ :
  HMul.hMul (β := R) (P.pairing i (threeShortAddTwoLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) (threeShortAddTwoLongRoot P) : M →ₗ[R] R) : (a : M) → R)
          (threeShortAddTwoLongRoot P) :
        R) =
    HMul.hMul (β := R) (P.pairing i (threeShortAddTwoLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (threeShortAddTwoLong P)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (threeShortAddTwoLong P) : M) :
        R)
⊢ HMul.hMul (β := R) (P.pairing i (threeShortAddTwoLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) (threeShortAddTwoLongRoot P) : M →ₗ[R] R) : (a : M) → R)
          (threeShortAddTwoLongRoot P) :
        R) =
    HMul.hMul (α := R) (β := R) (2 : R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          (threeShortAddTwoLongRoot P) :
        R)

Tactic:
rw [B.two_mul_apply_root_root]

Premises used: RootPairing.InvariantForm.two_mul_apply_root_root
-- 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.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
calc_2 :
  2 *
        HMul.hMul (α := R) (β := R) (3 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R) +
      2 *
        HMul.hMul (α := R) (β := R) (2 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R) =
    3 *
        HMul.hMul (α := R) (β := R) (2 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R) +
      2 *
        HMul.hMul (α := R) (β := R) (2 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R)
⊢ HMul.hMul (α := R) (β := R) (2 : R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          (threeShortAddTwoLongRoot P) :
        R) =
    3 *
        HMul.hMul (α := R) (β := R) (2 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R) +
      2 *
        HMul.hMul (α := R) (β := R) (2 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R)

Tactic:
simp only [threeShortAddTwoLongRoot_eq, map_add, mul_add, map_smul, smul_eq_mul]

Premises used: map_add, RootPairing.EmbeddedG2.threeShortAddTwoLongRoot_eq, mul_add, smul_eq_mul, map_smul
-- 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.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 2 *
        HMul.hMul (α := R) (β := R) (3 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R) +
      2 *
        HMul.hMul (α := R) (β := R) (2 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R) =
    3 *
        HMul.hMul (α := R) (β := R) (2 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R) +
      2 *
        HMul.hMul (α := R) (β := R) (2 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R)

Tactic:
ring
-- 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.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
calc_3 :
  3 *
        HMul.hMul (β := R) (P.pairing i (short P))
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (short P)) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) (short P) : M) :
            R) +
      2 *
        (P.pairing i (long P) *
          HMul.hMul (α := R) (β := R) (3 : R)
            ((((B.form : (a : M) → M →ₗ[R] R) (shortRoot P) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R)) =
    P.pairing i (short P) *
        HMul.hMul (α := R) (β := R) (3 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) (shortRoot P) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R) +
      2 * P.pairing i (long P) *
        HMul.hMul (α := R) (β := R) (3 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) (shortRoot P) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R)
⊢ 3 *
        HMul.hMul (α := R) (β := R) (2 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R) +
      2 *
        HMul.hMul (α := R) (β := R) (2 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R) =
    HMul.hMul (β := R) (P.pairing i (short P))
        ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R) +
      HMul.hMul (β := R) (2 * P.pairing i (long P))
        ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R)

Tactic:
rw [B.two_mul_apply_root_root, B.two_mul_apply_root_root, long_eq_three_mul_short]

Premises used: RootPairing.EmbeddedG2.long_eq_three_mul_short, RootPairing.InvariantForm.two_mul_apply_root_root
-- 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.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 3 *
        HMul.hMul (β := R) (P.pairing i (short P))
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (short P)) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) (short P) : M) :
            R) +
      2 *
        (P.pairing i (long P) *
          HMul.hMul (α := R) (β := R) (3 : R)
            ((((B.form : (a : M) → M →ₗ[R] R) (shortRoot P) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R)) =
    P.pairing i (short P) *
        HMul.hMul (α := R) (β := R) (3 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) (shortRoot P) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R) +
      2 * P.pairing i (long P) *
        HMul.hMul (α := R) (β := R) (3 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) (shortRoot P) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R)

Tactic:
ring
-- 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.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
calc_4 :
  HMul.hMul (β := R) (P.pairing i (short P))
        ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R) +
      HMul.hMul (β := R) (2 * P.pairing i (long P))
        ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R) =
    HMul.hMul (β := R) (P.pairing i (short P) + 2 * P.pairing i (long P))
      ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R)
⊢ HMul.hMul (β := R) (P.pairing i (short P))
        ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R) +
      HMul.hMul (β := R) (2 * P.pairing i (long P))
        ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R) =
    HMul.hMul (β := R) (P.pairing i (short P) + 2 * P.pairing i (long P))
      ((((B.form : (a : M) → M →ₗ[R] R) (threeShortAddTwoLongRoot P) : M →ₗ[R] R) : (a : M) → R)
          (threeShortAddTwoLongRoot P) :
        R)

Tactic:
rw [threeShortAddTwoLongRoot_longRoot]

Premises used: RootPairing.EmbeddedG2.threeShortAddTwoLongRoot_longRoot
-- 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.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ HMul.hMul (β := R) (P.pairing i (short P))
        ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R) +
      HMul.hMul (β := R) (2 * P.pairing i (long P))
        ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R) =
    HMul.hMul (β := R) (P.pairing i (short P) + 2 * P.pairing i (long P))
      ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R)

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
Goal:
a b c d e f a' b' c' d' e' f' : ℤ
S : Set (ℤ × ℤ)
S_def : S = {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
ha : (a, a') ∈ S
hb : (b, b') ∈ S
hc : (c, c') ∈ S
hd : (d, d') ∈ S
he : (e, e') ∈ S
hf : (f, f') ∈ S
h₁ : c = a + 3 * b
h₂ : c' = a' + b'
h₃ : d = 2 * a + 3 * b
h₄ : d' = 2 * a' + b'
h₅ : e = a + b
h₆ : e' = 3 * a' + b'
h₇ : f = a + 2 * b
h₈ : f' = 3 * a' + 2 * b'
⊢ a = 0 ∧ a' = 0 ∨
    a = 1 ∧ a' = 1 ∨
      a = -1 ∧ a' = -1 ∨
        a = 1 ∧ a' = 2 ∨
          a = 2 ∧ a' = 1 ∨
            a = -1 ∧ a' = -2 ∨ a = -2 ∧ a' = -1 ∨ a = 1 ∧ a' = 3 ∨ a = 3 ∧ a' = 1 ∨ a = -1 ∧ a' = -3 ∨ a = -3 ∧ a' = -1

Tactic:
simp [S_def] at ha hb hc hd he hf
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
Goal:
a b c d e f a' b' c' d' e' f' : ℤ
S : Set (ℤ × ℤ)
S_def : S = {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
ha : (a, a') ∈ S
hb : (b, b') ∈ S
hc : (c, c') ∈ S
hd : (d, d') ∈ S
he : (e, e') ∈ S
hf : (f, f') ∈ S
h₁ : c = a + 3 * b
h₂ : c' = a' + b'
h₃ : d = 2 * a + 3 * b
h₄ : d' = 2 * a' + b'
h₅ : e = a + b
h₆ : e' = 3 * a' + b'
h₇ : f = a + 2 * b
h₈ : f' = 3 * a' + 2 * b'
ha₁ :
  a = 0 ∧ a' = 0 ∨
    a = 1 ∧ a' = 1 ∨
      a = -1 ∧ a' = -1 ∨
        a = 1 ∧ a' = 2 ∨
          a = 2 ∧ a' = 1 ∨
            a = -1 ∧ a' = -2 ∨ a = -2 ∧ a' = -1 ∨ a = 1 ∧ a' = 3 ∨ a = 3 ∧ a' = 1 ∨ a = -1 ∧ a' = -3 ∨ a = -3 ∧ a' = -1
⊢ b = 0 ∧ b' = 0 ∨
    b = 1 ∧ b' = 1 ∨
      b = -1 ∧ b' = -1 ∨
        b = 1 ∧ b' = 2 ∨
          b = 2 ∧ b' = 1 ∨
            b = -1 ∧ b' = -2 ∨ b = -2 ∧ b' = -1 ∨ b = 1 ∧ b' = 3 ∨ b = 3 ∧ b' = 1 ∨ b = -1 ∧ b' = -3 ∨ b = -3 ∧ b' = -1

Tactic:
simp [S_def] at ha hb hc hd he hf
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
Goal:
a b c d e f a' b' c' d' e' f' : ℤ
S : Set (ℤ × ℤ)
S_def : S = {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
ha : (a, a') ∈ S
hb : (b, b') ∈ S
hc : (c, c') ∈ S
hd : (d, d') ∈ S
he : (e, e') ∈ S
hf : (f, f') ∈ S
h₁ : c = a + 3 * b
h₂ : c' = a' + b'
h₃ : d = 2 * a + 3 * b
h₄ : d' = 2 * a' + b'
h₅ : e = a + b
h₆ : e' = 3 * a' + b'
h₇ : f = a + 2 * b
h₈ : f' = 3 * a' + 2 * b'
ha₁ :
  a = 0 ∧ a' = 0 ∨
    a = 1 ∧ a' = 1 ∨
      a = -1 ∧ a' = -1 ∨
        a = 1 ∧ a' = 2 ∨
          a = 2 ∧ a' = 1 ∨
            a = -1 ∧ a' = -2 ∨ a = -2 ∧ a' = -1 ∨ a = 1 ∧ a' = 3 ∨ a = 3 ∧ a' = 1 ∨ a = -1 ∧ a' = -3 ∨ a = -3 ∧ a' = -1
hb₁ :
  b = 0 ∧ b' = 0 ∨
    b = 1 ∧ b' = 1 ∨
      b = -1 ∧ b' = -1 ∨
        b = 1 ∧ b' = 2 ∨
          b = 2 ∧ b' = 1 ∨
            b = -1 ∧ b' = -2 ∨ b = -2 ∧ b' = -1 ∨ b = 1 ∧ b' = 3 ∨ b = 3 ∧ b' = 1 ∨ b = -1 ∧ b' = -3 ∨ b = -3 ∧ b' = -1
⊢ c = 0 ∧ c' = 0 ∨
    c = 1 ∧ c' = 1 ∨
      c = -1 ∧ c' = -1 ∨
        c = 1 ∧ c' = 2 ∨
          c = 2 ∧ c' = 1 ∨
            c = -1 ∧ c' = -2 ∨ c = -2 ∧ c' = -1 ∨ c = 1 ∧ c' = 3 ∨ c = 3 ∧ c' = 1 ∨ c = -1 ∧ c' = -3 ∨ c = -3 ∧ c' = -1

Tactic:
simp [S_def] at ha hb hc hd he hf
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
Goal:
a b c d e f a' b' c' d' e' f' : ℤ
S : Set (ℤ × ℤ)
S_def : S = {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
ha : (a, a') ∈ S
hb : (b, b') ∈ S
hc : (c, c') ∈ S
hd : (d, d') ∈ S
he : (e, e') ∈ S
hf : (f, f') ∈ S
h₁ : c = a + 3 * b
h₂ : c' = a' + b'
h₃ : d = 2 * a + 3 * b
h₄ : d' = 2 * a' + b'
h₅ : e = a + b
h₆ : e' = 3 * a' + b'
h₇ : f = a + 2 * b
h₈ : f' = 3 * a' + 2 * b'
ha₁ :
  a = 0 ∧ a' = 0 ∨
    a = 1 ∧ a' = 1 ∨
      a = -1 ∧ a' = -1 ∨
        a = 1 ∧ a' = 2 ∨
          a = 2 ∧ a' = 1 ∨
            a = -1 ∧ a' = -2 ∨ a = -2 ∧ a' = -1 ∨ a = 1 ∧ a' = 3 ∨ a = 3 ∧ a' = 1 ∨ a = -1 ∧ a' = -3 ∨ a = -3 ∧ a' = -1
hb₁ :
  b = 0 ∧ b' = 0 ∨
    b = 1 ∧ b' = 1 ∨
      b = -1 ∧ b' = -1 ∨
        b = 1 ∧ b' = 2 ∨
          b = 2 ∧ b' = 1 ∨
            b = -1 ∧ b' = -2 ∨ b = -2 ∧ b' = -1 ∨ b = 1 ∧ b' = 3 ∨ b = 3 ∧ b' = 1 ∨ b = -1 ∧ b' = -3 ∨ b = -3 ∧ b' = -1
hc₁ :
  c = 0 ∧ c' = 0 ∨
    c = 1 ∧ c' = 1 ∨
      c = -1 ∧ c' = -1 ∨
        c = 1 ∧ c' = 2 ∨
          c = 2 ∧ c' = 1 ∨
            c = -1 ∧ c' = -2 ∨ c = -2 ∧ c' = -1 ∨ c = 1 ∧ c' = 3 ∨ c = 3 ∧ c' = 1 ∨ c = -1 ∧ c' = -3 ∨ c = -3 ∧ c' = -1
⊢ d = 0 ∧ d' = 0 ∨
    d = 1 ∧ d' = 1 ∨
      d = -1 ∧ d' = -1 ∨
        d = 1 ∧ d' = 2 ∨
          d = 2 ∧ d' = 1 ∨
            d = -1 ∧ d' = -2 ∨ d = -2 ∧ d' = -1 ∨ d = 1 ∧ d' = 3 ∨ d = 3 ∧ d' = 1 ∨ d = -1 ∧ d' = -3 ∨ d = -3 ∧ d' = -1

Tactic:
simp [S_def] at ha hb hc hd he hf
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
Goal:
a b c d e f a' b' c' d' e' f' : ℤ
S : Set (ℤ × ℤ)
S_def : S = {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
ha : (a, a') ∈ S
hb : (b, b') ∈ S
hc : (c, c') ∈ S
hd : (d, d') ∈ S
he : (e, e') ∈ S
hf : (f, f') ∈ S
h₁ : c = a + 3 * b
h₂ : c' = a' + b'
h₃ : d = 2 * a + 3 * b
h₄ : d' = 2 * a' + b'
h₅ : e = a + b
h₆ : e' = 3 * a' + b'
h₇ : f = a + 2 * b
h₈ : f' = 3 * a' + 2 * b'
ha₁ :
  a = 0 ∧ a' = 0 ∨
    a = 1 ∧ a' = 1 ∨
      a = -1 ∧ a' = -1 ∨
        a = 1 ∧ a' = 2 ∨
          a = 2 ∧ a' = 1 ∨
            a = -1 ∧ a' = -2 ∨ a = -2 ∧ a' = -1 ∨ a = 1 ∧ a' = 3 ∨ a = 3 ∧ a' = 1 ∨ a = -1 ∧ a' = -3 ∨ a = -3 ∧ a' = -1
hb₁ :
  b = 0 ∧ b' = 0 ∨
    b = 1 ∧ b' = 1 ∨
      b = -1 ∧ b' = -1 ∨
        b = 1 ∧ b' = 2 ∨
          b = 2 ∧ b' = 1 ∨
            b = -1 ∧ b' = -2 ∨ b = -2 ∧ b' = -1 ∨ b = 1 ∧ b' = 3 ∨ b = 3 ∧ b' = 1 ∨ b = -1 ∧ b' = -3 ∨ b = -3 ∧ b' = -1
hc₁ :
  c = 0 ∧ c' = 0 ∨
    c = 1 ∧ c' = 1 ∨
      c = -1 ∧ c' = -1 ∨
        c = 1 ∧ c' = 2 ∨
          c = 2 ∧ c' = 1 ∨
            c = -1 ∧ c' = -2 ∨ c = -2 ∧ c' = -1 ∨ c = 1 ∧ c' = 3 ∨ c = 3 ∧ c' = 1 ∨ c = -1 ∧ c' = -3 ∨ c = -3 ∧ c' = -1
hd₁ :
  d = 0 ∧ d' = 0 ∨
    d = 1 ∧ d' = 1 ∨
      d = -1 ∧ d' = -1 ∨
        d = 1 ∧ d' = 2 ∨
          d = 2 ∧ d' = 1 ∨
            d = -1 ∧ d' = -2 ∨ d = -2 ∧ d' = -1 ∨ d = 1 ∧ d' = 3 ∨ d = 3 ∧ d' = 1 ∨ d = -1 ∧ d' = -3 ∨ d = -3 ∧ d' = -1
⊢ e = 0 ∧ e' = 0 ∨
    e = 1 ∧ e' = 1 ∨
      e = -1 ∧ e' = -1 ∨
        e = 1 ∧ e' = 2 ∨
          e = 2 ∧ e' = 1 ∨
            e = -1 ∧ e' = -2 ∨ e = -2 ∧ e' = -1 ∨ e = 1 ∧ e' = 3 ∨ e = 3 ∧ e' = 1 ∨ e = -1 ∧ e' = -3 ∨ e = -3 ∧ e' = -1

Tactic:
simp [S_def] at ha hb hc hd he hf
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
Goal:
a b c d e f a' b' c' d' e' f' : ℤ
S : Set (ℤ × ℤ)
S_def : S = {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
ha : (a, a') ∈ S
hb : (b, b') ∈ S
hc : (c, c') ∈ S
hd : (d, d') ∈ S
he : (e, e') ∈ S
hf : (f, f') ∈ S
h₁ : c = a + 3 * b
h₂ : c' = a' + b'
h₃ : d = 2 * a + 3 * b
h₄ : d' = 2 * a' + b'
h₅ : e = a + b
h₆ : e' = 3 * a' + b'
h₇ : f = a + 2 * b
h₈ : f' = 3 * a' + 2 * b'
ha₁ :
  a = 0 ∧ a' = 0 ∨
    a = 1 ∧ a' = 1 ∨
      a = -1 ∧ a' = -1 ∨
        a = 1 ∧ a' = 2 ∨
          a = 2 ∧ a' = 1 ∨
            a = -1 ∧ a' = -2 ∨ a = -2 ∧ a' = -1 ∨ a = 1 ∧ a' = 3 ∨ a = 3 ∧ a' = 1 ∨ a = -1 ∧ a' = -3 ∨ a = -3 ∧ a' = -1
hb₁ :
  b = 0 ∧ b' = 0 ∨
    b = 1 ∧ b' = 1 ∨
      b = -1 ∧ b' = -1 ∨
        b = 1 ∧ b' = 2 ∨
          b = 2 ∧ b' = 1 ∨
            b = -1 ∧ b' = -2 ∨ b = -2 ∧ b' = -1 ∨ b = 1 ∧ b' = 3 ∨ b = 3 ∧ b' = 1 ∨ b = -1 ∧ b' = -3 ∨ b = -3 ∧ b' = -1
hc₁ :
  c = 0 ∧ c' = 0 ∨
    c = 1 ∧ c' = 1 ∨
      c = -1 ∧ c' = -1 ∨
        c = 1 ∧ c' = 2 ∨
          c = 2 ∧ c' = 1 ∨
            c = -1 ∧ c' = -2 ∨ c = -2 ∧ c' = -1 ∨ c = 1 ∧ c' = 3 ∨ c = 3 ∧ c' = 1 ∨ c = -1 ∧ c' = -3 ∨ c = -3 ∧ c' = -1
hd₁ :
  d = 0 ∧ d' = 0 ∨
    d = 1 ∧ d' = 1 ∨
      d = -1 ∧ d' = -1 ∨
        d = 1 ∧ d' = 2 ∨
          d = 2 ∧ d' = 1 ∨
            d = -1 ∧ d' = -2 ∨ d = -2 ∧ d' = -1 ∨ d = 1 ∧ d' = 3 ∨ d = 3 ∧ d' = 1 ∨ d = -1 ∧ d' = -3 ∨ d = -3 ∧ d' = -1
he₁ :
  e = 0 ∧ e' = 0 ∨
    e = 1 ∧ e' = 1 ∨
      e = -1 ∧ e' = -1 ∨
        e = 1 ∧ e' = 2 ∨
          e = 2 ∧ e' = 1 ∨
            e = -1 ∧ e' = -2 ∨ e = -2 ∧ e' = -1 ∨ e = 1 ∧ e' = 3 ∨ e = 3 ∧ e' = 1 ∨ e = -1 ∧ e' = -3 ∨ e = -3 ∧ e' = -1
⊢ f = 0 ∧ f' = 0 ∨
    f = 1 ∧ f' = 1 ∨
      f = -1 ∧ f' = -1 ∨
        f = 1 ∧ f' = 2 ∨
          f = 2 ∧ f' = 1 ∨
            f = -1 ∧ f' = -2 ∨ f = -2 ∧ f' = -1 ∨ f = 1 ∧ f' = 3 ∨ f = 3 ∧ f' = 1 ∨ f = -1 ∧ f' = -3 ∨ f = -3 ∧ f' = -1

Tactic:
simp [S_def] at ha hb hc hd he hf
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2
Goal:
a b c d e f a' b' c' d' e' f' : ℤ
S : Set (ℤ × ℤ)
S_def : S = {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
h₁ : c = a + 3 * b
h₂ : c' = a' + b'
h₃ : d = 2 * a + 3 * b
h₄ : d' = 2 * a' + b'
h₅ : e = a + b
h₆ : e' = 3 * a' + b'
h₇ : f = a + 2 * b
h₈ : f' = 3 * a' + 2 * b'
ha :
  a = 0 ∧ a' = 0 ∨
    a = 1 ∧ a' = 1 ∨
      a = -1 ∧ a' = -1 ∨
        a = 1 ∧ a' = 2 ∨
          a = 2 ∧ a' = 1 ∨
            a = -1 ∧ a' = -2 ∨ a = -2 ∧ a' = -1 ∨ a = 1 ∧ a' = 3 ∨ a = 3 ∧ a' = 1 ∨ a = -1 ∧ a' = -3 ∨ a = -3 ∧ a' = -1
hb :
  b = 0 ∧ b' = 0 ∨
    b = 1 ∧ b' = 1 ∨
      b = -1 ∧ b' = -1 ∨
        b = 1 ∧ b' = 2 ∨
          b = 2 ∧ b' = 1 ∨
            b = -1 ∧ b' = -2 ∨ b = -2 ∧ b' = -1 ∨ b = 1 ∧ b' = 3 ∨ b = 3 ∧ b' = 1 ∨ b = -1 ∧ b' = -3 ∨ b = -3 ∧ b' = -1
hc :
  c = 0 ∧ c' = 0 ∨
    c = 1 ∧ c' = 1 ∨
      c = -1 ∧ c' = -1 ∨
        c = 1 ∧ c' = 2 ∨
          c = 2 ∧ c' = 1 ∨
            c = -1 ∧ c' = -2 ∨ c = -2 ∧ c' = -1 ∨ c = 1 ∧ c' = 3 ∨ c = 3 ∧ c' = 1 ∨ c = -1 ∧ c' = -3 ∨ c = -3 ∧ c' = -1
hd :
  d = 0 ∧ d' = 0 ∨
    d = 1 ∧ d' = 1 ∨
      d = -1 ∧ d' = -1 ∨
        d = 1 ∧ d' = 2 ∨
          d = 2 ∧ d' = 1 ∨
            d = -1 ∧ d' = -2 ∨ d = -2 ∧ d' = -1 ∨ d = 1 ∧ d' = 3 ∨ d = 3 ∧ d' = 1 ∨ d = -1 ∧ d' = -3 ∨ d = -3 ∧ d' = -1
he :
  e = 0 ∧ e' = 0 ∨
    e = 1 ∧ e' = 1 ∨
      e = -1 ∧ e' = -1 ∨
        e = 1 ∧ e' = 2 ∨
          e = 2 ∧ e' = 1 ∨
            e = -1 ∧ e' = -2 ∨ e = -2 ∧ e' = -1 ∨ e = 1 ∧ e' = 3 ∨ e = 3 ∧ e' = 1 ∨ e = -1 ∧ e' = -3 ∨ e = -3 ∧ e' = -1
hf :
  f = 0 ∧ f' = 0 ∨
    f = 1 ∧ f' = 1 ∨
      f = -1 ∧ f' = -1 ∨
        f = 1 ∧ f' = 2 ∨
          f = 2 ∧ f' = 1 ∨
            f = -1 ∧ f' = -2 ∨ f = -2 ∧ f' = -1 ∨ f = 1 ∧ f' = 3 ∨ f = 3 ∧ f' = 1 ∨ f = -1 ∧ f' = -3 ∨ f = -3 ∧ f' = -1
⊢ a = 0 ∧ b = 0

Tactic:
omega
-- 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.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
⊢ Module.IsReflexive R M

Tactic:
have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
-- 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.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
hi : ((P.root : (a : ι) → M) i : M) ∉ allRoots P
this_1 : P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0
this : Module.IsReflexive R M
⊢ P.IsOrthogonal i (short P) ∧ P.IsOrthogonal i (long P)

Tactic:
simpa [isOrthogonal_iff_pairing_eq_zero, ← P.algebraMap_pairingIn ℤ]

Premises used: RootPairing.algebraMap_pairingIn, Int, RootPairing.isOrthogonal_iff_pairing_eq_zero
-- 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.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
hi : ((P.root : (a : ι) → M) i : M) ∉ allRoots P
suffices : P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0
⊢ P.IsOrthogonal i (short P) ∧ P.IsOrthogonal i (long P)

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 ℤ]
-- 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.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
hi : ((P.root : (a : ι) → M) i : M) ∉ allRoots P
⊢ ¬(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

Premises used: not_or, or_false, List.mem_cons, List.not_mem_nil