{α : Type u_1} →
  [inst : MeasurableSpace α] →
    [inst_1 : TopologicalSpace α] →
      {μ : MeasureTheory.Measure α} →
        {motive : μ.WeaklyRegular → Sort u} →
          (t : μ.WeaklyRegular) →
            ([toOuterRegular : μ.OuterRegular] → (innerRegular : μ.InnerRegularWRT IsClosed IsOpen) → motive ⋯) →
              motive t