awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
rw :
  Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ)
      (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) =
    μ ⊗ₘ κ
rw₁ : (⇑(Kernel.swap 𝓧 Ω ∘ₖ Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (Ω × 𝓧)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ κ
⊢ (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) ∘ₘ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ = μ ⊗ₘ κ
have rw₂ : (⇑Kernel.id : (a : Ω × 𝓧) → Measure (Ω × 𝓧)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ κ
Tactic: rw [compProd_posterior_eq_swap_comp, Measure.comp_assoc, Kernel.swap_swap, Measure.id_comp]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
rw :
  Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ)
      (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) =
    μ ⊗ₘ κ
rw₁ : (⇑(Kernel.swap 𝓧 Ω ∘ₖ Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (Ω × 𝓧)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ κ
rw₂ : (⇑Kernel.id : (a : Ω × 𝓧) → Measure (Ω × 𝓧)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ κ
⊢ (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) ∘ₘ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ = μ ⊗ₘ κ
have rw₃ : μ ⊗ₘ κ = μ ⊗ₘ κ
Tactic: rw [compProd_posterior_eq_swap_comp, Measure.comp_assoc, Kernel.swap_swap, Measure.id_comp]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
⊢ Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
      (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)) =
    ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ
have rw : ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ = ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ
Tactic: rw [← Measure.compProd_eq_parallelComp_comp_copy_comp]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
⊢ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ = (⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ
have rw : Eq (α := Measure (𝓧 × Ω)) ((⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ)
  ((⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ)
Tactic: rw [compProd_posterior_eq_swap_comp]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
⊢ Eq (α := Measure (𝓧 × Ω)) ((⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ)
    (Measure.bind (α := Ω × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
        (⇑(Kernel.id ∥ₖ κ) : (a : Ω × Ω) → Measure (Ω × 𝓧)))
      (⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)))
have rw : Eq (α := Measure (𝓧 × Ω))
  (Measure.bind (α := Ω × 𝓧) (mα := Prod.instMeasurableSpace)
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ κ) : (a : Ω × Ω) → Measure (Ω × 𝓧)))
    (⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)))
  (Measure.bind (α := Ω × 𝓧) (mα := Prod.instMeasurableSpace)
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ κ) : (a : Ω × Ω) → Measure (Ω × 𝓧)))
    (⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)))
Tactic: rw [Measure.compProd_eq_parallelComp_comp_copy_comp]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
⊢ Eq (α := Measure (𝓧 × Ω))
    (Measure.bind (α := Ω × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
        (⇑(Kernel.id ∥ₖ κ) : (a : Ω × Ω) → Measure (Ω × 𝓧)))
      (⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
have rw : Eq (α := Measure (𝓧 × Ω))
  (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
    (⇑(Kernel.swap Ω 𝓧 ∘ₖ (Kernel.id ∥ₖ κ)) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
  (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
    (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
Tactic: rw [Measure.comp_assoc, Kernel.swap_parallelComp, Measure.comp_assoc, Kernel.comp_assoc,
      Kernel.swap_copy, Measure.comp_assoc]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
rw :
  Eq (α := Measure (𝓧 × Ω))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.swap Ω 𝓧 ∘ₖ (Kernel.id ∥ₖ κ)) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
⊢ Eq (α := Measure (𝓧 × Ω))
    (Measure.bind (α := Ω × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
        (⇑(Kernel.id ∥ₖ κ) : (a : Ω × Ω) → Measure (Ω × 𝓧)))
      (⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
have rw₁ : Eq (α := Measure (𝓧 × Ω))
  (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
    (⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap Ω Ω) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
  (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
    (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
Tactic: rw [Measure.comp_assoc, Kernel.swap_parallelComp, Measure.comp_assoc, Kernel.comp_assoc,
      Kernel.swap_copy, Measure.comp_assoc]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
rw :
  Eq (α := Measure (𝓧 × Ω))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.swap Ω 𝓧 ∘ₖ (Kernel.id ∥ₖ κ)) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
rw₁ :
  Eq (α := Measure (𝓧 × Ω))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap Ω Ω) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
⊢ Eq (α := Measure (𝓧 × Ω))
    (Measure.bind (α := Ω × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
        (⇑(Kernel.id ∥ₖ κ) : (a : Ω × Ω) → Measure (Ω × 𝓧)))
      (⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
have rw₂ : Eq (α := Measure (𝓧 × Ω)) ((⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap Ω Ω ∘ₖ Kernel.copy Ω) : (a : Ω) → Measure (𝓧 × Ω)) ∘ₘ μ)
  (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
    (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
Tactic: rw [Measure.comp_assoc, Kernel.swap_parallelComp, Measure.comp_assoc, Kernel.comp_assoc,
      Kernel.swap_copy, Measure.comp_assoc]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
rw :
  Eq (α := Measure (𝓧 × Ω))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.swap Ω 𝓧 ∘ₖ (Kernel.id ∥ₖ κ)) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
rw₁ :
  Eq (α := Measure (𝓧 × Ω))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap Ω Ω) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
rw₂ :
  Eq (α := Measure (𝓧 × Ω)) ((⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap Ω Ω ∘ₖ Kernel.copy Ω) : (a : Ω) → Measure (𝓧 × Ω)) ∘ₘ μ)
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
⊢ Eq (α := Measure (𝓧 × Ω))
    (Measure.bind (α := Ω × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
        (⇑(Kernel.id ∥ₖ κ) : (a : Ω × Ω) → Measure (Ω × 𝓧)))
      (⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
have rw₃ : Eq (α := Measure (𝓧 × Ω)) ((⇑(κ ∥ₖ Kernel.id ∘ₖ (Kernel.swap Ω Ω ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓧 × Ω)) ∘ₘ μ)
  (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
    (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
Tactic: rw [Measure.comp_assoc, Kernel.swap_parallelComp, Measure.comp_assoc, Kernel.comp_assoc,
      Kernel.swap_copy, Measure.comp_assoc]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
rw :
  Eq (α := Measure (𝓧 × Ω))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.swap Ω 𝓧 ∘ₖ (Kernel.id ∥ₖ κ)) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
rw₁ :
  Eq (α := Measure (𝓧 × Ω))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap Ω Ω) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
rw₂ :
  Eq (α := Measure (𝓧 × Ω)) ((⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap Ω Ω ∘ₖ Kernel.copy Ω) : (a : Ω) → Measure (𝓧 × Ω)) ∘ₘ μ)
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
rw₃ :
  Eq (α := Measure (𝓧 × Ω)) ((⇑(κ ∥ₖ Kernel.id ∘ₖ (Kernel.swap Ω Ω ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓧 × Ω)) ∘ₘ μ)
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
⊢ Eq (α := Measure (𝓧 × Ω))
    (Measure.bind (α := Ω × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
        (⇑(Kernel.id ∥ₖ κ) : (a : Ω × Ω) → Measure (Ω × 𝓧)))
      (⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
have rw₄ : Eq (α := Measure (𝓧 × Ω)) ((⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω) : (a : Ω) → Measure (𝓧 × Ω)) ∘ₘ μ)
  (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
    (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
Tactic: rw [Measure.comp_assoc, Kernel.swap_parallelComp, Measure.comp_assoc, Kernel.comp_assoc,
      Kernel.swap_copy, Measure.comp_assoc]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
rw :
  Eq (α := Measure (𝓧 × Ω))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.swap Ω 𝓧 ∘ₖ (Kernel.id ∥ₖ κ)) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
rw₁ :
  Eq (α := Measure (𝓧 × Ω))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap Ω Ω) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
rw₂ :
  Eq (α := Measure (𝓧 × Ω)) ((⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap Ω Ω ∘ₖ Kernel.copy Ω) : (a : Ω) → Measure (𝓧 × Ω)) ∘ₘ μ)
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
rw₃ :
  Eq (α := Measure (𝓧 × Ω)) ((⇑(κ ∥ₖ Kernel.id ∘ₖ (Kernel.swap Ω Ω ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓧 × Ω)) ∘ₘ μ)
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
rw₄ :
  Eq (α := Measure (𝓧 × Ω)) ((⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω) : (a : Ω) → Measure (𝓧 × Ω)) ∘ₘ μ)
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
⊢ Eq (α := Measure (𝓧 × Ω))
    (Measure.bind (α := Ω × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
        (⇑(Kernel.id ∥ₖ κ) : (a : Ω × Ω) → Measure (Ω × 𝓧)))
      (⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
have rw₅ : Eq (α := Measure (𝓧 × Ω)) ((⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω) : (a : Ω) → Measure (𝓧 × Ω)) ∘ₘ μ)
  ((⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω) : (a : Ω) → Measure (𝓧 × Ω)) ∘ₘ μ)
Tactic: rw [Measure.comp_assoc, Kernel.swap_parallelComp, Measure.comp_assoc, Kernel.comp_assoc,
      Kernel.swap_copy, Measure.comp_assoc]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
⊢ Eq (α := Measure (𝓧 × Ω))
    (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
      (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
have calc : Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
    (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
    (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)) =
  ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ
Tactic: calc (Kernel.id ∥ₖ κ†μ) ∘ₘ Kernel.copy 𝓧 ∘ₘ κ ∘ₘ μ
  _ = (κ ∘ₘ μ) ⊗ₘ κ†μ := by rw [← Measure.compProd_eq_parallelComp_comp_copy_comp]
  _ = Kernel.swap _ _ ∘ₘ (μ ⊗ₘ κ) := by rw [compProd_posterior_eq_swap_comp]
  _ = Kernel.swap _ _ ∘ₘ (Kernel.id ∥ₖ κ) ∘ₘ Kernel.copy Ω ∘ₘ μ := by
    rw [Measure.compProd_eq_parallelComp_comp_copy_comp]
  _ = (κ ∥ₖ Kernel.id) ∘ₘ Kernel.copy Ω ∘ₘ μ := by
    rw [Measure.comp_assoc, Kernel.swap_parallelComp, Measure.comp_assoc, Kernel.comp_assoc,
      Kernel.swap_copy, Measure.comp_assoc]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
calc :
  Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
      (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)) =
    ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ
⊢ Eq (α := Measure (𝓧 × Ω))
    (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
      (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
have calc₁ : ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ = (⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ
Tactic: calc (Kernel.id ∥ₖ κ†μ) ∘ₘ Kernel.copy 𝓧 ∘ₘ κ ∘ₘ μ
  _ = (κ ∘ₘ μ) ⊗ₘ κ†μ := by rw [← Measure.compProd_eq_parallelComp_comp_copy_comp]
  _ = Kernel.swap _ _ ∘ₘ (μ ⊗ₘ κ) := by rw [compProd_posterior_eq_swap_comp]
  _ = Kernel.swap _ _ ∘ₘ (Kernel.id ∥ₖ κ) ∘ₘ Kernel.copy Ω ∘ₘ μ := by
    rw [Measure.compProd_eq_parallelComp_comp_copy_comp]
  _ = (κ ∥ₖ Kernel.id) ∘ₘ Kernel.copy Ω ∘ₘ μ := by
    rw [Measure.comp_assoc, Kernel.swap_parallelComp, Measure.comp_assoc, Kernel.comp_assoc,
      Kernel.swap_copy, Measure.comp_assoc]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
calc :
  Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
      (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)) =
    ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ
calc₁ : ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ = (⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ
⊢ Eq (α := Measure (𝓧 × Ω))
    (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
      (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
have calc₂ : Eq (α := Measure (𝓧 × Ω)) ((⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ)
  (Measure.bind (α := Ω × 𝓧) (mα := Prod.instMeasurableSpace)
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ κ) : (a : Ω × Ω) → Measure (Ω × 𝓧)))
    (⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)))
Tactic: calc (Kernel.id ∥ₖ κ†μ) ∘ₘ Kernel.copy 𝓧 ∘ₘ κ ∘ₘ μ
  _ = (κ ∘ₘ μ) ⊗ₘ κ†μ := by rw [← Measure.compProd_eq_parallelComp_comp_copy_comp]
  _ = Kernel.swap _ _ ∘ₘ (μ ⊗ₘ κ) := by rw [compProd_posterior_eq_swap_comp]
  _ = Kernel.swap _ _ ∘ₘ (Kernel.id ∥ₖ κ) ∘ₘ Kernel.copy Ω ∘ₘ μ := by
    rw [Measure.compProd_eq_parallelComp_comp_copy_comp]
  _ = (κ ∥ₖ Kernel.id) ∘ₘ Kernel.copy Ω ∘ₘ μ := by
    rw [Measure.comp_assoc, Kernel.swap_parallelComp, Measure.comp_assoc, Kernel.comp_assoc,
      Kernel.swap_copy, Measure.comp_assoc]