Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
h₁ : ¬P.root i = longRoot P
h₂ : ¬P.root i = -longRoot P
h₃ : ¬P.root i = shortRoot P
h₄ : ¬P.root i = -shortRoot P
h₅ : ¬P.root i = shortAddLongRoot P
h₆ : ¬P.root i = -shortAddLongRoot P
h₇ : ¬P.root i = twoShortAddLongRoot P
h₈ : ¬P.root i = -twoShortAddLongRoot P
h₉ : ¬P.root i = threeShortAddLongRoot P
h₁₀ : ¬P.root i = -threeShortAddLongRoot P
h₁₁ : ¬P.root i = threeShortAddTwoLongRoot P
h₁₂ : ¬P.root i = -threeShortAddTwoLongRoot P
ha :
  (P.pairingIn ℤ i (short P), P.pairingIn ℤ (short P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hb :
  (P.pairingIn ℤ i (long P), P.pairingIn ℤ (long P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hc :
  (P.pairingIn ℤ i (shortAddLong P), P.pairingIn ℤ (shortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hd :
  (P.pairingIn ℤ i (twoShortAddLong P), P.pairingIn ℤ (twoShortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
he :
  (P.pairingIn ℤ i (threeShortAddLong P), P.pairingIn ℤ (threeShortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hf :
  (P.pairingIn ℤ i (threeShortAddTwoLong P), P.pairingIn ℤ (threeShortAddTwoLong P) i) ∈
    {(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) = 0 ∧ P.pairingIn ℤ i (long P) = 0

Tactic:
apply isOrthogonal_short_and_long_aux rfl ha hb hc hd he hf

Goal state after:
case h₁
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
h₁ : ¬P.root i = longRoot P
h₂ : ¬P.root i = -longRoot P
h₃ : ¬P.root i = shortRoot P
h₄ : ¬P.root i = -shortRoot P
h₅ : ¬P.root i = shortAddLongRoot P
h₆ : ¬P.root i = -shortAddLongRoot P
h₇ : ¬P.root i = twoShortAddLongRoot P
h₈ : ¬P.root i = -twoShortAddLongRoot P
h₉ : ¬P.root i = threeShortAddLongRoot P
h₁₀ : ¬P.root i = -threeShortAddLongRoot P
h₁₁ : ¬P.root i = threeShortAddTwoLongRoot P
h₁₂ : ¬P.root i = -threeShortAddTwoLongRoot P
ha :
  (P.pairingIn ℤ i (short P), P.pairingIn ℤ (short P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hb :
  (P.pairingIn ℤ i (long P), P.pairingIn ℤ (long P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hc :
  (P.pairingIn ℤ i (shortAddLong P), P.pairingIn ℤ (shortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hd :
  (P.pairingIn ℤ i (twoShortAddLong P), P.pairingIn ℤ (twoShortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
he :
  (P.pairingIn ℤ i (threeShortAddLong P), P.pairingIn ℤ (threeShortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hf :
  (P.pairingIn ℤ i (threeShortAddTwoLong P), P.pairingIn ℤ (threeShortAddTwoLong P) i) ∈
    {(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 ℤ i (short P) + 3 * P.pairingIn ℤ i (long P)

case h₂
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
h₁ : ¬P.root i = longRoot P
h₂ : ¬P.root i = -longRoot P
h₃ : ¬P.root i = shortRoot P
h₄ : ¬P.root i = -shortRoot P
h₅ : ¬P.root i = shortAddLongRoot P
h₆ : ¬P.root i = -shortAddLongRoot P
h₇ : ¬P.root i = twoShortAddLongRoot P
h₈ : ¬P.root i = -twoShortAddLongRoot P
h₉ : ¬P.root i = threeShortAddLongRoot P
h₁₀ : ¬P.root i = -threeShortAddLongRoot P
h₁₁ : ¬P.root i = threeShortAddTwoLongRoot P
h₁₂ : ¬P.root i = -threeShortAddTwoLongRoot P
ha :
  (P.pairingIn ℤ i (short P), P.pairingIn ℤ (short P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hb :
  (P.pairingIn ℤ i (long P), P.pairingIn ℤ (long P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hc :
  (P.pairingIn ℤ i (shortAddLong P), P.pairingIn ℤ (shortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hd :
  (P.pairingIn ℤ i (twoShortAddLong P), P.pairingIn ℤ (twoShortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
he :
  (P.pairingIn ℤ i (threeShortAddLong P), P.pairingIn ℤ (threeShortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hf :
  (P.pairingIn ℤ i (threeShortAddTwoLong P), P.pairingIn ℤ (threeShortAddTwoLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
⊢ P.pairingIn ℤ (shortAddLong P) i = P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i

case h₃
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
h₁ : ¬P.root i = longRoot P
h₂ : ¬P.root i = -longRoot P
h₃ : ¬P.root i = shortRoot P
h₄ : ¬P.root i = -shortRoot P
h₅ : ¬P.root i = shortAddLongRoot P
h₆ : ¬P.root i = -shortAddLongRoot P
h₇ : ¬P.root i = twoShortAddLongRoot P
h₈ : ¬P.root i = -twoShortAddLongRoot P
h₉ : ¬P.root i = threeShortAddLongRoot P
h₁₀ : ¬P.root i = -threeShortAddLongRoot P
h₁₁ : ¬P.root i = threeShortAddTwoLongRoot P
h₁₂ : ¬P.root i = -threeShortAddTwoLongRoot P
ha :
  (P.pairingIn ℤ i (short P), P.pairingIn ℤ (short P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hb :
  (P.pairingIn ℤ i (long P), P.pairingIn ℤ (long P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hc :
  (P.pairingIn ℤ i (shortAddLong P), P.pairingIn ℤ (shortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hd :
  (P.pairingIn ℤ i (twoShortAddLong P), P.pairingIn ℤ (twoShortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
he :
  (P.pairingIn ℤ i (threeShortAddLong P), P.pairingIn ℤ (threeShortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hf :
  (P.pairingIn ℤ i (threeShortAddTwoLong P), P.pairingIn ℤ (threeShortAddTwoLong P) i) ∈
    {(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) = 2 * P.pairingIn ℤ i (short P) + 3 * P.pairingIn ℤ i (long P)

case h₄
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
h₁ : ¬P.root i = longRoot P
h₂ : ¬P.root i = -longRoot P
h₃ : ¬P.root i = shortRoot P
h₄ : ¬P.root i = -shortRoot P
h₅ : ¬P.root i = shortAddLongRoot P
h₆ : ¬P.root i = -shortAddLongRoot P
h₇ : ¬P.root i = twoShortAddLongRoot P
h₈ : ¬P.root i = -twoShortAddLongRoot P
h₉ : ¬P.root i = threeShortAddLongRoot P
h₁₀ : ¬P.root i = -threeShortAddLongRoot P
h₁₁ : ¬P.root i = threeShortAddTwoLongRoot P
h₁₂ : ¬P.root i = -threeShortAddTwoLongRoot P
ha :
  (P.pairingIn ℤ i (short P), P.pairingIn ℤ (short P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hb :
  (P.pairingIn ℤ i (long P), P.pairingIn ℤ (long P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hc :
  (P.pairingIn ℤ i (shortAddLong P), P.pairingIn ℤ (shortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hd :
  (P.pairingIn ℤ i (twoShortAddLong P), P.pairingIn ℤ (twoShortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
he :
  (P.pairingIn ℤ i (threeShortAddLong P), P.pairingIn ℤ (threeShortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hf :
  (P.pairingIn ℤ i (threeShortAddTwoLong P), P.pairingIn ℤ (threeShortAddTwoLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
⊢ P.pairingIn ℤ (twoShortAddLong P) i = 2 * P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i

case h₅
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
h₁ : ¬P.root i = longRoot P
h₂ : ¬P.root i = -longRoot P
h₃ : ¬P.root i = shortRoot P
h₄ : ¬P.root i = -shortRoot P
h₅ : ¬P.root i = shortAddLongRoot P
h₆ : ¬P.root i = -shortAddLongRoot P
h₇ : ¬P.root i = twoShortAddLongRoot P
h₈ : ¬P.root i = -twoShortAddLongRoot P
h₉ : ¬P.root i = threeShortAddLongRoot P
h₁₀ : ¬P.root i = -threeShortAddLongRoot P
h₁₁ : ¬P.root i = threeShortAddTwoLongRoot P
h₁₂ : ¬P.root i = -threeShortAddTwoLongRoot P
ha :
  (P.pairingIn ℤ i (short P), P.pairingIn ℤ (short P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hb :
  (P.pairingIn ℤ i (long P), P.pairingIn ℤ (long P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hc :
  (P.pairingIn ℤ i (shortAddLong P), P.pairingIn ℤ (shortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hd :
  (P.pairingIn ℤ i (twoShortAddLong P), P.pairingIn ℤ (twoShortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
he :
  (P.pairingIn ℤ i (threeShortAddLong P), P.pairingIn ℤ (threeShortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hf :
  (P.pairingIn ℤ i (threeShortAddTwoLong P), P.pairingIn ℤ (threeShortAddTwoLong P) i) ∈
    {(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 ℤ i (short P) + P.pairingIn ℤ i (long P)

case h₆
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
h₁ : ¬P.root i = longRoot P
h₂ : ¬P.root i = -longRoot P
h₃ : ¬P.root i = shortRoot P
h₄ : ¬P.root i = -shortRoot P
h₅ : ¬P.root i = shortAddLongRoot P
h₆ : ¬P.root i = -shortAddLongRoot P
h₇ : ¬P.root i = twoShortAddLongRoot P
h₈ : ¬P.root i = -twoShortAddLongRoot P
h₉ : ¬P.root i = threeShortAddLongRoot P
h₁₀ : ¬P.root i = -threeShortAddLongRoot P
h₁₁ : ¬P.root i = threeShortAddTwoLongRoot P
h₁₂ : ¬P.root i = -threeShortAddTwoLongRoot P
ha :
  (P.pairingIn ℤ i (short P), P.pairingIn ℤ (short P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hb :
  (P.pairingIn ℤ i (long P), P.pairingIn ℤ (long P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hc :
  (P.pairingIn ℤ i (shortAddLong P), P.pairingIn ℤ (shortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hd :
  (P.pairingIn ℤ i (twoShortAddLong P), P.pairingIn ℤ (twoShortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
he :
  (P.pairingIn ℤ i (threeShortAddLong P), P.pairingIn ℤ (threeShortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hf :
  (P.pairingIn ℤ i (threeShortAddTwoLong P), P.pairingIn ℤ (threeShortAddTwoLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
⊢ P.pairingIn ℤ (threeShortAddLong P) i = 3 * P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i

case h₇
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
h₁ : ¬P.root i = longRoot P
h₂ : ¬P.root i = -longRoot P
h₃ : ¬P.root i = shortRoot P
h₄ : ¬P.root i = -shortRoot P
h₅ : ¬P.root i = shortAddLongRoot P
h₆ : ¬P.root i = -shortAddLongRoot P
h₇ : ¬P.root i = twoShortAddLongRoot P
h₈ : ¬P.root i = -twoShortAddLongRoot P
h₉ : ¬P.root i = threeShortAddLongRoot P
h₁₀ : ¬P.root i = -threeShortAddLongRoot P
h₁₁ : ¬P.root i = threeShortAddTwoLongRoot P
h₁₂ : ¬P.root i = -threeShortAddTwoLongRoot P
ha :
  (P.pairingIn ℤ i (short P), P.pairingIn ℤ (short P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hb :
  (P.pairingIn ℤ i (long P), P.pairingIn ℤ (long P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hc :
  (P.pairingIn ℤ i (shortAddLong P), P.pairingIn ℤ (shortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hd :
  (P.pairingIn ℤ i (twoShortAddLong P), P.pairingIn ℤ (twoShortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
he :
  (P.pairingIn ℤ i (threeShortAddLong P), P.pairingIn ℤ (threeShortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hf :
  (P.pairingIn ℤ i (threeShortAddTwoLong P), P.pairingIn ℤ (threeShortAddTwoLong P) i) ∈
    {(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 ℤ i (short P) + 2 * P.pairingIn ℤ i (long P)

case h₈
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
h₁ : ¬P.root i = longRoot P
h₂ : ¬P.root i = -longRoot P
h₃ : ¬P.root i = shortRoot P
h₄ : ¬P.root i = -shortRoot P
h₅ : ¬P.root i = shortAddLongRoot P
h₆ : ¬P.root i = -shortAddLongRoot P
h₇ : ¬P.root i = twoShortAddLongRoot P
h₈ : ¬P.root i = -twoShortAddLongRoot P
h₉ : ¬P.root i = threeShortAddLongRoot P
h₁₀ : ¬P.root i = -threeShortAddLongRoot P
h₁₁ : ¬P.root i = threeShortAddTwoLongRoot P
h₁₂ : ¬P.root i = -threeShortAddTwoLongRoot P
ha :
  (P.pairingIn ℤ i (short P), P.pairingIn ℤ (short P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hb :
  (P.pairingIn ℤ i (long P), P.pairingIn ℤ (long P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hc :
  (P.pairingIn ℤ i (shortAddLong P), P.pairingIn ℤ (shortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hd :
  (P.pairingIn ℤ i (twoShortAddLong P), P.pairingIn ℤ (twoShortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
he :
  (P.pairingIn ℤ i (threeShortAddLong P), P.pairingIn ℤ (threeShortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hf :
  (P.pairingIn ℤ i (threeShortAddTwoLong P), P.pairingIn ℤ (threeShortAddTwoLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
⊢ P.pairingIn ℤ (threeShortAddTwoLong P) i = 3 * P.pairingIn ℤ (short P) i + 2 * P.pairingIn ℤ (long P) i