no goals
α : Type u_1
β : Type ?u.561248
γ : Type ?u.561251
δ : Type ?u.561254
ι : Type u_2
R : Type ?u.561260
R' : Type ?u.561263
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
s : ι → Set α
t : Set ι
ht : Set.Countable t
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_eq s ht, mem_iSup]