no goals
ι : Type ?u.68894
ι' : Type ?u.68897
𝕜✝ : Type ?u.68900
inst✝¹⁰ : IsROrC 𝕜✝
E : Type ?u.68906
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜✝ E
E' : Type ?u.68926
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜✝ E'
F : Type ?u.68944
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.68964
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
n : Type u_2
inst✝ : Fintype n
x : EuclideanSpace 𝕜 n
⊢ ‖x‖ = Real.sqrt (∑ i : n, ‖x i‖ ^ 2)
simpa only [Real.coe_sqrt, NNReal.coe_sum] using congr_arg ((↑) : ℝ≥0 → ℝ) x.nnnorm_eq