no goals
α : Type u_1
β : Type ?u.562282
γ : Type ?u.562285
δ : Type ?u.562288
ι : Type u_2
R : Type ?u.562294
R' : Type ?u.562297
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
s : ι → Set α
t : Finset ι
p : α → Prop
⊢ (∀ᵐ (x : α) ∂Measure.restrict μ (⋃ (i : ι) (_ : i ∈ t), s i), p x) ↔
    ∀ (i : ι), i ∈ t → ∀ᵐ (x : α) ∂Measure.restrict μ (s i), p x
simp_rw [Filter.Eventually, ae_restrict_biUnion_finset_eq s, mem_iSup]