no goals
α : Type u_2
β : Type ?u.359713
γ : Type ?u.359716
δ : Type ?u.359719
ι : Type u_1
R : Type ?u.359725
R' : Type ?u.359728
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
hm : ∀ (i : ι), NullMeasurableSet (s i)
t : Set α
ht : MeasurableSet t
⊢ ↑↑(restrict μ (⋃ (i : ι), s i)) t = ↑↑(sum fun i => restrict μ (s i)) t
simp only [sum_apply _ ht, restrict_iUnion_apply_ae hd hm ht]