no goals
α : Type u_1
β : Type ?u.963625
γ : Type ?u.963628
δ : Type ?u.963631
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
hμf : 0 < ↑↑μ {x | f x = ⊤}
⊢ ⊤ = ⊤ * ↑↑μ {x | ⊤ ≤ f x}
simp [mul_eq_top, hμf.ne.symm]