∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
  MeasureTheory.Conservative f μ →
    MeasureTheory.NullMeasurableSet s μ → μ s ≠ 0 → ∃ᶠ (m : ℕ) in Filter.atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0