case h.h
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κ η : ι → { x // x ∈ kernel α β }
a : α
s : Set β
⊢ MeasurableSet s → ↑↑(↑(kernel.sum fun n => κ n + η n) a) s = ↑↑(↑(kernel.sum κ + kernel.sum η) a) s
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κ η : ι → { x // x ∈ kernel α β }
⊢ (kernel.sum fun n => κ n + η n) = kernel.sum κ + kernel.sum η
ext a s
case h.h
α : 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 fun n => κ n + η n) a) s = ↑↑(↑(kernel.sum κ + kernel.sum η) a) s
case h.h
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κ η : ι → { x // x ∈ kernel α β }
a : α
s : Set β
⊢ MeasurableSet s → ↑↑(↑(kernel.sum fun n => κ n + η n) a) s = ↑↑(↑(kernel.sum κ + kernel.sum η) a) s
intro hs
no goals
case h.h
α : 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 fun n => κ n + η n) a) s = ↑↑(↑(kernel.sum κ + kernel.sum η) a) s
simp only [coeFn_add, Pi.add_apply, sum_apply, Measure.sum_apply _ hs, Pi.add_apply,
  Measure.coe_add, tsum_add ENNReal.summable ENNReal.summable]