no goals
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s✝ t u v : Set α
inst✝ : Countable ι
s : ι → Set α
⊢ AEDisjoint μ (⋃ (i : ι), s i) t ↔ ∀ (i : ι), AEDisjoint μ (s i) t
simp only [AEDisjoint, iUnion_inter, measure_iUnion_null_iff]