no goals
α : Type u_1
β : Type ?u.560456
γ : Type ?u.560459
δ : Type ?u.560462
ι : Type ?u.560465
R : Type ?u.560468
R' : Type ?u.560471
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t : Set α
p : α → Prop
⊢ (∀ᵐ (x : α) ∂Measure.restrict μ (s ∪ t), p x) ↔
    (∀ᵐ (x : α) ∂Measure.restrict μ s, p x) ∧ ∀ᵐ (x : α) ∂Measure.restrict μ t, p x
simp