awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
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 : ι
⊢ P.pairingIn ℤ (threeShortAddLong P) i = 3 * P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i
have 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
Tactic: rw [pairingIn_eq_add_of_root_eq_smul_add_smul (x := 3) (y := 1) (i := short P) (l := long P)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
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
⊢ P.pairingIn ℤ (threeShortAddLong P) i = 3 * P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i
have 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)
Tactic: rw [pairingIn_eq_add_of_root_eq_smul_add_smul (x := 3) (y := 1) (i := short P) (l := long P)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
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 : ι
⊢ (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)
have simp : HSMul.hSMul.{u_2, u_3, u_3} (α := R) 3 (shortRoot P) =
  HSMul.hSMul (α := ℤ) (β := M) 3 ((P.root : (a : ι) → M) (short P) : M)
Tactic: simp only [threeShortAddLongRoot_eq, one_smul, add_left_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
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.{u_2, u_3, u_3} (α := R) 3 (shortRoot P) =
    HSMul.hSMul (α := ℤ) (β := M) 3 ((P.root : (a : ι) → M) (short P) : M)
have norm_cast : HSMul.hSMul (α := ℕ) 3 (shortRoot P) = HSMul.hSMul (α := ℕ) (β := M) 3 ((P.root : (a : ι) → M) (short P) : M)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
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 : ι
⊢ P.pairingIn ℤ i (threeShortAddLong P) = P.pairingIn ℤ i (short P) + P.pairingIn ℤ i (long P)
have suffices : P.pairing i (threeShortAddLong P) = P.pairing i (short P) + P.pairing 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
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 : ι
⊢ P.pairing i (threeShortAddLong P) = P.pairing i (short P) + P.pairing i (long P)
have have : ∀ (this : Fintype ι), P.pairing i (threeShortAddLong P) = P.pairing i (short P) + P.pairing i (long P)
Tactic: have : Fintype ι := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
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 ι
⊢ P.pairing i (threeShortAddLong P) = P.pairing i (short P) + P.pairing i (long P)
have have : ∀ (B : P.InvariantForm), P.pairing i (threeShortAddLong P) = P.pairing i (short P) + P.pairing i (long P)
Tactic: have B := (P.posRootForm ℤ).toInvariantForm
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
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
⊢ P.pairing i (threeShortAddLong P) = P.pairing i (short P) + P.pairing i (long P)
have apply : HMul.hMul (β := R) (P.pairing i (threeShortAddLong P))
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (threeShortAddLong P)) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) (threeShortAddLong P) : M) :
      R) =
  HMul.hMul (β := R) (P.pairing i (short P) + P.pairing i (long P))
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (threeShortAddLong P)) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) (threeShortAddLong P) : M) :
      R)
Tactic: apply mul_right_cancel₀ (B.ne_zero <| threeShortAddLong P)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
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 (threeShortAddLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (threeShortAddLong P)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (threeShortAddLong P) : M) :
        R) =
    HMul.hMul (β := R) (P.pairing i (short P) + P.pairing i (long P))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (threeShortAddLong P)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (threeShortAddLong P) : M) :
        R)
have calc_1 : HMul.hMul (β := R) (P.pairing i (threeShortAddLong P))
    ((((B.form : (a : M) → M →ₗ[R] R) (threeShortAddLongRoot P) : M →ₗ[R] R) : (a : M) → R) (threeShortAddLongRoot 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) (threeShortAddLongRoot P) :
      R)
Tactic: calc P.pairing i (threeShortAddLong P) *
          B.form (threeShortAddLongRoot P) (threeShortAddLongRoot P)
    _ = 2 * B.form (P.root i) (threeShortAddLongRoot P) := ?_
    _ = 3 * (2 * B.form (P.root i) (shortRoot P)) + 2 * B.form (P.root i) (longRoot P) := ?_
    _ = P.pairing i (short P) * B.form (longRoot P) (longRoot P) +
          P.pairing i (long P) * B.form (longRoot P) (longRoot P) := ?_
    _ = (P.pairing i (short P) + P.pairing i (long P)) *
          B.form (threeShortAddLongRoot P) (threeShortAddLongRoot P) := ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
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 :
  HMul.hMul (β := R) (P.pairing i (threeShortAddLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) (threeShortAddLongRoot P) : M →ₗ[R] R) : (a : M) → R)
          (threeShortAddLongRoot 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)
          (threeShortAddLongRoot P) :
        R)
⊢ HMul.hMul (β := R) (P.pairing i (threeShortAddLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (threeShortAddLong P)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (threeShortAddLong P) : M) :
        R) =
    HMul.hMul (β := R) (P.pairing i (short P) + P.pairing i (long P))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (threeShortAddLong P)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (threeShortAddLong P) : M) :
        R)
have 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) (threeShortAddLongRoot 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) +
    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: calc P.pairing i (threeShortAddLong P) *
          B.form (threeShortAddLongRoot P) (threeShortAddLongRoot P)
    _ = 2 * B.form (P.root i) (threeShortAddLongRoot P) := ?_
    _ = 3 * (2 * B.form (P.root i) (shortRoot P)) + 2 * B.form (P.root i) (longRoot P) := ?_
    _ = P.pairing i (short P) * B.form (longRoot P) (longRoot P) +
          P.pairing i (long P) * B.form (longRoot P) (longRoot P) := ?_
    _ = (P.pairing i (short P) + P.pairing i (long P)) *
          B.form (threeShortAddLongRoot P) (threeShortAddLongRoot P) := ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
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 :
  HMul.hMul (β := R) (P.pairing i (threeShortAddLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) (threeShortAddLongRoot P) : M →ₗ[R] R) : (a : M) → R)
          (threeShortAddLongRoot 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)
          (threeShortAddLongRoot P) :
        R)
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)
          (threeShortAddLongRoot 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) +
      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 (threeShortAddLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (threeShortAddLong P)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (threeShortAddLong P) : M) :
        R) =
    HMul.hMul (β := R) (P.pairing i (short P) + P.pairing i (long P))
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (threeShortAddLong P)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (threeShortAddLong P) : M) :
        R)
have calc_3 : 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) +
    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) (P.pairing i (long P))
      ((((B.form : (a : M) → M →ₗ[R] R) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot P) : R)
Tactic: calc P.pairing i (threeShortAddLong P) *
          B.form (threeShortAddLongRoot P) (threeShortAddLongRoot P)
    _ = 2 * B.form (P.root i) (threeShortAddLongRoot P) := ?_
    _ = 3 * (2 * B.form (P.root i) (shortRoot P)) + 2 * B.form (P.root i) (longRoot P) := ?_
    _ = P.pairing i (short P) * B.form (longRoot P) (longRoot P) +
          P.pairing i (long P) * B.form (longRoot P) (longRoot P) := ?_
    _ = (P.pairing i (short P) + P.pairing i (long P)) *
          B.form (threeShortAddLongRoot P) (threeShortAddLongRoot P) := ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
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 (threeShortAddLong P))
      ((((B.form : (a : M) → M →ₗ[R] R) (threeShortAddLongRoot P) : M →ₗ[R] R) : (a : M) → R)
          (threeShortAddLongRoot 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)
          (threeShortAddLongRoot P) :
        R)
have calc_1 : HMul.hMul (β := R) (P.pairing i (threeShortAddLong P))
    ((((B.form : (a : M) → M →ₗ[R] R) (threeShortAddLongRoot P) : M →ₗ[R] R) : (a : M) → R) (threeShortAddLongRoot P) :
      R) =
  HMul.hMul (β := R) (P.pairing i (threeShortAddLong P))
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (threeShortAddLong P)) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) (threeShortAddLong P) : M) :
      R)
Tactic: rw [B.two_mul_apply_root_root]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
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)
          (threeShortAddLongRoot 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) +
      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)
have 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) +
    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) +
    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 [threeShortAddLongRoot_eq, map_add, mul_add, map_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
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) (β := 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) (longRoot P) : M →ₗ[R] R) : (a : M) → R) (longRoot 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)
have 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) +
    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) +
    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: rw [B.two_mul_apply_root_root, B.two_mul_apply_root_root, long_eq_three_mul_short]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
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) (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) + P.pairing i (long P))
      ((((B.form : (a : M) → M →ₗ[R] R) (threeShortAddLongRoot P) : M →ₗ[R] R) : (a : M) → R)
          (threeShortAddLongRoot P) :
        R)
have 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) (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) + 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 [threeShortAddLongRoot_longRoot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
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 : ι
⊢ P.pairingIn ℤ (threeShortAddTwoLong P) i = 3 * P.pairingIn ℤ (short P) i + 2 * P.pairingIn ℤ (long P) i
have rw : HSMul.hSMul (α := ℤ) 3 (P.pairingIn ℤ (short P) i) + HSMul.hSMul (α := ℤ) 2 (P.pairingIn ℤ (long P) i) =
  3 * P.pairingIn ℤ (short P) i + 2 * P.pairingIn ℤ (long P) i
Tactic: rw [pairingIn_eq_add_of_root_eq_smul_add_smul (x := 3) (y := 2) (i := short P) (l := long P)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
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 (α := ℤ) 3 (P.pairingIn ℤ (short P) i) + HSMul.hSMul (α := ℤ) 2 (P.pairingIn ℤ (long P) i) =
    3 * P.pairingIn ℤ (short P) i + 2 * P.pairingIn ℤ (long P) i
⊢ P.pairingIn ℤ (threeShortAddTwoLong P) i = 3 * P.pairingIn ℤ (short P) i + 2 * P.pairingIn ℤ (long P) i
have rw₁ : (P.root : (a : ι) → M) (threeShortAddTwoLong P) =
  HSMul.hSMul (α := ℤ) (β := M) 3 ((P.root : (a : ι) → M) (short P) : M) +
    HSMul.hSMul (α := ℤ) (β := M) 2 ((P.root : (a : ι) → M) (long P) : M)
Tactic: rw [pairingIn_eq_add_of_root_eq_smul_add_smul (x := 3) (y := 2) (i := short P) (l := long P)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
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 : ι
⊢ (P.root : (a : ι) → M) (threeShortAddTwoLong P) =
    HSMul.hSMul (α := ℤ) (β := M) 3 ((P.root : (a : ι) → M) (short P) : M) +
      HSMul.hSMul (α := ℤ) (β := M) 2 ((P.root : (a : ι) → M) (long P) : M)
have simp : HSMul.hSMul.{u_2, u_3, u_3} (α := R) 3 (shortRoot P) + HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (longRoot P) =
  HSMul.hSMul (α := ℤ) (β := M) 3 ((P.root : (a : ι) → M) (short P) : M) +
    HSMul.hSMul (α := ℤ) (β := M) 2 ((P.root : (a : ι) → M) (long P) : M)
Tactic: simp only [threeShortAddTwoLongRoot_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
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.{u_2, u_3, u_3} (α := R) 3 (shortRoot P) + HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (longRoot P) =
    HSMul.hSMul (α := ℤ) (β := M) 3 ((P.root : (a : ι) → M) (short P) : M) +
      HSMul.hSMul (α := ℤ) (β := M) 2 ((P.root : (a : ι) → M) (long P) : M)
have norm_cast : HSMul.hSMul (α := ℕ) 3 (shortRoot P) + HSMul.hSMul (α := ℕ) 2 (longRoot P) =
  HSMul.hSMul (α := ℕ) (β := M) 3 ((P.root : (a : ι) → M) (short P) : M) +
    HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) (long P) : M)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
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 : ι
⊢ P.pairingIn ℤ i (threeShortAddTwoLong P) = P.pairingIn ℤ i (short P) + 2 * P.pairingIn ℤ i (long P)
have suffices : P.pairing i (threeShortAddTwoLong P) = P.pairing i (short P) + 2 * P.pairing i (long P)
Tactic: suffices P.pairing i (threeShortAddTwoLong P) =
      P.pairing i (short P) + 2 * P.pairing i (long P) from
    algebraMap_injective ℤ R <| by simpa only [algebraMap_pairingIn, map_add, map_mul, map_ofNat]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.G2 (goal)
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 : ι
⊢ P.pairing i (threeShortAddTwoLong P) = P.pairing i (short P) + 2 * P.pairing i (long P)
have have : ∀ (this : Fintype ι), P.pairing i (threeShortAddTwoLong P) = P.pairing i (short P) + 2 * P.pairing i (long P)
Tactic: have : Fintype ι := Fintype.ofFinite ι