Variance eq norm sq sub expected Value sq

lemma variance_eq_norm_sq_sub_expectedValue_sq (T : H →ₗ.[ℂ] H)    (hT : T.IsSymmetric) (ψ : T.domain) (hψ_norm : ‖(ψ : H)‖ = 1) :    variance T ψ = ‖T ψ‖ ^ 2 - expectedValue T ψ ^ 2 := by  let μ := expectedValue T ψ  let a : H := T ψ  have hμ_right : ⟪(ψ : H), a⟫_ℂ = (μ : ℂ) := by    simpa [a, μ] using expectedValue_eq_inner T hT ψ  have hμ_left : ⟪a, (ψ : H)⟫_ℂ = (μ : ℂ) := by    simpa [inner_conj_symm] using congrArg star hμ_right  have h_re_inner_centered : (⟪a, (μ : ℂ) • (ψ : H)⟫_ℂ).re = μ ^ 2 := by    rw [inner_smul_right, hμ_left]    simp [μ]    ring  have h_norm_centered_smul : ‖(μ : ℂ) • (ψ : H)‖ ^ 2 = μ ^ 2 := by    rw [norm_smul, hψ_norm]    simp [μ]  have h_norm_sub_sq :      ‖a - (μ : ℂ) • (ψ : H)‖ ^ 2 =        ‖a‖ ^ 2 - 2 * (⟪a, (μ : ℂ) • (ψ : H)⟫_ℂ).re + ‖(μ : ℂ) • (ψ : H)‖ ^ 2 := by    simpa using (norm_sub_sq (𝕜 := ℂ) a ((μ : ℂ) • (ψ : H)))  rw [variance_eq_norm_sub_sq, h_norm_sub_sq, h_re_inner_centered,    h_norm_centered_smul]  ring