∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : Set α → Prop}
  [inst_1 : TopologicalSpace α] [μ.OuterRegular],
  μ.InnerRegularWRT p IsOpen →
    (∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)) → μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤