-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem compProd_eq_sum_compProd_right (κ : Kernel α β) (η : Kernel (α × β) γ)
    [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 α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
⊢ (Kernel.sum fun n => Kernel.sum fun m => κ.seq n ⊗ₖ η.seq m) =
    Kernel.sum fun n => Kernel.sum fun n_1 => κ.seq n_1 ⊗ₖ η.seq n

Tactic:
rw [Kernel.sum_comm]

Result:
no goals

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

Tactic:
simp_rw [compProd_of_not_isSFiniteKernel_left _ _ hκ]

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

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
⊢ κ ⊗ₖ η = 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 α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
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 α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
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 α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
⊢ (Kernel.sum fun n => Kernel.sum fun m => κ.seq n ⊗ₖ η.seq m) = Kernel.sum fun n => κ ⊗ₖ η.seq n

Tactic:
simp_rw [compProd_eq_sum_compProd_left κ _]

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

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

Tactic:
simp

Result:
no goals

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