𝕜 : Type ?u.131195
E : Type u_1
F : Type ?u.131201
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type ?u.131330
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x✝ : G
n : ℕ∞
x : E
hx : x ≠ 0
this : ‖id x‖ ^ 2 ≠ 0
⊢ ContDiffAt ℝ n Norm.norm x
𝕜 : Type ?u.131195
E : Type u_1
F : Type ?u.131201
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type ?u.131330
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x✝ : G
n : ℕ∞
x : E
hx : x ≠ 0
⊢ ContDiffAt ℝ n Norm.norm x
have : ‖id x‖ ^ 2 ≠ 0 := pow_ne_zero 2 (norm_pos_iff.2 hx).ne'
no goals
𝕜 : Type ?u.131195
E : Type u_1
F : Type ?u.131201
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : NormedSpace ℝ E
G : Type ?u.131330
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
s : Set G
x✝ : G
n : ℕ∞
x : E
hx : x ≠ 0
this : ‖id x‖ ^ 2 ≠ 0
⊢ ContDiffAt ℝ n Norm.norm x
simpa only [id, sqrt_sq, norm_nonneg] using (contDiffAt_id.norm_sq 𝕜).sqrt this