α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : MeasureTheory.Measure α
hf : Ergodic f
hs : MeasurableSet s
h_fin : ↑↑μ s ≠ ⊤
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : MeasureTheory.Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : f '' s ≤ᶠ[ae μ] s
h_fin : ↑↑μ s ≠ ⊤
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
replace hs' : s ≤ᵐ[μ] f ⁻¹' s :=
  (HasSubset.Subset.eventuallyLE (subset_preimage_image f s)).trans
    (hf.quasiMeasurePreserving.preimage_mono_ae hs')
no goals
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : MeasureTheory.Measure α
hf : Ergodic f
hs : MeasurableSet s
h_fin : ↑↑μ s ≠ ⊤
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
exact ae_empty_or_univ_of_ae_le_preimage' hf hs hs' h_fin