case h.e'_10.h
𝕜 : Type ?u.101013
E : Type u_1
F : Type ?u.101019
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type ?u.101148
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
x✝ : E
⊢ ‖x✝‖ ^ 2 = (↑reClm ∘ fun x => inner (id x) (id x)) x✝
𝕜 : Type ?u.101013
E : Type u_1
F : Type ?u.101019
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type ?u.101148
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
⊢ ContDiff ℝ n fun x => ‖x‖ ^ 2
convert (reClm : 𝕜 →L[ℝ] ℝ).contDiff.comp ((contDiff_id (E := E)).inner 𝕜 (contDiff_id (E := E)))
no goals
case h.e'_10.h
𝕜 : Type ?u.101013
E : Type u_1
F : Type ?u.101019
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type ?u.101148
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x : G
n : ℕ∞
x✝ : E
⊢ ‖x✝‖ ^ 2 = (↑reClm ∘ fun x => inner (id x) (id x)) x✝
exact (inner_self_eq_norm_sq _).symm