no goals
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κ : ι → { x // x ∈ kernel α β }
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑(kernel.sum κ) a) s = ∑' (n : ι), ↑↑(↑(κ n) a) s
rw [sum_apply κ a, Measure.sum_apply _ hs]