-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Rayleigh (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
T : F →L[ℝ] F
hT : LinearMap.IsSymmetric.{0, u_3} (𝕜 := ℝ) (E := F) (↑T : F →ₗ[ℝ] F)
x₀ : F
e_8 : Real.instAddCommGroup = Ring.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
y : F
h :
  HSMul.hSMul (α := ℕ) (β := ℝ) 2
      ((((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) : (a : F) → ℝ) y : ℝ) =
    (fderivInnerCLM ℝ ((T : (a : F) → F) x₀, id x₀) ∘SL T.prod (ContinuousLinearMap.id ℝ F) : (a : F) → ℝ) y
h₁ :
  HSMul.hSMul (α := ℕ) (β := ℝ) 2
      ((((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) : (a : F) → ℝ) y : ℝ) =
    (fderivInnerCLM ℝ ((T : (a : F) → F) x₀, id x₀) : (a : F × F) → ℝ)
      ((T.prod (ContinuousLinearMap.id ℝ F) : (a : F) → F × F) y : F × F)
h₂ :
  HSMul.hSMul (α := ℕ) (β := ℝ) 2
      ((((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) : (a : F) → ℝ) y : ℝ) =
    inner ℝ (E := F) (((T : (a : F) → F) x₀, id x₀).1 : F)
        (((T.prod (ContinuousLinearMap.id ℝ F) : (a : F) → F × F) y).2 : F) +
      ⟪((T.prod (ContinuousLinearMap.id ℝ F) : (a : F) → F × F) y).1, (((T : (a : F) → F) x₀, id x₀) : F × F).2⟫_ℝ
h₃ :
  HSMul.hSMul (α := ℕ) (β := ℝ) 2
      ((((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) : (a : F) → ℝ) y : ℝ) =
    inner ℝ (E := F) (((T : (a : F) → F) x₀, id x₀).1 : F)
        (((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).2 : F) +
      ⟪((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).1,
        (((T : (a : F) → F) x₀, id x₀) : F × F).2⟫_ℝ
h₄ :
  HSMul.hSMul (α := ℕ) 2 ⟪(T : (a : F) → F) x₀, y⟫_ℝ =
    inner ℝ (E := F) (((T : (a : F) → F) x₀, id x₀).1 : F)
        (((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).2 : F) +
      ⟪((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).1,
        (((T : (a : F) → F) x₀, id x₀) : F × F).2⟫_ℝ
h₅ :
  HSMul.hSMul (α := ℕ) 2 ⟪(T : (a : F) → F) x₀, y⟫_ℝ =
    inner ℝ (E := F) (((T : (a : F) → F) x₀, x₀).1 : F)
        (((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).2 : F) +
      ⟪((T : (a : F) → F) y, (ContinuousLinearMap.id ℝ F : (a : F) → F) y).1, (((T : (a : F) → F) x₀, x₀) : F × F).2⟫_ℝ
h₆ :
  HSMul.hSMul (α := ℕ) 2 ⟪(T : (a : F) → F) x₀, y⟫_ℝ =
    ⟪((T : (a : F) → F) x₀, x₀).1, (((T : (a : F) → F) y, y) : F × F).2⟫_ℝ +
      ⟪((T : (a : F) → F) y, y).1, (((T : (a : F) → F) x₀, x₀) : F × F).2⟫_ℝ
⊢ Eq (α := ℝ)
    ((HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
            ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) ((T : (a : F) → F) x₀ : F) : F →L[ℝ] ℝ) :
          (a : F) → ℝ)
        y :
      ℝ)
    ((fderivInnerCLM ℝ ((T : (a : F) → F) x₀, id x₀) ∘SL T.prod (ContinuousLinearMap.id ℝ F) : (a : F) → ℝ) y : ℝ)
have h₇ : HSMul.hSMul (α := ℕ) 2 ⟪x₀, (T : (a : F) → F) y⟫_ℝ =
  ⟪x₀, (T : (a : F) → F) y⟫_ℝ + ⟪((T : (a : F) → F) y, y).1, (((T : (a : F) → F) x₀, x₀) : F × F).2⟫_ℝ
Tactic: rw [ContinuousLinearMap.smul_apply, ContinuousLinearMap.comp_apply, fderivInnerCLM_apply,
    ContinuousLinearMap.prod_apply, innerSL_apply_apply, id, ContinuousLinearMap.id_apply,
    hT.apply_clm x₀ y, real_inner_comm _ x₀, two_smul]