-- Mathlib/Probability/Kernel/Composition/CompProd.lean
lemma compProd_add_right (μ : Kernel α β) (κ η : Kernel (α × β) γ)
    [IsSFiniteKernel κ] [IsSFiniteKernel η] :
    μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η

Proof state:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Kernel α β
κ η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
hμ : ¬IsSFiniteKernel μ
⊢ μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η

Tactic:
simp [hμ]

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 κ
inst✝ : IsSFiniteKernel η
hμ : IsSFiniteKernel μ
⊢ μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η

Tactic:
ext a s hs

Result:
case pos.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Kernel α β
κ η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
hμ : IsSFiniteKernel μ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((μ ⊗ₖ (κ + η)) a) s = ((μ ⊗ₖ κ + μ ⊗ₖ η) a) s

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

Tactic:
rw [lintegral_add_left]

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

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Kernel α β
κ η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
⊢ μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η

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 κ
inst✝ : IsSFiniteKernel η
hμ : IsSFiniteKernel μ
⊢ μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Kernel α β
κ η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
hμ : ¬IsSFiniteKernel μ
⊢ μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η

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

Tactic:
exact measurable_kernel_prod_mk_left' hs a

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 κ
inst✝ : IsSFiniteKernel η
hμ : IsSFiniteKernel μ
⊢ μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Kernel α β
κ η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
hμ : ¬IsSFiniteKernel μ
⊢ μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η

Tactic:
swap

Result:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Kernel α β
κ η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
hμ : ¬IsSFiniteKernel μ
⊢ μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η

case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Kernel α β
κ η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
hμ : IsSFiniteKernel μ
⊢ μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η

Proof state:
case pos.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Kernel α β
κ η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
hμ : IsSFiniteKernel μ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((μ ⊗ₖ (κ + η)) a) s = ((μ ⊗ₖ κ + μ ⊗ₖ η) a) s

Tactic:
simp only [compProd_apply hs, coe_add, Pi.add_apply, Measure.coe_add]

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