∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ] (x : α)
  {n : ℕ}, MeasureTheory.spanningSetsIndex μ x ≤ n → x ∈ MeasureTheory.spanningSets μ n