∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
  MeasureTheory.Conservative f μ →
    MeasureTheory.NullMeasurableSet s μ → μ (s ∩ {x | ∃ᶠ (n : ℕ) in Filter.atTop, f^[n] x ∈ s}) = μ s