∀ {α : Type u_1} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  {C : Set (Set α)},
  MeasureTheory.IsSetSemiring C →
    (∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0) →
      mα = MeasurableSpace.generateFrom C →
        ∀ {s : Set α}, MeasurableSet s → ∀ {ε : ENNReal}, 0 < ε → ∃ t ∈ supClosure C, μ (symmDiff t s) < ε