p : ℝ≥0∞
𝕜 : Type ?u.285404
𝕜' : Type ?u.285407
ι : Type u_2
α : ι → Type ?u.285415
β✝ : ι → Type ?u.285420
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ‖x‖₊ ^ 2 = ∑ i : ι, ‖x i‖₊ ^ 2
p : ℝ≥0∞
𝕜 : Type ?u.285404
𝕜' : Type ?u.285407
ι : Type u_2
α : ι → Type ?u.285415
β✝ : ι → Type ?u.285420
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ‖x‖ ^ 2 = ∑ i : ι, ‖x i‖ ^ 2
suffices ‖x‖₊ ^ 2 = ∑ i : ι, ‖x i‖₊ ^ 2 by
  simpa only [NNReal.coe_sum] using congr_arg ((↑) : ℝ≥0 → ℝ) this
no goals
p : ℝ≥0∞
𝕜 : Type ?u.285404
𝕜' : Type ?u.285407
ι : Type u_2
α : ι → Type ?u.285415
β✝ : ι → Type ?u.285420
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ‖x‖₊ ^ 2 = ∑ i : ι, ‖x i‖₊ ^ 2
rw [nnnorm_eq_of_L2, NNReal.sq_sqrt]
no goals
p : ℝ≥0∞
𝕜 : Type ?u.285404
𝕜' : Type ?u.285407
ι : Type u_2
α : ι → Type ?u.285415
β✝ : ι → Type ?u.285420
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
this : ‖x‖₊ ^ 2 = ∑ i : ι, ‖x i‖₊ ^ 2
⊢ ‖x‖ ^ 2 = ∑ i : ι, ‖x i‖ ^ 2
simpa only [NNReal.coe_sum] using congr_arg ((↑) : ℝ≥0 → ℝ) this