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
⊢ LinearIndependent ℤ ![shortRoot P, longRoot P]

Tactic:
(linearIndependent_short_long P).restrict_scalars' ℤ

Premises used: RootPairing.EmbeddedG2.linearIndependent_short_long, Int, LinearIndependent.restrict_scalars'
-- 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
⊢ LinearIndependent ℤ ![shortRoot P, longRoot P]

Tactic:
exact (linearIndependent_short_long P).restrict_scalars' ℤ

Premises used: RootPairing.EmbeddedG2.linearIndependent_short_long, Int, LinearIndependent.restrict_scalars'
-- 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
⊢ Injective (α := Fin (Nat.succ 0).succ → ℤ) (β := M)
    (⇑(Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) : (a : Fin (Nat.succ 0).succ → ℤ) → M)

Tactic:
have hli : Injective (Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) := by
    rw [← linearIndependent_iff_injective_fintypeLinearCombination]
    exact (linearIndependent_short_long P).restrict_scalars' ℤ
-- 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
hli :
  Injective (α := Fin (Nat.succ 0).succ → ℤ) (β := M)
    (⇑(Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) : (a : Fin (Nat.succ 0).succ → ℤ) → M)
rw : allCoeffs.Nodup
⊢ (allRoots P).Nodup

Tactic:
rw [allRoots_eq_map_allCoeffs, nodup_map_iff hli]

Premises used: RootPairing.EmbeddedG2.allRoots_eq_map_allCoeffs, List.nodup_map_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.EmbeddedG2
inst_6 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
hli :
  Injective (α := Fin (Nat.succ 0).succ → ℤ) (β := M)
    (⇑(Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) : (a : Fin (Nat.succ 0).succ → ℤ) → M)
⊢ allCoeffs.Nodup

Tactic:
decide
-- 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
x : M
hx : x ∈ allRoots P
⊢ {longRoot P, shortRoot P} = Set.range ![shortRoot P, longRoot 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
x : M
hx : x ∈ allRoots P
⊢ {longRoot P, shortRoot P} = Set.range ![shortRoot P, longRoot P]

Tactic:
have : {longRoot P, shortRoot P} = range ![shortRoot P, longRoot P] := by 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
x : M
hx : x ∈ allRoots P
this : {longRoot P, shortRoot P} = Set.range ![shortRoot P, longRoot P]
simp_rw :
  ∃ (c : Fin (Nat.succ 0).succ → ℤ),
    (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin (Nat.succ 0).succ → ℤ) → M) c = x
⊢ Membership.mem (γ := Submodule ℤ M) (Submodule.span ℤ {longRoot P, shortRoot P}) x

Tactic:
simp_rw [this, Submodule.mem_span_range_iff_exists_fun, ← Fintype.linearCombination_apply]

Premises used: Submodule.mem_span_range_iff_exists_fun, Fintype.linearCombination_apply
-- 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
x : M
hx : x ∈ allRoots P
this : {longRoot P, shortRoot P} = Set.range ![shortRoot P, longRoot P]
⊢ x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![0, 1] ∨
    x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![0, -1] ∨
      x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![1, 0] ∨
        x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![-1, 0] ∨
          x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![1, 1] ∨
            x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![-1, -1] ∨
              x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![2, 1] ∨
                x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![-2, -1] ∨
                  x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![3, 1] ∨
                    x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![-3, -1] ∨
                      x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![3, 2] ∨
                        x = (Fintype.linearCombination ℤ ![shortRoot P, longRoot P] : (a : Fin 2 → ℤ) → M) ![-3, -2]

Tactic:
simp [allRoots_eq_map_allCoeffs] at hx

Premises used: RootPairing.EmbeddedG2.allRoots_eq_map_allCoeffs
-- 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
B : P.InvariantForm
⊢ (((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot 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:
simpa using B.pairing_mul_eq_pairing_mul_swap (long P) (short P)

Premises used: RootPairing.InvariantForm.pairing_mul_eq_pairing_mul_swap, RootPairing.EmbeddedG2.long, RootPairing.EmbeddedG2.short
-- 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
B : P.InvariantForm
⊢ Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) (shortAddLongRoot P) : M →ₗ[R] R) : (a : M) → R) (shortAddLongRoot P) : R)
    ((((B.form : (a : M) → M →ₗ[R] R) (shortRoot P) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R)

Tactic:
simp [shortAddLongRoot, shortAddLong]

Premises used: RootPairing.EmbeddedG2.shortAddLongRoot, RootPairing.EmbeddedG2.shortAddLong
-- 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
B : P.InvariantForm
⊢ Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) (twoShortAddLongRoot P) : M →ₗ[R] R) : (a : M) → R) (twoShortAddLongRoot P) : R)
    ((((B.form : (a : M) → M →ₗ[R] R) (shortRoot P) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R)

Tactic:
simp [twoShortAddLongRoot, twoShortAddLong]

Premises used: RootPairing.EmbeddedG2.twoShortAddLong, RootPairing.EmbeddedG2.twoShortAddLongRoot
-- 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
B : P.InvariantForm
⊢ Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) (threeShortAddLongRoot P) : M →ₗ[R] R) : (a : M) → R) (threeShortAddLongRoot P) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R)

Tactic:
simp [threeShortAddLongRoot, threeShortAddLong]

Premises used: RootPairing.EmbeddedG2.threeShortAddLong, RootPairing.EmbeddedG2.threeShortAddLongRoot
-- 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
B : P.InvariantForm
⊢ Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) (threeShortAddTwoLongRoot P) : M →ₗ[R] R) : (a : M) → R)
        (threeShortAddTwoLongRoot P) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R)

Tactic:
simp [threeShortAddTwoLongRoot, threeShortAddTwoLong]

Premises used: RootPairing.EmbeddedG2.threeShortAddTwoLong, RootPairing.EmbeddedG2.threeShortAddTwoLongRoot
-- 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 : ι
rw rw₁ : P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i = P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i
⊢ P.pairingIn ℤ (shortAddLong P) i = P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i

Tactic:
rw [pairingIn_eq_add_of_root_eq_add (shortAddLongRoot_eq P)]

Premises used: RootPairing.pairingIn_eq_add_of_root_eq_add, RootPairing.EmbeddedG2.shortAddLongRoot_eq
-- 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 : P.pairing i (shortAddLong P) = P.pairing i (short P) + 3 * P.pairing i (long P)
⊢ Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ i (shortAddLong P)) : R)
    ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ i (short P) + 3 * P.pairingIn ℤ i (long P)) : R)

Tactic:
simpa only [algebraMap_pairingIn, map_add, map_mul, map_ofNat]

Premises used: map_ofNat, map_add, RootPairing.algebraMap_pairingIn, map_mul
-- 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 : ι
suffices : P.pairing i (shortAddLong P) = P.pairing i (short P) + 3 * P.pairing i (long P)
⊢ P.pairingIn ℤ i (shortAddLong P) = P.pairingIn ℤ i (short P) + 3 * P.pairingIn ℤ i (long P)

Tactic:
suffices P.pairing i (shortAddLong P) = P.pairing i (short P) + 3 * P.pairing i (long P) from
    algebraMap_injective ℤ R <| by simpa only [algebraMap_pairingIn, map_add, map_mul, map_ofNat]
-- 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 : ι
have : ∀ (this : Fintype ι), P.pairing i (shortAddLong P) = P.pairing i (short P) + 3 * P.pairing i (long P)
⊢ P.pairing i (shortAddLong P) = P.pairing i (short P) + 3 * P.pairing i (long P)

Tactic:
have : Fintype ι := Fintype.ofFinite ι
-- 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 ι
have : ∀ (B : P.InvariantForm), P.pairing i (shortAddLong P) = P.pairing i (short P) + 3 * P.pairing i (long P)
⊢ P.pairing i (shortAddLong P) = P.pairing i (short P) + 3 * P.pairing i (long P)

Tactic:
have B := (P.posRootForm ℤ).toInvariantForm
-- 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
apply :
  HMul.hMul (β := R) (P.pairing i (shortAddLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (shortAddLong P)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (shortAddLong P) : M) :
        R) =
    HMul.hMul (β := R) (P.pairing i (short P) + 3 * P.pairing i (long P))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (shortAddLong P)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (shortAddLong P) : M) :
        R)
⊢ P.pairing i (shortAddLong P) = P.pairing i (short P) + 3 * P.pairing i (long P)

Tactic:
apply mul_right_cancel₀ (B.ne_zero (shortAddLong P))

Premises used: RootPairing.InvariantForm.ne_zero, RootPairing.EmbeddedG2.shortAddLong, mul_right_cancel₀
-- 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 (shortAddLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (shortAddLong P)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (shortAddLong P) : M) :
        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) (shortAddLongRoot 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
⊢ HMul.hMul (α := R) (β := R) (2 : R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (shortAddLongRoot 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) (shortRoot 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) (longRoot 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
⊢ 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) +
      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) (shortRoot P) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R) +
      HMul.hMul (β := R) (P.pairing i (long P))
        ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot 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
⊢ HMul.hMul (β := R) (P.pairing i (short P))
        ((((B.form : (a : M) → M →ₗ[R] R) (shortRoot P) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R) +
      HMul.hMul (β := R) (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) + 3 * P.pairing i (long P))
      ((((B.form : (a : M) → M →ₗ[R] R) (shortAddLongRoot P) : M →ₗ[R] R) : (a : M) → R) (shortAddLongRoot 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 (shortAddLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (shortAddLong P)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (shortAddLong P) : M) :
        R) =
    HMul.hMul (β := R) (P.pairing i (shortAddLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (shortAddLong P)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (shortAddLong P) : M) :
        R)
⊢ HMul.hMul (β := R) (P.pairing i (shortAddLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (shortAddLong P)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (shortAddLong P) : M) :
        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) (shortAddLongRoot 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 :
  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 + 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) (shortRoot 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) (longRoot P) : R)
calc_2₁ :
  2 *
      HAdd.hAdd (α := R) (β := R)
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : 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) (shortRoot 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) (longRoot P) : R)
calc_2₂ calc_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) (shortRoot 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) (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) (shortRoot 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) (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) (shortAddLongRoot 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) (shortRoot 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) (longRoot P) : R)

Tactic:
rw [shortAddLongRoot_eq, map_add, mul_add]

Premises used: map_add, mul_add, RootPairing.EmbeddedG2.shortAddLongRoot_eq