∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {f : α → α} {μ : MeasureTheory.Measure α},
  Ergodic f μ → MeasureTheory.NullMeasurableSet s μ → s ≤ᵐ[μ] f ⁻¹' s → μ s ≠ ⊤ → s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] Set.univ