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 : ι
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
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)
hb :
  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 (long P), P.pairingIn ℤ (long P) i)
hc :
  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 (shortAddLong P), P.pairingIn ℤ (shortAddLong P) i)
hd :
  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 (twoShortAddLong P), P.pairingIn ℤ (twoShortAddLong P) i)
⊢ 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 (threeShortAddLong P), P.pairingIn ℤ (threeShortAddLong P) i)

Tactic:
have he := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed' i (threeShortAddLong P) ‹_› ‹_›
-- 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 : ι
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
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)
hb :
  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 (long P), P.pairingIn ℤ (long P) i)
hc :
  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 (shortAddLong P), P.pairingIn ℤ (shortAddLong P) i)
hd :
  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 (twoShortAddLong P), P.pairingIn ℤ (twoShortAddLong P) i)
he :
  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 (threeShortAddLong P), P.pairingIn ℤ (threeShortAddLong P) i)
⊢ 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 (threeShortAddTwoLong P), P.pairingIn ℤ (threeShortAddTwoLong P) i)

Tactic:
have hf := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed' i (threeShortAddTwoLong P) ‹_› ‹_›
-- 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 : ι
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
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)
hb :
  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 (long P), P.pairingIn ℤ (long P) i)
hc :
  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 (shortAddLong P), P.pairingIn ℤ (shortAddLong P) i)
hd :
  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 (twoShortAddLong P), P.pairingIn ℤ (twoShortAddLong P) i)
he :
  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 (threeShortAddLong P), P.pairingIn ℤ (threeShortAddLong P) i)
hf :
  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 (threeShortAddTwoLong P), P.pairingIn ℤ (threeShortAddTwoLong P) i)
⊢ P.pairingIn ℤ i (shortAddLong P) = P.pairingIn ℤ i (short P) + 3 * P.pairingIn ℤ i (long P)

Tactic:
simp
-- 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 : ι
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
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)
hb :
  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 (long P), P.pairingIn ℤ (long P) i)
hc :
  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 (shortAddLong P), P.pairingIn ℤ (shortAddLong P) i)
hd :
  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 (twoShortAddLong P), P.pairingIn ℤ (twoShortAddLong P) i)
he :
  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 (threeShortAddLong P), P.pairingIn ℤ (threeShortAddLong P) i)
hf :
  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 (threeShortAddTwoLong P), P.pairingIn ℤ (threeShortAddTwoLong P) i)
⊢ P.pairingIn ℤ (shortAddLong P) i = P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i

Tactic:
simp
-- 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 : ι
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
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)
hb :
  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 (long P), P.pairingIn ℤ (long P) i)
hc :
  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 (shortAddLong P), P.pairingIn ℤ (shortAddLong P) i)
hd :
  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 (twoShortAddLong P), P.pairingIn ℤ (twoShortAddLong P) i)
he :
  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 (threeShortAddLong P), P.pairingIn ℤ (threeShortAddLong P) i)
hf :
  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 (threeShortAddTwoLong P), P.pairingIn ℤ (threeShortAddTwoLong P) i)
⊢ P.pairingIn ℤ i (twoShortAddLong P) = 2 * P.pairingIn ℤ i (short P) + 3 * P.pairingIn ℤ i (long P)

Tactic:
simp
-- 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 : ι
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
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)
hb :
  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 (long P), P.pairingIn ℤ (long P) i)
hc :
  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 (shortAddLong P), P.pairingIn ℤ (shortAddLong P) i)
hd :
  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 (twoShortAddLong P), P.pairingIn ℤ (twoShortAddLong P) i)
he :
  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 (threeShortAddLong P), P.pairingIn ℤ (threeShortAddLong P) i)
hf :
  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 (threeShortAddTwoLong P), P.pairingIn ℤ (threeShortAddTwoLong P) i)
⊢ P.pairingIn ℤ (twoShortAddLong P) i = 2 * P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i

Tactic:
simp
-- 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 : ι
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
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)
hb :
  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 (long P), P.pairingIn ℤ (long P) i)
hc :
  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 (shortAddLong P), P.pairingIn ℤ (shortAddLong P) i)
hd :
  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 (twoShortAddLong P), P.pairingIn ℤ (twoShortAddLong P) i)
he :
  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 (threeShortAddLong P), P.pairingIn ℤ (threeShortAddLong P) i)
hf :
  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 (threeShortAddTwoLong P), P.pairingIn ℤ (threeShortAddTwoLong P) i)
⊢ P.pairingIn ℤ i (threeShortAddLong P) = P.pairingIn ℤ i (short P) + P.pairingIn ℤ i (long P)

Tactic:
simp
-- 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 : ι
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
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)
hb :
  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 (long P), P.pairingIn ℤ (long P) i)
hc :
  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 (shortAddLong P), P.pairingIn ℤ (shortAddLong P) i)
hd :
  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 (twoShortAddLong P), P.pairingIn ℤ (twoShortAddLong P) i)
he :
  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 (threeShortAddLong P), P.pairingIn ℤ (threeShortAddLong P) i)
hf :
  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 (threeShortAddTwoLong P), P.pairingIn ℤ (threeShortAddTwoLong P) i)
⊢ P.pairingIn ℤ (threeShortAddLong P) i = 3 * P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i

Tactic:
simp
-- 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 : ι
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
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)
hb :
  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 (long P), P.pairingIn ℤ (long P) i)
hc :
  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 (shortAddLong P), P.pairingIn ℤ (shortAddLong P) i)
hd :
  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 (twoShortAddLong P), P.pairingIn ℤ (twoShortAddLong P) i)
he :
  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 (threeShortAddLong P), P.pairingIn ℤ (threeShortAddLong P) i)
hf :
  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 (threeShortAddTwoLong P), P.pairingIn ℤ (threeShortAddTwoLong P) i)
⊢ P.pairingIn ℤ i (threeShortAddTwoLong P) = P.pairingIn ℤ i (short P) + 2 * P.pairingIn ℤ i (long P)

Tactic:
simp
-- 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 : ι
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
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)
hb :
  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 (long P), P.pairingIn ℤ (long P) i)
hc :
  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 (shortAddLong P), P.pairingIn ℤ (shortAddLong P) i)
hd :
  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 (twoShortAddLong P), P.pairingIn ℤ (twoShortAddLong P) i)
he :
  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 (threeShortAddLong P), P.pairingIn ℤ (threeShortAddLong P) i)
hf :
  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 (threeShortAddTwoLong P), P.pairingIn ℤ (threeShortAddTwoLong P) i)
⊢ P.pairingIn ℤ (threeShortAddTwoLong P) i = 3 * P.pairingIn ℤ (short P) i + 2 * P.pairingIn ℤ (long P) i

Tactic:
simp
-- 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
inst_9 : P.IsIrreducible
⊢ Set.Nonempty (α := ι) {long P, short P}

Tactic:
simp