-- 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)
simp_rw₆ :
  Eq (α := E) ((T : (a : E) → E) x : E)
    (∑ x_1 : Fin (Module.finrank 𝕜 E),
        HSMul.hSMul (β := E)
          ((↑√(⋯.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)
          ((↑√(⋯.eigenvalues ⋯ x_1) : 𝕜) *
            ((↑√(⋯.eigenvalues ⋯ x_1) : 𝕜) * ⟪(⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) x_1, x⟫))
          ((⋯.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 (α := 𝕜) (↑√(⋯.eigenvalues ⋯ x_1) : 𝕜) (↑√(⋯.eigenvalues ⋯ x_1) : 𝕜) *
            ⟪(⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) x_1, x⟫)
          ((⋯.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)
          ((↑(√(⋯.eigenvalues ⋯ x_1) * √(⋯.eigenvalues ⋯ x_1)) : 𝕜) *
            ⟪(⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) x_1, x⟫)
          ((⋯.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)
          ((↑√(⋯.eigenvalues ⋯ x_1 * ⋯.eigenvalues ⋯ x_1) : 𝕜) *
            ⟪(⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) x_1, x⟫)
          ((⋯.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)
          ((↑(⋯.eigenvalues ⋯ x_1) : 𝕜) * ⟪(⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) x_1, x⟫)
          ((⋯.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)
          (⟪(⋯.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)
          (HSMul.hSMul (β := 𝕜) ⟪(⋯.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),
        ⟪(⋯.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) ⟪(⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) x_1, x⟫
          (((↑T : E →ₗ[𝕜] E) : (a : E) → E) ((⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) x_1 : E) : E) :
      E)
simp_rw₁₆ :
  Eq (α := E) ((T : (a : E) → E) x : E)
    (∑ x_1 : Fin (Module.finrank 𝕜 E),
        ((↑T : E →ₗ[𝕜] E) : (a : E) → E)
          (HSMul.hSMul (β := E) ⟪(⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) x_1, x⟫
            ((⋯.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)
  (((↑T : E →ₗ[𝕜] E) : (a : E) → E)
      (∑ x_1 : Fin (Module.finrank 𝕜 E),
        HSMul.hSMul (β := E) ⟪(sorry.eigenvectorBasis sorry : (a : Fin (Module.finrank 𝕜 E)) → E) x_1, x⟫
          ((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]