-- Mathlib/Probability/Kernel/Composition/Lemmas.lean
lemma prod_comp_right [SFinite ν] {κ : Kernel β γ} [IsSFiniteKernel κ] :
    μ.prod (κ ∘ₘ ν) = (Kernel.id ∥ₖ κ) ∘ₘ (μ.prod ν)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
⊢ μ.prod (⇑κ ∘ₘ ν) = ⇑(Kernel.id ∥ₖ κ) ∘ₘ μ.prod ν

Tactic:
ext s hs

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ (μ.prod (⇑κ ∘ₘ ν)) s = (⇑(Kernel.id ∥ₖ κ) ∘ₘ μ.prod ν) s

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ (μ.prod (⇑κ ∘ₘ ν)) s = (⇑(Kernel.id ∥ₖ κ) ∘ₘ μ.prod ν) s

Tactic:
rw [Measure.prod_apply hs, Measure.bind_apply hs (Kernel.measurable _)]

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), (⇑κ ∘ₘ ν) (Prod.mk x ⁻¹' s) ∂μ = ∫⁻ (a : α × β), ((Kernel.id ∥ₖ κ) a) s ∂μ.prod ν

Proof state:
case h.e_f.h.e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
a : α
b : β
⊢ (κ b) (Prod.mk a ⁻¹' s) = ((Kernel.id ∥ₖ κ) (a, b)) s

Tactic:
rw [Kernel.parallelComp_apply, Kernel.id_apply, Measure.prod_apply hs, lintegral_dirac']

Result:
case h.e_f.h.e_f.h.hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
a : α
b : β
⊢ Measurable fun x => (κ (a, b).2) (Prod.mk x ⁻¹' s)

Proof state:
case h.e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
a : α
⊢ ∫⁻ (a_1 : β), (κ a_1) (Prod.mk a ⁻¹' s) ∂ν = ∫⁻ (y : β), ((Kernel.id ∥ₖ κ) (a, y)) s ∂ν

Tactic:
congr with b

Result:
case h.e_f.h.e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
a : α
b : β
⊢ (κ b) (Prod.mk a ⁻¹' s) = ((Kernel.id ∥ₖ κ) (a, b)) s

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), (⇑κ ∘ₘ ν) (Prod.mk x ⁻¹' s) ∂μ = ∫⁻ (a : α × β), ((Kernel.id ∥ₖ κ) a) s ∂μ.prod ν

Tactic:
simp_rw [Measure.bind_apply (measurable_prod_mk_left hs) (Kernel.measurable _)]

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ∫⁻ (a : β), (κ a) (Prod.mk x ⁻¹' s) ∂ν ∂μ = ∫⁻ (a : α × β), ((Kernel.id ∥ₖ κ) a) s ∂μ.prod ν

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ∫⁻ (a : β), (κ a) (Prod.mk x ⁻¹' s) ∂ν ∂μ = ∫⁻ (x : α), ∫⁻ (y : β), ((Kernel.id ∥ₖ κ) (x, y)) s ∂ν ∂μ

Tactic:
congr with a

Result:
case h.e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
a : α
⊢ ∫⁻ (a_1 : β), (κ a_1) (Prod.mk a ⁻¹' s) ∂ν = ∫⁻ (y : β), ((Kernel.id ∥ₖ κ) (a, y)) s ∂ν

Proof state:
case h.hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ AEMeasurable (fun a => ((Kernel.id ∥ₖ κ) a) s) (μ.prod ν)

Tactic:
exact (Kernel.measurable_coe _ hs).aemeasurable

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ∫⁻ (a : β), (κ a) (Prod.mk x ⁻¹' s) ∂ν ∂μ = ∫⁻ (a : α × β), ((Kernel.id ∥ₖ κ) a) s ∂μ.prod ν

Tactic:
rw [MeasureTheory.lintegral_prod]

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ∫⁻ (a : β), (κ a) (Prod.mk x ⁻¹' s) ∂ν ∂μ = ∫⁻ (x : α), ∫⁻ (y : β), ((Kernel.id ∥ₖ κ) (x, y)) s ∂ν ∂μ

case h.hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ AEMeasurable (fun a => ((Kernel.id ∥ₖ κ) a) s) (μ.prod ν)

Proof state:
case h.e_f.h.e_f.h.hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
a : α
b : β
⊢ Measurable fun x => (κ (a, b).2) (Prod.mk x ⁻¹' s)

Tactic:
exact measurable_measure_prod_mk_left hs

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ∫⁻ (a : β), (κ a) (Prod.mk x ⁻¹' s) ∂ν ∂μ = ∫⁻ (x : α), ∫⁻ (y : β), ((Kernel.id ∥ₖ κ) (x, y)) s ∂ν ∂μ

case h.hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ AEMeasurable (fun a => ((Kernel.id ∥ₖ κ) a) s) (μ.prod ν)

Tactic:
swap

Result:
case h.hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ AEMeasurable (fun a => ((Kernel.id ∥ₖ κ) a) s) (μ.prod ν)

case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ∫⁻ (a : β), (κ a) (Prod.mk x ⁻¹' s) ∂ν ∂μ = ∫⁻ (x : α), ∫⁻ (y : β), ((Kernel.id ∥ₖ κ) (x, y)) s ∂ν ∂μ