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 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
this : Fintype ι
⊢ P.pairing i (shortAddLong P) = P.pairing i (short P) + 3 * P.pairing i (long P)
have have : ∀ (B : P.InvariantForm), P.pairing i (shortAddLong P) = P.pairing i (short P) + 3 * 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 (shortAddLong P) = P.pairing i (short P) + 3 * P.pairing i (long P)
have 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)
Tactic: apply mul_right_cancel₀ (B.ne_zero (shortAddLong 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 (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)
have 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) (β := 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: calc P.pairing i (shortAddLong P) * B.form (P.root (shortAddLong P)) (P.root (shortAddLong P))
    _ = 2 * B.form (P.root i) (shortAddLongRoot P) := ?_
    _ = 2 * B.form (P.root i) (shortRoot P) + 2 * B.form (P.root i) (longRoot P) := ?_
    _ = P.pairing i (short P) * B.form (shortRoot P) (shortRoot P) +
          P.pairing i (long P) * B.form (longRoot P) (longRoot P) := ?_
    _ = (P.pairing i (short P) + 3 * P.pairing i (long P)) *
          B.form (shortAddLongRoot P) (shortAddLongRoot 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 (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)
⊢ 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)
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) (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: calc P.pairing i (shortAddLong P) * B.form (P.root (shortAddLong P)) (P.root (shortAddLong P))
    _ = 2 * B.form (P.root i) (shortAddLongRoot P) := ?_
    _ = 2 * B.form (P.root i) (shortRoot P) + 2 * B.form (P.root i) (longRoot P) := ?_
    _ = P.pairing i (short P) * B.form (shortRoot P) (shortRoot P) +
          P.pairing i (long P) * B.form (longRoot P) (longRoot P) := ?_
    _ = (P.pairing i (short P) + 3 * P.pairing i (long P)) *
          B.form (shortAddLongRoot P) (shortAddLongRoot 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 (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)
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) (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)
⊢ 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)
have calc_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) (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: calc P.pairing i (shortAddLong P) * B.form (P.root (shortAddLong P)) (P.root (shortAddLong P))
    _ = 2 * B.form (P.root i) (shortAddLongRoot P) := ?_
    _ = 2 * B.form (P.root i) (shortRoot P) + 2 * B.form (P.root i) (longRoot P) := ?_
    _ = P.pairing i (short P) * B.form (shortRoot P) (shortRoot P) +
          P.pairing i (long P) * B.form (longRoot P) (longRoot P) := ?_
    _ = (P.pairing i (short P) + 3 * P.pairing i (long P)) *
          B.form (shortAddLongRoot P) (shortAddLongRoot 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 (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)
have 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)
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) (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)
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)
        (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)
Tactic: rw [shortAddLongRoot_eq, map_add, mul_add]
-- 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_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)
⊢ 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)
have 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)
Tactic: rw [shortAddLongRoot_eq, map_add, mul_add]
-- 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_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)
⊢ 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)
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) (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)
Tactic: rw [shortAddLongRoot_eq, map_add, mul_add]
-- 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) (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)
have 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)
Tactic: rw [B.two_mul_apply_root_root, 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
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)
⊢ 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)
have 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)
Tactic: rw [B.two_mul_apply_root_root, 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) (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)
have 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)
Tactic: rw [long_eq_three_mul_short, shortAddLongRoot_shortRoot]
-- 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 ℤ (twoShortAddLong P) i = 2 * P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i
have 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
Tactic: rw [pairingIn_eq_add_of_root_eq_smul_add_smul (x := 2) (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 : 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
⊢ P.pairingIn ℤ (twoShortAddLong P) i = 2 * P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i
have 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)
Tactic: rw [pairingIn_eq_add_of_root_eq_smul_add_smul (x := 2) (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 : Finite ι
inst_7 : CharZero R
inst_8 : IsDomain R
i : ι
⊢ (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)
have simp : HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (shortRoot P) =
  HSMul.hSMul (α := ℤ) (β := M) 2 ((P.root : (a : ι) → M) (short P) : M)
Tactic: simp only [twoShortAddLongRoot_eq, one_smul, add_left_inj]