{α : Type u_2} →
  {x : MeasurableSpace α} →
    {μ : MeasureTheory.Measure α} →
      {motive : μ.IsComplete → Sort u} →
        ((out' : ∀ (s : Set α), μ s = 0 → MeasurableSet s) → motive ⋯) → (t : μ.IsComplete) → motive t