∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {f : α → α} {μ : MeasureTheory.Measure α},
  QuasiErgodic f μ →
    MeasureTheory.NullMeasurableSet s μ → f ⁻¹' s =ᵐ[μ] s → Filter.EventuallyConst s (MeasureTheory.ae μ)