-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear (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 : Fintype ι
i : ι
rw :
  HSMul.hSMul (α := ℕ) (β := M) 4
      ((P.CoPolarization ∘ₗ P.Polarization : (a : M) → M) ((P.root : (a : ι) → M) i : M) : M) =
    HSMul.hSMul (β := M)
      (HMul.hMul (α := R) (β := R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)
        ((((P.CorootForm : (a : N) → N →ₗ[R] R) ((P.coroot : (a : ι) → N) i) : N →ₗ[R] R) : (a : N) → R)
            ((P.coroot : (a : ι) → N) i : N) :
          R))
      ((P.root : (a : ι) → M) i : M)
rw₁ :
  HSMul.hSMul (α := ℕ) (β := M) 4
      ((P.CoPolarization : (a : N) → M) ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) : M) =
    HSMul.hSMul (β := M)
      (HMul.hMul (α := R) (β := R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)
        ((((P.CorootForm : (a : N) → N →ₗ[R] R) ((P.coroot : (a : ι) → N) i) : N →ₗ[R] R) : (a : N) → R)
            ((P.coroot : (a : ι) → N) i : N) :
          R))
      ((P.root : (a : ι) → M) i : M)
rw₂ :
  HSMul.hSMul (β := M) (HMul.hMul (α := ℕ) 2 2)
      ((P.CoPolarization : (a : N) → M) ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) : M) =
    HSMul.hSMul (β := M)
      (HMul.hMul (α := R) (β := R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)
        ((((P.CorootForm : (a : N) → N →ₗ[R] R) ((P.coroot : (a : ι) → N) i) : N →ₗ[R] R) : (a : N) → R)
            ((P.coroot : (a : ι) → N) i : N) :
          R))
      ((P.root : (a : ι) → M) i : M)
rw₃ :
  HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul (α := ℕ) (β := M) 2
        ((P.CoPolarization : (a : N) → M) ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) : M)) =
    HSMul.hSMul (β := M)
      (HMul.hMul (α := R) (β := R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)
        ((((P.CorootForm : (a : N) → N →ₗ[R] R) ((P.coroot : (a : ι) → N) i) : N →ₗ[R] R) : (a : N) → R)
            ((P.coroot : (a : ι) → N) i : N) :
          R))
      ((P.root : (a : ι) → M) i : M)
rw₄ :
  HSMul.hSMul (α := ℕ) (β := M) 2
      ((P.CoPolarization : (a : N) → M)
          (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) :
        M) =
    HSMul.hSMul (β := M)
      (HMul.hMul (α := R) (β := R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)
        ((((P.CorootForm : (a : N) → N →ₗ[R] R) ((P.coroot : (a : ι) → N) i) : N →ₗ[R] R) : (a : N) → R)
            ((P.coroot : (a : ι) → N) i : N) :
          R))
      ((P.root : (a : ι) → M) i : M)
rw₅ :
  HSMul.hSMul (α := ℕ) (β := M) 2
      ((P.CoPolarization : (a : N) → M)
          (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
            ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
                ((P.root : (a : ι) → M) i : M) :
              R)
            ((P.coroot : (a : ι) → N) i : N)) :
        M) =
    HSMul.hSMul (β := M)
      (HMul.hMul (α := R) (β := R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)
        ((((P.CorootForm : (a : N) → N →ₗ[R] R) ((P.coroot : (a : ι) → N) i) : N →ₗ[R] R) : (a : N) → R)
            ((P.coroot : (a : ι) → N) i : N) :
          R))
      ((P.root : (a : ι) → M) i : M)
rw₆ :
  HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)
        ((P.CoPolarization : (a : N) → M) ((P.coroot : (a : ι) → N) i : N) : M)) =
    HSMul.hSMul (β := M)
      (HMul.hMul (α := R) (β := R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)
        ((((P.CorootForm : (a : N) → N →ₗ[R] R) ((P.coroot : (a : ι) → N) i) : N →ₗ[R] R) : (a : N) → R)
            ((P.coroot : (a : ι) → N) i : N) :
          R))
      ((P.root : (a : ι) → M) i : M)
rw₇ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R)
      (HSMul.hSMul (α := ℕ) (β := M) 2 ((P.CoPolarization : (a : N) → M) ((P.coroot : (a : ι) → N) i : N) : M)) =
    HSMul.hSMul (β := M)
      (HMul.hMul (α := R) (β := R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)
        ((((P.CorootForm : (a : N) → N →ₗ[R] R) ((P.coroot : (a : ι) → N) i) : N →ₗ[R] R) : (a : N) → R)
            ((P.coroot : (a : ι) → N) i : N) :
          R))
      ((P.root : (a : ι) → M) i : M)
⊢ (HSMul.hSMul (α := ℕ) 4 (P.CoPolarization ∘ₗ P.Polarization) : (a : M) → M) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul (β := M)
      (HMul.hMul (α := R) (β := R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)
        ((((P.CorootForm : (a : N) → N →ₗ[R] R) ((P.coroot : (a : ι) → N) i) : N →ₗ[R] R) : (a : N) → R)
            ((P.coroot : (a : ι) → N) i : N) :
          R))
      ((P.root : (a : ι) → M) i : M)
have rw₈ : HSMul.hSMul.{u_2, u_3, u_3} (α := R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.CorootForm : (a : N) → N →ₗ[R] R) ((P.coroot : (a : ι) → N) i) : N →ₗ[R] R) : (a : N) → R)
          ((P.coroot : (a : ι) → N) i : N) :
        R)
      ((P.root : (a : ι) → M) i : M)) =
  HSMul.hSMul (β := M)
    (HMul.hMul (α := R) (β := R)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R)
      ((((P.CorootForm : (a : N) → N →ₗ[R] R) ((P.coroot : (a : ι) → N) i) : N →ₗ[R] R) : (a : N) → R)
          ((P.coroot : (a : ι) → N) i : N) :
        R))
    ((P.root : (a : ι) → M) i : M)
Tactic: rw [LinearMap.smul_apply, LinearMap.comp_apply, show 4 = 2 * 2 from rfl, mul_smul, ← map_nsmul,
    ← rootForm_self_smul_coroot, map_smul, smul_comm, ← corootForm_self_smul_root, smul_smul]