-- Mathlib/Probability/Kernel/Defs.lean
theorem isSFiniteKernel_sum_of_denumerable [Denumerable ι] {κs : ι → Kernel α β}
    (hκs : ∀ n, IsSFiniteKernel (κs n)) : IsSFiniteKernel (Kernel.sum κs)

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
⊢ Kernel.sum κs = Kernel.sum fun n => Kernel.sum (κs n).seq

Tactic:
simp_rw [kernel_sum_seq]

Result:
no goals

Proof state:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : Kernel.sum κs = Kernel.sum fun n => Kernel.sum (κs n).seq
a : α
s : Set β
hs : MeasurableSet s
⊢ ∑' (n : ι) (n_1 : ℕ), (((κs n).seq n_1) a) s = ∑' (n : ℕ), (((κs (e n).1).seq (e n).2) a) s

Tactic:
change (∑' i, ∑' m, seq (κs i) m a s) = ∑' n, (fun im : ι × ℕ => seq (κs im.fst) im.snd a s) (e n)

Result:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : Kernel.sum κs = Kernel.sum fun n => Kernel.sum (κs n).seq
a : α
s : Set β
hs : MeasurableSet s
⊢ ∑' (i : ι) (m : ℕ), (((κs i).seq m) a) s = ∑' (n : ℕ), (fun im => (((κs im.1).seq im.2) a) s) (e n)

Proof state:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : Kernel.sum κs = Kernel.sum fun n => Kernel.sum (κs n).seq
a : α
s : Set β
hs : MeasurableSet s
⊢ ∑' (i : ι) (m : ℕ), (((κs i).seq m) a) s = ∑' (n : ℕ), (fun im => (((κs im.1).seq im.2) a) s) (e n)

Tactic:
rw [e.tsum_eq (fun im : ι × ℕ => seq (κs im.fst) im.snd a s),
  tsum_prod' ENNReal.summable fun _ => ENNReal.summable]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : Kernel.sum κs = Kernel.sum fun n => Kernel.sum (κs n).seq
⊢ Kernel.sum κs = Kernel.sum fun n => (κs (e n).1).seq (e n).2

Tactic:
ext a s hs

Result:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : Kernel.sum κs = Kernel.sum fun n => Kernel.sum (κs n).seq
a : α
s : Set β
hs : MeasurableSet s
⊢ ((Kernel.sum κs) a) s = ((Kernel.sum fun n => (κs (e n).1).seq (e n).2) a) s

Proof state:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : Kernel.sum κs = Kernel.sum fun n => Kernel.sum (κs n).seq
a : α
s : Set β
hs : MeasurableSet s
⊢ ((Kernel.sum κs) a) s = ((Kernel.sum fun n => (κs (e n).1).seq (e n).2) a) s

Tactic:
rw [hκ_eq]

Result:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : Kernel.sum κs = Kernel.sum fun n => Kernel.sum (κs n).seq
a : α
s : Set β
hs : MeasurableSet s
⊢ ((Kernel.sum fun n => Kernel.sum (κs n).seq) a) s = ((Kernel.sum fun n => (κs (e n).1).seq (e n).2) a) s

Proof state:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : Kernel.sum κs = Kernel.sum fun n => Kernel.sum (κs n).seq
a : α
s : Set β
hs : MeasurableSet s
⊢ ((Kernel.sum fun n => Kernel.sum (κs n).seq) a) s = ((Kernel.sum fun n => (κs (e n).1).seq (e n).2) a) s

Tactic:
simp_rw [Kernel.sum_apply' _ _ hs]

Result:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : Kernel.sum κs = Kernel.sum fun n => Kernel.sum (κs n).seq
a : α
s : Set β
hs : MeasurableSet s
⊢ ∑' (n : ι) (n_1 : ℕ), (((κs n).seq n_1) a) s = ∑' (n : ℕ), (((κs (e n).1).seq (e n).2) a) s

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
⊢ IsSFiniteKernel (Kernel.sum κs)

Tactic:
refine ⟨⟨fun n => seq (κs (e n).1) (e n).2, inferInstance, ?_⟩⟩

Result:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
⊢ Kernel.sum κs = Kernel.sum fun n => (κs (e n).1).seq (e n).2

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
⊢ Kernel.sum κs = Kernel.sum fun n => (κs (e n).1).seq (e n).2

Tactic:
have hκ_eq : Kernel.sum κs = Kernel.sum fun n => Kernel.sum (seq (κs n)) := by
  simp_rw [kernel_sum_seq]

Result:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : Kernel.sum κs = Kernel.sum fun n => Kernel.sum (κs n).seq
⊢ Kernel.sum κs = Kernel.sum fun n => (κs (e n).1).seq (e n).2

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
⊢ IsSFiniteKernel (Kernel.sum κs)

Tactic:
let e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm

Result:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
⊢ IsSFiniteKernel (Kernel.sum κs)