no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.4189796
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
T : E →L[𝕜] E
x : E
c : 𝕜
⊢ reApplyInnerSelf T (c • x) = ‖c‖ ^ 2 * reApplyInnerSelf T x
simp only [ContinuousLinearMap.map_smul, ContinuousLinearMap.reApplyInnerSelf_apply,
  inner_smul_left, inner_smul_right, ← mul_assoc, mul_conj, normSq_eq_def', ← smul_re,
  Algebra.smul_def (‖c‖ ^ 2) ⟪T x, x⟫, algebraMap_eq_ofReal]