no goals
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : MeasureTheory.Measure α
hf : PreErgodic f
hs : MeasurableSet s
hs' : f ⁻¹' s = s
⊢ ↑↑μ s = 0 ∨ ↑↑μ (sᶜ) = 0
simpa using hf.ae_empty_or_univ hs hs'