{X : Type u_1} →
  [m : MeasurableSpace X] →
    {μ : MeasureTheory.Measure X} →
      {𝒜 : Set (Set X)} →
        {motive : μ.MeasureDense 𝒜 → Sort u} →
          ((measurable : ∀ s ∈ 𝒜, MeasurableSet s) →
              (approx :
                  ∀ (s : Set X),
                    MeasurableSet s → μ s ≠ ⊤ → ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ (symmDiff s t) < ENNReal.ofReal ε) →
                motive ⋯) →
            (t : μ.MeasureDense 𝒜) → motive t