-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem compProdFun_tsum_right (κ : Kernel α β) (η : Kernel (α × β) γ) [IsSFiniteKernel η] (a : α)
    (hs : MeasurableSet s) : compProdFun κ η a s = ∑' n, compProdFun κ (seq η n) a s

Proof state:
case e_f.h.hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
b : β
⊢ MeasurableSet {c | (b, c) ∈ s}

Tactic:
exact measurable_prod_mk_left hs

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ κ.compProdFun η a s = ∑' (n : ℕ), κ.compProdFun (η.seq n) a s

Tactic:
simp_rw [compProdFun, (measure_sum_seq η _).symm]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (Measure.sum fun n => (η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a =
    ∑' (n : ℕ), ∫⁻ (b : β), ((η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
this :
  ∫⁻ (b : β), (Measure.sum fun n => (η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a =
    ∫⁻ (b : β), ∑' (n : ℕ), ((η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a
⊢ ∫⁻ (b : β), (Measure.sum fun n => (η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a =
    ∑' (n : ℕ), ∫⁻ (b : β), ((η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a

Tactic:
rw [this, lintegral_tsum]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
this :
  ∫⁻ (b : β), (Measure.sum fun n => (η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a =
    ∫⁻ (b : β), ∑' (n : ℕ), ((η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a
⊢ ∀ (i : ℕ), AEMeasurable (fun b => ((η.seq i) (a, b)) {c | (b, c) ∈ s}) (κ a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
this :
  ∫⁻ (b : β), (Measure.sum fun n => (η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a =
    ∫⁻ (b : β), ∑' (n : ℕ), ((η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a
⊢ ∀ (i : ℕ), AEMeasurable (fun b => ((η.seq i) (a, b)) {c | (b, c) ∈ s}) (κ a)

Tactic:
exact fun n ↦ ((measurable_kernel_prod_mk_left (κ := (seq η n))
  ((measurable_fst.snd.prod_mk measurable_snd) hs)).comp measurable_prod_mk_left).aemeasurable

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (Measure.sum fun n => (η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a =
    ∑' (n : ℕ), ∫⁻ (b : β), ((η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a

Tactic:
have : ∫⁻ b, Measure.sum (fun n => seq η n (a, b)) {c : γ | (b, c) ∈ s} ∂κ a
    = ∫⁻ b, ∑' n, seq η n (a, b) {c : γ | (b, c) ∈ s} ∂κ a := by
  congr with b
  rw [Measure.sum_apply]
  exact measurable_prod_mk_left hs

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
this :
  ∫⁻ (b : β), (Measure.sum fun n => (η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a =
    ∫⁻ (b : β), ∑' (n : ℕ), ((η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a
⊢ ∫⁻ (b : β), (Measure.sum fun n => (η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a =
    ∑' (n : ℕ), ∫⁻ (b : β), ((η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (Measure.sum fun n => (η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a =
    ∫⁻ (b : β), ∑' (n : ℕ), ((η.seq n) (a, b)) {c | (b, c) ∈ s} ∂κ a

Tactic:
congr with b

Result:
case e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
b : β
⊢ (Measure.sum fun n => (η.seq n) (a, b)) {c | (b, c) ∈ s} = ∑' (n : ℕ), ((η.seq n) (a, b)) {c | (b, c) ∈ s}

Proof state:
case e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
b : β
⊢ (Measure.sum fun n => (η.seq n) (a, b)) {c | (b, c) ∈ s} = ∑' (n : ℕ), ((η.seq n) (a, b)) {c | (b, c) ∈ s}

Tactic:
rw [Measure.sum_apply]

Result:
case e_f.h.hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
b : β
⊢ MeasurableSet {c | (b, c) ∈ s}