case intro
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.56213
F : Type ?u.56216
G : Type ?u.56219
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →L[𝕜] E
hT : IsSymmetric ↑T
x : E
r : ℝ
hr : inner (↑T x) x = ↑r
⊢ ↑(ContinuousLinearMap.reApplyInnerSelf T x) = inner (↑T x) x

𝕜 : Type u_1
E : Type u_2
E' : Type ?u.56213
F : Type ?u.56216
G : Type ?u.56219
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →L[𝕜] E
hT : IsSymmetric ↑T
x : E
⊢ ∃ r, inner (↑T x) x = ↑r
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.56213
F : Type ?u.56216
G : Type ?u.56219
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →L[𝕜] E
hT : IsSymmetric ↑T
x : E
⊢ ↑(ContinuousLinearMap.reApplyInnerSelf T x) = inner (↑T x) x
rsuffices ⟨r, hr⟩ : ∃ r : ℝ, ⟪T x, x⟫ = r
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.56213
F : Type ?u.56216
G : Type ?u.56219
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →L[𝕜] E
hT : IsSymmetric ↑T
x : E
⊢ ↑(starRingEnd 𝕜) (inner (↑T x) x) = inner (↑T x) x
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.56213
F : Type ?u.56216
G : Type ?u.56219
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →L[𝕜] E
hT : IsSymmetric ↑T
x : E
⊢ ∃ r, inner (↑T x) x = ↑r
rw [← conj_eq_iff_real]
no goals
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.56213
F : Type ?u.56216
G : Type ?u.56219
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →L[𝕜] E
hT : IsSymmetric ↑T
x : E
⊢ ↑(starRingEnd 𝕜) (inner (↑T x) x) = inner (↑T x) x
exact hT.conj_inner_sym x x
no goals
case intro
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.56213
F : Type ?u.56216
G : Type ?u.56219
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →L[𝕜] E
hT : IsSymmetric ↑T
x : E
r : ℝ
hr : inner (↑T x) x = ↑r
⊢ ↑(ContinuousLinearMap.reApplyInnerSelf T x) = inner (↑T x) x
simp [hr, T.reApplyInnerSelf_apply]