no goals
α : Type u_1
E : Type ?u.4185587
F : Type u_2
G : Type ?u.4185593
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
hq_pos : 0 < q
f : α → F
inst✝ : IsProbabilityMeasure μ
⊢ snormEssSup f μ * ↑↑μ Set.univ ^ (1 / q) = snormEssSup f μ
simp [measure_univ]