no goals
α : Type u_1
E : Type ?u.375839
F : Type u_2
G : Type ?u.375845
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 μ = snorm' f (ENNReal.toReal p) μ
simp [snorm, hp_ne_zero, hp_ne_top]