no goals
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f : α → ℝ≥0∞
hf_nonzero : (∫⁻ (a : α), f a ^ p ∂μ) ≠ 0
hf_top : (∫⁻ (a : α), f a ^ p ∂μ) ≠ ⊤
a : α
⊢ f a = funMulInvSnorm f p μ a * (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)
simp [funMulInvSnorm, mul_assoc, ENNReal.inv_mul_cancel, hf_nonzero, hf_top]