∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α}
  [OpensMeasurableSpace α] [μ.InnerRegular], MeasurableSet s → μ.IsEverywherePos (μ.everywherePosSubset s)