-- Mathlib/Probability/Kernel/Composition/Lemmas.lean
lemma prod_comp_left [SFinite μ] [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 μ
inst✝¹ : SFinite ν
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
h1 : (⇑κ ∘ₘ μ).prod ν = map Prod.swap (ν.prod (⇑κ ∘ₘ μ))
⊢ ⇑(κ ∥ₖ Kernel.id) ∘ₘ μ.prod ν = map Prod.swap (⇑(Kernel.id ∥ₖ κ) ∘ₘ ν.prod μ)

Tactic:
calc (κ ∥ₖ Kernel.id) ∘ₘ (μ.prod ν)
_ = (κ ∥ₖ Kernel.id) ∘ₘ ((ν.prod μ).map Prod.swap) := by rw [Measure.prod_swap]
_ = (κ ∥ₖ Kernel.id) ∘ₘ ((Kernel.swap _ _) ∘ₘ (ν.prod μ)) := by
  rw [Kernel.swap, Measure.deterministic_comp_eq_map]
_ = (Kernel.swap _ _) ∘ₘ ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)) := by
  rw [Measure.comp_assoc, Measure.comp_assoc, Kernel.swap_parallelComp]
_ = ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)).map Prod.swap := by
  rw [Kernel.swap, Measure.deterministic_comp_eq_map]

Result:
no goals

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

Tactic:
rw [Kernel.swap, Measure.deterministic_comp_eq_map]

Result:
no goals

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

Tactic:
rw [Measure.comp_assoc, Measure.comp_assoc, Kernel.swap_parallelComp]

Result:
no goals

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

Tactic:
rw [← Measure.prod_comp_right, ← h1] at h2

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝² : SFinite μ
inst✝¹ : SFinite ν
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
h1 : (⇑κ ∘ₘ μ).prod ν = map Prod.swap (ν.prod (⇑κ ∘ₘ μ))
h2 : ⇑(κ ∥ₖ Kernel.id) ∘ₘ μ.prod ν = (⇑κ ∘ₘ μ).prod ν
⊢ (⇑κ ∘ₘ μ).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 μ
inst✝¹ : SFinite ν
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
h1 : (⇑κ ∘ₘ μ).prod ν = map Prod.swap (ν.prod (⇑κ ∘ₘ μ))
h2 : ⇑(κ ∥ₖ Kernel.id) ∘ₘ μ.prod ν = (⇑κ ∘ₘ μ).prod ν
⊢ (⇑κ ∘ₘ μ).prod ν = ⇑(κ ∥ₖ Kernel.id) ∘ₘ μ.prod ν

Tactic:
exact h2.symm

Result:
no goals

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

Tactic:
rw [Measure.prod_swap]

Result:
no goals

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

Tactic:
have h1 : (κ ∘ₘ μ).prod ν = (ν.prod (κ ∘ₘ μ)).map Prod.swap := by rw [Measure.prod_swap]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝² : SFinite μ
inst✝¹ : SFinite ν
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
h1 : (⇑κ ∘ₘ μ).prod ν = map Prod.swap (ν.prod (⇑κ ∘ₘ μ))
⊢ (⇑κ ∘ₘ μ).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 μ
inst✝¹ : SFinite ν
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
h1 : (⇑κ ∘ₘ μ).prod ν = map Prod.swap (ν.prod (⇑κ ∘ₘ μ))
⊢ ⇑(Kernel.swap β γ) ∘ₘ ⇑(Kernel.id ∥ₖ κ) ∘ₘ ν.prod μ = map Prod.swap (⇑(Kernel.id ∥ₖ κ) ∘ₘ ν.prod μ)

Tactic:
rw [Kernel.swap, Measure.deterministic_comp_eq_map]

Result:
no goals

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

Tactic:
rw [Measure.prod_swap]

Result:
no goals

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

Tactic:
have h2 : (κ ∥ₖ Kernel.id) ∘ₘ (μ.prod ν) = ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)).map Prod.swap := by
  calc (κ ∥ₖ Kernel.id) ∘ₘ (μ.prod ν)
  _ = (κ ∥ₖ Kernel.id) ∘ₘ ((ν.prod μ).map Prod.swap) := by rw [Measure.prod_swap]
  _ = (κ ∥ₖ Kernel.id) ∘ₘ ((Kernel.swap _ _) ∘ₘ (ν.prod μ)) := by
    rw [Kernel.swap, Measure.deterministic_comp_eq_map]
  _ = (Kernel.swap _ _) ∘ₘ ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)) := by
    rw [Measure.comp_assoc, Measure.comp_assoc, Kernel.swap_parallelComp]
  _ = ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)).map Prod.swap := by
    rw [Kernel.swap, Measure.deterministic_comp_eq_map]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝² : SFinite μ
inst✝¹ : SFinite ν
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
h1 : (⇑κ ∘ₘ μ).prod ν = map Prod.swap (ν.prod (⇑κ ∘ₘ μ))
h2 : ⇑(κ ∥ₖ Kernel.id) ∘ₘ μ.prod ν = map Prod.swap (⇑(Kernel.id ∥ₖ κ) ∘ₘ ν.prod μ)
⊢ (⇑κ ∘ₘ μ).prod ν = ⇑(κ ∥ₖ Kernel.id) ∘ₘ μ.prod ν