no goals
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : MeasureTheory.Measure α
inst✝ : IsProbabilityMeasure μ
hf : PreErgodic f
hs : MeasurableSet s
hs' : f ⁻¹' s = s
⊢ ↑↑μ s = 0 ∨ ↑↑μ s = 1
simpa [hs] using hf.measure_self_or_compl_eq_zero hs hs'