no goals
α : Type u_1
β : Type ?u.563935
γ : Type ?u.563938
δ : Type u_3
ι : Type u_2
R : Type ?u.563947
R' : Type ?u.563950
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
s : ι → Set α
t : Set ι
ht : Set.Countable t
f g : α → δ
⊢ f =ᶠ[ae (Measure.restrict μ (⋃ (i : ι) (_ : i ∈ t), s i))] g ↔
    ∀ (i : ι), i ∈ t → f =ᶠ[ae (Measure.restrict μ (s i))] g
simp_rw [ae_restrict_biUnion_eq s ht, EventuallyEq, eventually_iSup]