no goals
α : Type u_1
E : Type ?u.946710
F : Type u_2
G : Type ?u.946716
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
inst✝ : MeasurableSpace α
f : α → F
hq_pos : 0 < q
⊢ snorm' f q 0 = 0
simp [snorm', hq_pos]