-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
rw :
  HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ)
        (HAdd.hAdd (β := ℝ) (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t) ((re : (a : 𝕜) → ℝ) ((↑t : 𝕜) * ⟪x, y⟫) : ℝ))
        ((re : (a : 𝕜) → ℝ) (⟪y, x⟫ * (↑t : 𝕜)) : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) =
    HAdd.hAdd (β := ℝ)
      (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) t +
        HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) t)
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
rw₁ :
  HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ) (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (β := ℝ) t ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ))
        ((re : (a : 𝕜) → ℝ) (⟪y, x⟫ * (↑t : 𝕜)) : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) =
    HAdd.hAdd (β := ℝ)
      (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) t +
        HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) t)
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
rw₂ :
  HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ) (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) t)
        ((re : (a : 𝕜) → ℝ) (⟪y, x⟫ * (↑t : 𝕜)) : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) =
    HAdd.hAdd (β := ℝ)
      (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) t +
        HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) t)
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
rw₃ :
  HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ) (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) t)
        ((re : (a : 𝕜) → ℝ) ((↑t : 𝕜) * ⟪y, x⟫) : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) =
    HAdd.hAdd (β := ℝ)
      (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) t +
        HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) t)
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
rw₄ :
  HAdd.hAdd (β := ℝ)
      (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) t +
        HMul.hMul (β := ℝ) t ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) =
    HAdd.hAdd (β := ℝ)
      (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) t +
        HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) t)
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
⊢ HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ)
        (HAdd.hAdd (β := ℝ) (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t) ((re : (a : 𝕜) → ℝ) (⟪x, y⟫ * (↑t : 𝕜)) : ℝ))
        ((re : (a : 𝕜) → ℝ) (⟪y, x⟫ * (↑t : 𝕜)) : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) =
    HAdd.hAdd (β := ℝ)
      (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) t +
        HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) t)
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
have rw₅ : HAdd.hAdd (β := ℝ)
    (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) t +
      HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) t)
    ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) =
  HAdd.hAdd (β := ℝ)
    (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) t +
      HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) t)
    ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
Tactic: rw [mul_comm ⟪x, y⟫ _,
    RCLike.re_ofReal_mul, mul_comm t _, mul_comm ⟪y, x⟫ _, RCLike.re_ofReal_mul, mul_comm t _]