{α : Type u_1} →
  {m : MeasurableSpace α} →
    {f : α → α} →
      {μ : MeasureTheory.Measure α} →
        {motive : PreErgodic f μ → Sort u} →
          (t : PreErgodic f μ) →
            ((aeconst_set :
                  ∀ ⦃s : Set α⦄, MeasurableSet s → f ⁻¹' s = s → Filter.EventuallyConst s (MeasureTheory.ae μ)) →
                motive ⋯) →
              motive t