-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem compProd_eq_sum_compProd_left (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ) :
    κ ⊗ₖ η = Kernel.sum fun n => seq κ n ⊗ₖ η

Proof state:
case pos.e_κ.h.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
η : Kernel (α × β) γ
h : IsSFiniteKernel η
n : ℕ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((Kernel.sum fun m => κ.seq n ⊗ₖ η.seq m) a) s = ((κ.seq n ⊗ₖ η) a) s

Tactic:
simp_rw [Kernel.sum_apply' _ _ hs, compProd_apply_eq_compProdFun _ _ _ hs,
  compProdFun_tsum_right _ η a hs]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
η : Kernel (α × β) γ
⊢ κ ⊗ₖ η = Kernel.sum fun n => κ.seq n ⊗ₖ η

Tactic:
by_cases h : IsSFiniteKernel η

Result:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
η : Kernel (α × β) γ
h : IsSFiniteKernel η
⊢ κ ⊗ₖ η = Kernel.sum fun n => κ.seq n ⊗ₖ η

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
η : Kernel (α × β) γ
h : ¬IsSFiniteKernel η
⊢ κ ⊗ₖ η = Kernel.sum fun n => κ.seq n ⊗ₖ η

Proof state:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
η : Kernel (α × β) γ
h : IsSFiniteKernel η
⊢ (Kernel.sum fun n => Kernel.sum fun m => κ.seq n ⊗ₖ η.seq m) = Kernel.sum fun n => κ.seq n ⊗ₖ η

Tactic:
congr with n a s hs

Result:
case pos.e_κ.h.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
η : Kernel (α × β) γ
h : IsSFiniteKernel η
n : ℕ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((Kernel.sum fun m => κ.seq n ⊗ₖ η.seq m) a) s = ((κ.seq n ⊗ₖ η) a) s

Proof state:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
η : Kernel (α × β) γ
h : IsSFiniteKernel η
⊢ κ ⊗ₖ η = Kernel.sum fun n => κ.seq n ⊗ₖ η

Tactic:
rw [compProd_eq_sum_compProd]

Result:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
η : Kernel (α × β) γ
h : IsSFiniteKernel η
⊢ (Kernel.sum fun n => Kernel.sum fun m => κ.seq n ⊗ₖ η.seq m) = Kernel.sum fun n => κ.seq n ⊗ₖ η

Proof state:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
η : Kernel (α × β) γ
h : ¬IsSFiniteKernel η
⊢ 0 = Kernel.sum fun n => 0

Tactic:
simp

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
η : Kernel (α × β) γ
h : ¬IsSFiniteKernel η
⊢ κ ⊗ₖ η = Kernel.sum fun n => κ.seq n ⊗ₖ η

Tactic:
simp_rw [compProd_of_not_isSFiniteKernel_right _ _ h]

Result:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
η : Kernel (α × β) γ
h : ¬IsSFiniteKernel η
⊢ 0 = Kernel.sum fun n => 0

Proof state:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
η : Kernel (α × β) γ
h : IsSFiniteKernel η
⊢ κ ⊗ₖ η = Kernel.sum fun n => κ.seq n ⊗ₖ η

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
η : Kernel (α × β) γ
h : ¬IsSFiniteKernel η
⊢ κ ⊗ₖ η = Kernel.sum fun n => κ.seq n ⊗ₖ η

Tactic:
swap

Result:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
η : Kernel (α × β) γ
h : ¬IsSFiniteKernel η
⊢ κ ⊗ₖ η = Kernel.sum fun n => κ.seq n ⊗ₖ η

case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
η : Kernel (α × β) γ
h : IsSFiniteKernel η
⊢ κ ⊗ₖ η = Kernel.sum fun n => κ.seq n ⊗ₖ η