no goals
α : Type u_1
β : Type ?u.728649
γ : Type ?u.728652
δ : Type ?u.728655
ι : Type ?u.728658
R : Type ?u.728661
R' : Type ?u.728664
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ : Measure α
inst✝ : SigmaFinite μ
x : α
n : ℕ
⊢ spanningSetsIndex μ x = n ↔ x ∈ disjointed (spanningSets μ) n
convert Set.ext_iff.1 (preimage_spanningSetsIndex_singleton μ n) x