cases p with
| none => exact snorm_top_lt_top f
| some p =>
  simp
  cases eq_or_lt_of_le (zero_le p) with
  | inl hp => simp [← hp]
  | inr hp => exact snorm_nnreal_lt_top f hp
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
f : 𝓢(E, F)
p : ENNReal
⊢ snorm (⇑f) p volume < ⊤
no goals