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
calc_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) +
      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)
calc_3₁ calc_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) +
      HMul.hMul (β := R) (P.pairing i (long P))
        ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (long P)) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) (long P) : M) :
          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)
⊢ 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:
rw [B.two_mul_apply_root_root, 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_4 :
  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) +
      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) =
    HMul.hMul (β := R) (P.pairing i (short P) + 3 * P.pairing i (long 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 (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:
rw [long_eq_three_mul_short, shortAddLongRoot_shortRoot]

Premises used: RootPairing.EmbeddedG2.shortAddLongRoot_shortRoot, RootPairing.EmbeddedG2.long_eq_three_mul_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
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) +
      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) =
    HMul.hMul (β := R) (P.pairing i (short P) + 3 * P.pairing i (long P))
      ((((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 : ι
rw :
  HSMul.hSMul (α := ℤ) 2 (P.pairingIn ℤ (short P) i) + HSMul.hSMul (α := ℤ) 1 (P.pairingIn ℤ (long P) i) =
    2 * P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i
rw₁ :
  (P.root : (a : ι) → M) (twoShortAddLong P) =
    HSMul.hSMul (α := ℤ) (β := M) 2 ((P.root : (a : ι) → M) (short P) : M) +
      HSMul.hSMul (α := ℤ) (β := M) 1 ((P.root : (a : ι) → M) (long P) : M)
⊢ P.pairingIn ℤ (twoShortAddLong P) i = 2 * P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i

Tactic:
rw [pairingIn_eq_add_of_root_eq_smul_add_smul (x := 2) (y := 1) (i := short P) (l := long P)]

Premises used: RootPairing.pairingIn_eq_add_of_root_eq_smul_add_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 : ι
⊢ HSMul.hSMul (α := ℤ) 2 (P.pairingIn ℤ (short P) i) + HSMul.hSMul (α := ℤ) 1 (P.pairingIn ℤ (long 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 : ι
simp :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (shortRoot P) =
    HSMul.hSMul (α := ℤ) (β := M) 2 ((P.root : (a : ι) → M) (short P) : M)
⊢ (P.root : (a : ι) → M) (twoShortAddLong P) =
    HSMul.hSMul (α := ℤ) (β := M) 2 ((P.root : (a : ι) → M) (short P) : M) +
      HSMul.hSMul (α := ℤ) (β := M) 1 ((P.root : (a : ι) → M) (long P) : M)

Tactic:
simp only [twoShortAddLongRoot_eq, one_smul, add_left_inj]

Premises used: RootPairing.EmbeddedG2.twoShortAddLongRoot_eq, add_left_inj, one_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 : ι
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  HSMul.hSMul (α := ℕ) 2 (shortRoot P) = HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) (short P) : M)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (shortRoot P) =
    HSMul.hSMul (α := ℤ) (β := M) 2 ((P.root : (a : ι) → M) (short P) : M)

Tactic:
norm_cast
-- 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 (twoShortAddLong P) = 2 * P.pairing i (short P) + 3 * P.pairing i (long P)
⊢ Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ i (twoShortAddLong P)) : R)
    ((algebraMap ℤ R : (a : ℤ) → R) (2 * 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 (twoShortAddLong P) = 2 * P.pairing i (short P) + 3 * P.pairing i (long P)
⊢ P.pairingIn ℤ i (twoShortAddLong P) = 2 * P.pairingIn ℤ i (short P) + 3 * P.pairingIn ℤ i (long P)

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

Tactic:
apply mul_right_cancel₀ (B.ne_zero <| twoShortAddLong P)

Premises used: RootPairing.EmbeddedG2.twoShortAddLong, RootPairing.InvariantForm.ne_zero, 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 (twoShortAddLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) (twoShortAddLongRoot P) : M →ₗ[R] R) : (a : M) → R) (twoShortAddLongRoot 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) (twoShortAddLongRoot 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) (twoShortAddLongRoot 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) (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
⊢ 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) (2 * 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) (2 * 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) (2 * P.pairing i (short P) + 3 * P.pairing i (long P))
      ((((B.form : (a : M) → M →ₗ[R] R) (twoShortAddLongRoot P) : M →ₗ[R] R) : (a : M) → R) (twoShortAddLongRoot 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 (twoShortAddLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) (twoShortAddLongRoot P) : M →ₗ[R] R) : (a : M) → R) (twoShortAddLongRoot P) :
        R) =
    HMul.hMul (β := R) (P.pairing i (twoShortAddLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (twoShortAddLong P)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (twoShortAddLong P) : M) :
        R)
⊢ HMul.hMul (β := R) (P.pairing i (twoShortAddLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) (twoShortAddLongRoot P) : M →ₗ[R] R) : (a : M) → R) (twoShortAddLongRoot 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) (twoShortAddLongRoot 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_4 :
  HMul.hMul (β := R) (2 * P.pairing i (short P))
        ((((B.form : (a : M) → M →ₗ[R] R) (shortRoot P) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R) +
      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) =
    HMul.hMul (β := R) (2 * P.pairing i (short P) + 3 * P.pairing i (long P))
      ((((B.form : (a : M) → M →ₗ[R] R) (shortRoot P) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R)
⊢ HMul.hMul (β := R) (2 * 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) (2 * P.pairing i (short P) + 3 * P.pairing i (long P))
      ((((B.form : (a : M) → M →ₗ[R] R) (twoShortAddLongRoot P) : M →ₗ[R] R) : (a : M) → R) (twoShortAddLongRoot P) : R)

Tactic:
rw [long_eq_three_mul_short, twoShortAddLongRoot_shortRoot]

Premises used: RootPairing.EmbeddedG2.long_eq_three_mul_short, RootPairing.EmbeddedG2.twoShortAddLongRoot_shortRoot
-- 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) (2 * P.pairing i (short P))
        ((((B.form : (a : M) → M →ₗ[R] R) (shortRoot P) : M →ₗ[R] R) : (a : M) → R) (shortRoot P) : R) +
      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) =
    HMul.hMul (β := R) (2 * P.pairing i (short P) + 3 * P.pairing i (long P))
      ((((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 : CharZero R
i : ι
rw :
  HSMul.hSMul (α := ℤ) 3 (P.pairingIn ℤ (short P) i) + HSMul.hSMul (α := ℤ) 1 (P.pairingIn ℤ (long P) i) =
    3 * P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i
rw₁ :
  (P.root : (a : ι) → M) (threeShortAddLong P) =
    HSMul.hSMul (α := ℤ) (β := M) 3 ((P.root : (a : ι) → M) (short P) : M) +
      HSMul.hSMul (α := ℤ) (β := M) 1 ((P.root : (a : ι) → M) (long P) : M)
⊢ P.pairingIn ℤ (threeShortAddLong P) i = 3 * P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i

Tactic:
rw [pairingIn_eq_add_of_root_eq_smul_add_smul (x := 3) (y := 1) (i := short P) (l := long P)]

Premises used: RootPairing.pairingIn_eq_add_of_root_eq_smul_add_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 : CharZero R
i : ι
⊢ HSMul.hSMul (α := ℤ) 3 (P.pairingIn ℤ (short P) i) + HSMul.hSMul (α := ℤ) 1 (P.pairingIn ℤ (long 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 : CharZero R
i : ι
simp :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) 3 (shortRoot P) =
    HSMul.hSMul (α := ℤ) (β := M) 3 ((P.root : (a : ι) → M) (short P) : M)
⊢ (P.root : (a : ι) → M) (threeShortAddLong P) =
    HSMul.hSMul (α := ℤ) (β := M) 3 ((P.root : (a : ι) → M) (short P) : M) +
      HSMul.hSMul (α := ℤ) (β := M) 1 ((P.root : (a : ι) → M) (long P) : M)

Tactic:
simp only [threeShortAddLongRoot_eq, one_smul, add_left_inj]

Premises used: add_left_inj, one_smul, RootPairing.EmbeddedG2.threeShortAddLongRoot_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 : CharZero R
i : ι
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  HSMul.hSMul (α := ℕ) 3 (shortRoot P) = HSMul.hSMul (α := ℕ) (β := M) 3 ((P.root : (a : ι) → M) (short P) : M)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) 3 (shortRoot P) =
    HSMul.hSMul (α := ℤ) (β := M) 3 ((P.root : (a : ι) → M) (short P) : M)

Tactic:
norm_cast
-- 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 (threeShortAddLong P) = P.pairing i (short P) + P.pairing i (long P)
⊢ Eq (α := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ i (threeShortAddLong P)) : R)
    ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ i (short P) + 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 (threeShortAddLong P) = P.pairing i (short P) + P.pairing i (long P)
⊢ P.pairingIn ℤ i (threeShortAddLong P) = P.pairingIn ℤ i (short P) + P.pairingIn ℤ i (long P)

Tactic:
suffices P.pairing i (threeShortAddLong P) =
      P.pairing i (short P) + 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 (threeShortAddLong P) = P.pairing i (short P) + P.pairing i (long P)
⊢ P.pairing i (threeShortAddLong P) = P.pairing i (short P) + 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 (threeShortAddLong P) = P.pairing i (short P) + P.pairing i (long P)
⊢ P.pairing i (threeShortAddLong P) = P.pairing i (short P) + P.pairing i (long P)

Tactic:
have B := (P.posRootForm ℤ).toInvariantForm