no goals
α : Type u_1
E : Type ?u.376592
F : Type u_2
G : Type ?u.376598
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α → F
⊢ snorm f p μ = (∫⁻ (x : α), ↑‖f x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p)
rw [snorm_eq_snorm' hp_ne_zero hp_ne_top, snorm']