no goals
α : Type u_2
β : Type ?u.563218
γ : Type ?u.563221
δ : Type u_3
ι : Type u_1
R : Type ?u.563230
R' : Type ?u.563233
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : Countable ι
s : ι → Set α
f g : α → δ
⊢ f =ᶠ[ae (Measure.restrict μ (⋃ (i : ι), s i))] g ↔ ∀ (i : ι), f =ᶠ[ae (Measure.restrict μ (s i))] g
simp_rw [EventuallyEq, ae_restrict_iUnion_eq, eventually_iSup]