-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
a : (i : Fin (Module.finrank 𝕜 E)) → E :=
  fun (i : Fin (Module.finrank 𝕜 E)) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑√(⋯.eigenvalues ⋯ i) : 𝕜)
      ((⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) i : E)
x : E
simp_rw :
  Eq (α := E) ((T : (a : E) → E) x : E)
    (∑ d : Fin (Module.finrank 𝕜 E),
        (((((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) (a d) : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) (a d) :
              E →L[𝕜] E) :
            (a : E) → E)
          x :
      E)
simp_rw₁ : Eq (α := E) ((T : (a : E) → E) x : E) (∑ x_1 : Fin (Module.finrank 𝕜 E), ⟪a x_1, x⟫ • a x_1 : E)
simp_rw₂ :
  Eq (α := E) ((T : (a : E) → E) x : E)
    (∑ x_1 : Fin (Module.finrank 𝕜 E),
        ⟪HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑√(⋯.eigenvalues ⋯ x_1) : 𝕜)
              ((⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) x_1 : E),
            x⟫ •
          HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑√(⋯.eigenvalues ⋯ x_1) : 𝕜)
            ((⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) x_1 : E) :
      E)
simp_rw₃ :
  Eq (α := E) ((T : (a : E) → E) x : E)
    (∑ x_1 : Fin (Module.finrank 𝕜 E),
        HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑√(⋯.eigenvalues ⋯ x_1) : 𝕜) : 𝕜)
            ⟪(⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) x_1, x⟫ •
          HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑√(⋯.eigenvalues ⋯ x_1) : 𝕜)
            ((⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) x_1 : E) :
      E)
simp_rw₄ :
  Eq (α := E) ((T : (a : E) → E) x : E)
    (∑ x_1 : Fin (Module.finrank 𝕜 E),
        HSMul.hSMul (β := E)
          (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑√(⋯.eigenvalues ⋯ x_1) : 𝕜) : 𝕜)
              ⟪(⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) x_1, x⟫ *
            (↑√(⋯.eigenvalues ⋯ x_1) : 𝕜))
          ((⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) x_1 : E) :
      E)
simp_rw₅ :
  Eq (α := E) ((T : (a : E) → E) x : E)
    (∑ x_1 : Fin (Module.finrank 𝕜 E),
        HSMul.hSMul (β := E)
          (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑√(⋯.eigenvalues ⋯ x_1) : 𝕜) : 𝕜)
            (⟪(⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) x_1, x⟫ * (↑√(⋯.eigenvalues ⋯ x_1) : 𝕜)))
          ((⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) x_1 : E) :
      E)
⊢ Eq (α := E) ((T : (a : E) → E) x : E)
    ((∑ i : Fin (Module.finrank 𝕜 E),
            (((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) (a i) : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) (a i) :
          (a : E) → E)
        x :
      E)
have simp_rw₆ : Eq (α := E) ((T : (a : E) → E) x : E)
  (∑ x_1 : Fin (Module.finrank 𝕜 E),
      HSMul.hSMul (β := E)
        ((↑√(sorry.eigenvalues sorry x_1) : 𝕜) *
          (⟪(sorry.eigenvectorBasis sorry : (a : Fin (Module.finrank 𝕜 E)) → E) x_1, x⟫ * (↑√(sorry.eigenvalues sorry x_1) : 𝕜)))
        ((sorry.eigenvectorBasis sorry : (a : Fin (Module.finrank 𝕜 E)) → E) x_1 : E) :
    E)
Tactic: simp_rw [sum_apply, rankOne_apply, a, inner_smul_left, smul_smul, mul_assoc, conj_ofReal,
    mul_comm (⟪_, _⟫_𝕜), ← mul_assoc, ← ofReal_mul,
    ← Real.sqrt_mul (hT.toLinearMap.nonneg_eigenvalues rfl _),
    Real.sqrt_mul_self (hT.toLinearMap.nonneg_eigenvalues rfl _), mul_comm _ (⟪_, _⟫_𝕜),
    ← smul_eq_mul, smul_assoc, ← hT.isSymmetric.apply_eigenvectorBasis, ← map_smul, ← map_sum,
    ← OrthonormalBasis.repr_apply_apply, OrthonormalBasis.sum_repr, coe_coe]