no goals
α : Type u_1
E : Type ?u.526534
F : Type u_2
G : Type ?u.526540
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
⊢ snorm f 1 μ = ∫⁻ (x : α), ↑‖f x‖₊ ∂μ
simp_rw [snorm_eq_lintegral_rpow_nnnorm one_ne_zero ENNReal.coe_ne_top, ENNReal.one_toReal,
  one_div_one, ENNReal.rpow_one]