-- Module: Mathlib.Analysis.InnerProductSpace.Positive
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)
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) ⟪(⋯.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)
    (((↑T : E →ₗ[𝕜] E) : (a : E) → E)
        (∑ x_1 : Fin (Module.finrank 𝕜 E),
          HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E)
            (WithLp.ofLp (p := 2)
              (((⋯.eigenvectorBasis ⋯).repr : (a : E) → EuclideanSpace 𝕜 (Fin (Module.finrank 𝕜 E))) x) x_1)
            ((⋯.eigenvectorBasis ⋯ : (a : Fin (Module.finrank 𝕜 E)) → E) x_1 : E)) :
      E)
simp_rw₁₉ : Eq (α := E) ((T : (a : E) → E) x : E) (((↑T : E →ₗ[𝕜] E) : (a : E) → E) x : 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)

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]

Premises used: ContinuousLinearMap.IsPositive.toLinearMap, LinearMap.IsPositive.nonneg_eigenvalues, smul_assoc, ContinuousLinearMap.sum_apply, InnerProductSpace.rankOne_apply, Inner.inner, mul_assoc, Real.sqrt_mul_self, RCLike.conj_ofReal, RCLike.ofReal_mul, smul_smul, ContinuousLinearMap.IsPositive.isSymmetric, ContinuousLinearMap.coe_coe, OrthonormalBasis.repr_apply_apply, Real.sqrt_mul, map_sum, LinearMap.IsSymmetric.apply_eigenvectorBasis, mul_comm, OrthonormalBasis.sum_repr, smul_eq_mul, rfl, map_smul, inner_smul_left