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 => kernel.sum (κ n)) a) s = ↑↑(↑(kernel.sum fun m => kernel.sum fun n => κ n m) 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 => kernel.sum (κ n)) = kernel.sum fun m => kernel.sum fun n => κ n m
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 β
a✝ : MeasurableSet s
⊢ ↑↑(↑(kernel.sum fun n => kernel.sum (κ n)) a) s = ↑↑(↑(kernel.sum fun m => kernel.sum fun n => κ n m) 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 => kernel.sum (κ n)) a) s = ↑↑(↑(kernel.sum fun m => kernel.sum fun n => κ n m) a) s
intro
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 β
a✝ : MeasurableSet s
⊢ ↑↑(Measure.sum fun n => Measure.sum fun n_1 => ↑(κ n n_1) a) s =
    ↑↑(Measure.sum fun n => Measure.sum fun n_1 => ↑(κ n_1 n) 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 β
a✝ : MeasurableSet s
⊢ ↑↑(↑(kernel.sum fun n => kernel.sum (κ n)) a) s = ↑↑(↑(kernel.sum fun m => kernel.sum fun n => κ n m) a) s
simp_rw [sum_apply]
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 β
a✝ : MeasurableSet s
⊢ ↑↑(Measure.sum fun n => Measure.sum fun n_1 => ↑(κ n n_1) a) s =
    ↑↑(Measure.sum fun n => Measure.sum fun n_1 => ↑(κ n_1 n) a) s
rw [Measure.sum_comm]