no goals
α : Type u_1
β : Type ?u.344710
γ : Type ?u.344713
δ : Type ?u.344716
ι : Type u_2
R : Type ?u.344722
R' : Type ?u.344725
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
μ : ι → Measure α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ ↑↑(restrict (sum μ) s) t = ↑↑(sum fun i => restrict (μ i) s) t
simp only [sum_apply, restrict_apply, ht, ht.inter hs]