-- 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)
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)
⊢ 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_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) (threeShortAddLongRoot P) : 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) := ?_