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 Ω
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 (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ
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 (𝓧 × Ω)))
⊢ 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 (𝓧 × Ω))
  (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 (𝓧 × Ω)))
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 Ω
⊢ Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ ×ₖ Kernel.id) : (a : 𝓧) → Measure (Ω × 𝓧)) =
    μ ⊗ₘ κ
have rw : Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
    (⇑(Kernel.swap 𝓧 Ω ∘ₖ (Kernel.id ×ₖ κ†μ)) : (a : 𝓧) → Measure (Ω × 𝓧)) =
  μ ⊗ₘ κ
Tactic: rw [← Kernel.swap_prod, ← Measure.comp_assoc, ← Measure.compProd_eq_comp_prod,
    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α := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
      (⇑(Kernel.swap 𝓧 Ω ∘ₖ (Kernel.id ×ₖ κ†μ)) : (a : 𝓧) → Measure (Ω × 𝓧)) =
    μ ⊗ₘ κ
⊢ Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ ×ₖ Kernel.id) : (a : 𝓧) → Measure (Ω × 𝓧)) =
    μ ⊗ₘ κ
have rw₁ : Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
    (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
      (⇑(Kernel.id ×ₖ κ†μ) : (a : 𝓧) → Measure (𝓧 × Ω)))
    (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) =
  μ ⊗ₘ κ
Tactic: rw [← Kernel.swap_prod, ← Measure.comp_assoc, ← Measure.compProd_eq_comp_prod,
    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α := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
      (⇑(Kernel.swap 𝓧 Ω ∘ₖ (Kernel.id ×ₖ κ†μ)) : (a : 𝓧) → Measure (Ω × 𝓧)) =
    μ ⊗ₘ κ
rw₁ :
  Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        (⇑(Kernel.id ×ₖ κ†μ) : (a : 𝓧) → Measure (𝓧 × Ω)))
      (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) =
    μ ⊗ₘ κ
⊢ Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ ×ₖ Kernel.id) : (a : 𝓧) → Measure (Ω × 𝓧)) =
    μ ⊗ₘ κ
have rw₂ : (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) ∘ₘ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ = μ ⊗ₘ κ
Tactic: rw [← Kernel.swap_prod, ← Measure.comp_assoc, ← Measure.compProd_eq_comp_prod,
    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α := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
      (⇑(Kernel.swap 𝓧 Ω ∘ₖ (Kernel.id ×ₖ κ†μ)) : (a : 𝓧) → Measure (Ω × 𝓧)) =
    μ ⊗ₘ κ
rw₁ :
  Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        (⇑(Kernel.id ×ₖ κ†μ) : (a : 𝓧) → Measure (𝓧 × Ω)))
      (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) =
    μ ⊗ₘ κ
rw₂ : (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) ∘ₘ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ = μ ⊗ₘ κ
⊢ Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ ×ₖ Kernel.id) : (a : 𝓧) → Measure (Ω × 𝓧)) =
    μ ⊗ₘ κ
have rw₃ : Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
    ((⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ)
    (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) =
  μ ⊗ₘ κ
Tactic: rw [← Kernel.swap_prod, ← Measure.comp_assoc, ← Measure.compProd_eq_comp_prod,
    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α := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
      (⇑(Kernel.swap 𝓧 Ω ∘ₖ (Kernel.id ×ₖ κ†μ)) : (a : 𝓧) → Measure (Ω × 𝓧)) =
    μ ⊗ₘ κ
rw₁ :
  Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        (⇑(Kernel.id ×ₖ κ†μ) : (a : 𝓧) → Measure (𝓧 × Ω)))
      (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) =
    μ ⊗ₘ κ
rw₂ : (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) ∘ₘ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ = μ ⊗ₘ κ
rw₃ :
  Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ)
      (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) =
    μ ⊗ₘ κ
⊢ Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ ×ₖ Kernel.id) : (a : 𝓧) → Measure (Ω × 𝓧)) =
    μ ⊗ₘ κ
have rw₄ : (⇑(Kernel.swap 𝓧 Ω ∘ₖ Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (Ω × 𝓧)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ κ
Tactic: rw [← Kernel.swap_prod, ← Measure.comp_assoc, ← Measure.compProd_eq_comp_prod,
    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α := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
      (⇑(Kernel.swap 𝓧 Ω ∘ₖ (Kernel.id ×ₖ κ†μ)) : (a : 𝓧) → Measure (Ω × 𝓧)) =
    μ ⊗ₘ κ
rw₁ :
  Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        (⇑(Kernel.id ×ₖ κ†μ) : (a : 𝓧) → Measure (𝓧 × Ω)))
      (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) =
    μ ⊗ₘ κ
rw₂ : (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) ∘ₘ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ = μ ⊗ₘ κ
rw₃ :
  Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ)
      (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) =
    μ ⊗ₘ κ
rw₄ : (⇑(Kernel.swap 𝓧 Ω ∘ₖ Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (Ω × 𝓧)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ κ
⊢ Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ ×ₖ Kernel.id) : (a : 𝓧) → Measure (Ω × 𝓧)) =
    μ ⊗ₘ κ
have rw₅ : (⇑Kernel.id : (a : Ω × 𝓧) → Measure (Ω × 𝓧)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ κ
Tactic: rw [← Kernel.swap_prod, ← Measure.comp_assoc, ← Measure.compProd_eq_comp_prod,
    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α := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
      (⇑(Kernel.swap 𝓧 Ω ∘ₖ (Kernel.id ×ₖ κ†μ)) : (a : 𝓧) → Measure (Ω × 𝓧)) =
    μ ⊗ₘ κ
rw₁ :
  Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        (⇑(Kernel.id ×ₖ κ†μ) : (a : 𝓧) → Measure (𝓧 × Ω)))
      (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) =
    μ ⊗ₘ κ
rw₂ : (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) ∘ₘ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ = μ ⊗ₘ κ
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 (Ω × 𝓧)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ κ
⊢ Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ ×ₖ Kernel.id) : (a : 𝓧) → Measure (Ω × 𝓧)) =
    μ ⊗ₘ κ
have rw₆ : μ ⊗ₘ κ = μ ⊗ₘ κ
Tactic: rw [← Kernel.swap_prod, ← Measure.comp_assoc, ← Measure.compProd_eq_comp_prod,
    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 Ω
η : Kernel 𝓧 Ω
inst_4 : IsFiniteKernel η
h : ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ η = (⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ
⊢ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ η = Measure.map Prod.swap (μ ⊗ₘ κ)
have rw : Eq (α := Measure (𝓧 × Ω)) ((⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ)
  (Measure.map Prod.swap (μ ⊗ₘ κ))
Tactic: rw [h, Measure.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 Ω
η : Kernel 𝓧 Ω
inst_4 : IsFiniteKernel η
h : ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ η = (⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ
rw :
  Eq (α := Measure (𝓧 × Ω)) ((⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ)
    (Measure.map Prod.swap (μ ⊗ₘ κ))
⊢ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ η = Measure.map Prod.swap (μ ⊗ₘ κ)
have rw₁ : Eq (α := Measure (𝓧 × Ω)) (Measure.map Prod.swap (μ ⊗ₘ κ)) (Measure.map Prod.swap (μ ⊗ₘ κ))
Tactic: rw [h, Measure.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 Ω
inst_4 : IsMarkovKernel κ
⊢ Measure.bind.{u_2, u_1} (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ) : (a : 𝓧) → Measure Ω) = μ
have rw : (((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ).snd = μ
Tactic: rw [← Measure.snd_compProd, compProd_posterior_eq_map_swap, Measure.snd_map_swap,
    Measure.fst_compProd]
-- 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 Ω
inst_4 : IsMarkovKernel κ
rw : (((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ).snd = μ
⊢ Measure.bind.{u_2, u_1} (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ) : (a : 𝓧) → Measure Ω) = μ
have rw₁ : Measure.snd (Measure.map Prod.swap (μ ⊗ₘ κ)) = μ
Tactic: rw [← Measure.snd_compProd, compProd_posterior_eq_map_swap, Measure.snd_map_swap,
    Measure.fst_compProd]
-- 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 Ω
inst_4 : IsMarkovKernel κ
rw : (((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ).snd = μ
rw₁ : Measure.snd (Measure.map Prod.swap (μ ⊗ₘ κ)) = μ
⊢ Measure.bind.{u_2, u_1} (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ) : (a : 𝓧) → Measure Ω) = μ
have rw₂ : (μ ⊗ₘ κ).fst = μ
Tactic: rw [← Measure.snd_compProd, compProd_posterior_eq_map_swap, Measure.snd_map_swap,
    Measure.fst_compProd]
-- 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 Ω
inst_4 : IsMarkovKernel κ
rw : (((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ).snd = μ
rw₁ : Measure.snd (Measure.map Prod.swap (μ ⊗ₘ κ)) = μ
rw₂ : (μ ⊗ₘ κ).fst = μ
⊢ Measure.bind.{u_2, u_1} (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ) : (a : 𝓧) → Measure Ω) = μ
have rw₃ : μ = μ
Tactic: rw [← Measure.snd_compProd, compProd_posterior_eq_map_swap, Measure.snd_map_swap,
    Measure.fst_compProd]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
this :
  (ae (F := Measure Ω) ((⇑Kernel.id : (a : Ω) → Measure Ω) ∘ₘ μ)).EventuallyEq (β := Measure Ω)
    (⇑Kernel.id : (a : Ω) → Measure Ω) (⇑(Kernel.id†μ) : (a : Ω) → Measure Ω)
⊢ (ae μ).EventuallyEq (β := Measure Ω) (⇑(Kernel.id†μ) : (a : Ω) → Measure Ω) (⇑Kernel.id : (a : Ω) → Measure Ω)
have this₁ : (ae μ).EventuallyEq (β := Measure Ω) (⇑Kernel.id : (a : Ω) → Measure Ω) (⇑(Kernel.id†μ) : (a : Ω) → Measure Ω)
Tactic: rw [Measure.id_comp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
this : (ae μ).EventuallyEq (β := Measure Ω) (⇑Kernel.id : (a : Ω) → Measure Ω) (⇑(Kernel.id†μ) : (a : Ω) → Measure Ω)
⊢ (ae μ).EventuallyEq (β := Measure Ω) (⇑(Kernel.id†μ) : (a : Ω) → Measure Ω) (⇑Kernel.id : (a : Ω) → Measure Ω)
have h : ∀ (a : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω)
          {x : Ω |
            (fun (x : Ω) ↦
                Eq (α := Measure Ω) ((Kernel.id : (a : Ω) → Measure Ω) x : Measure Ω)
                  ((Kernel.id†μ : (a : Ω) → Measure Ω) x : Measure Ω))
              x}
          x →
        Membership.mem (γ := Set Ω)
          {x : Ω |
            (fun (x : Ω) ↦
                Eq (α := Measure Ω) ((Kernel.id†μ : (a : Ω) → Measure Ω) x : Measure Ω)
                  ((Kernel.id : (a : Ω) → Measure Ω) x : Measure Ω))
              x}
          x}
    a
Tactic: filter_upwards [this] with a ha using ha.symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
this : (ae μ).EventuallyEq (β := Measure Ω) (⇑Kernel.id : (a : Ω) → Measure Ω) (⇑(Kernel.id†μ) : (a : Ω) → Measure Ω)
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (x : Ω) ↦
                  Eq (α := Measure Ω) ((Kernel.id : (a : Ω) → Measure Ω) x : Measure Ω)
                    ((Kernel.id†μ : (a : Ω) → Measure Ω) x : Measure Ω))
                x}
            x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (x : Ω) ↦
                  Eq (α := Measure Ω) ((Kernel.id†μ : (a : Ω) → Measure Ω) x : Measure Ω)
                    ((Kernel.id : (a : Ω) → Measure Ω) x : Measure Ω))
                x}
            x}
      a
⊢ (ae μ).EventuallyEq (β := Measure Ω) (⇑(Kernel.id†μ) : (a : Ω) → Measure Ω) (⇑Kernel.id : (a : Ω) → Measure Ω)
have h₁ : ∀ (a : Ω),
  Eq (α := Measure Ω) ((Kernel.id : (a : Ω) → Measure Ω) a : Measure Ω)
      ((Kernel.id†μ : (a : Ω) → Measure Ω) a : Measure Ω) →
    Eq (α := Measure Ω) ((Kernel.id†μ : (a : Ω) → Measure Ω) a : Measure Ω)
      ((Kernel.id : (a : Ω) → Measure Ω) a : Measure Ω)
Tactic: filter_upwards [this] with a ha using ha.symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
⊢ (ae μ).EventuallyEq (β := Measure Ω) (⇑(Kernel.id†μ) : (a : Ω) → Measure Ω) (⇑Kernel.id : (a : Ω) → Measure Ω)
have suffices : (ae (F := Measure Ω) ((⇑Kernel.id : (a : Ω) → Measure Ω) ∘ₘ μ)).EventuallyEq (β := Measure Ω)
  (⇑Kernel.id : (a : Ω) → Measure Ω) (⇑(Kernel.id†μ) : (a : Ω) → Measure Ω)
Tactic: suffices Kernel.id =ᵐ[Kernel.id ∘ₘ μ] (Kernel.id : Kernel Ω Ω)†μ by
    rw [Measure.id_comp] at this
    filter_upwards [this] with a ha using ha.symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
⊢ (ae (F := Measure Ω) ((⇑Kernel.id : (a : Ω) → Measure Ω) ∘ₘ μ)).EventuallyEq (β := Measure Ω)
    (⇑Kernel.id : (a : Ω) → Measure Ω) (⇑(Kernel.id†μ) : (a : Ω) → Measure Ω)
have refine : Eq (α := Measure (Ω × Ω)) (((⇑Kernel.id : (a : Ω) → Measure Ω) ∘ₘ μ) ⊗ₘ Kernel.id)
  ((⇑(Kernel.swap Ω Ω) : (a : Ω × Ω) → Measure (Ω × Ω)) ∘ₘ μ ⊗ₘ Kernel.id)
Tactic: refine ae_eq_posterior_of_compProd_eq_swap_comp Kernel.id ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
⊢ Eq (α := Measure (Ω × Ω)) (((⇑Kernel.id : (a : Ω) → Measure Ω) ∘ₘ μ) ⊗ₘ Kernel.id)
    ((⇑(Kernel.swap Ω Ω) : (a : Ω × Ω) → Measure (Ω × Ω)) ∘ₘ μ ⊗ₘ Kernel.id)
have rw : μ ⊗ₘ Kernel.id = (⇑(Kernel.swap Ω Ω) : (a : Ω × Ω) → Measure (Ω × Ω)) ∘ₘ μ ⊗ₘ Kernel.id
Tactic: rw [Measure.id_comp, Measure.compProd_id_eq_copy_comp, Measure.comp_assoc, Kernel.swap_copy]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
rw : μ ⊗ₘ Kernel.id = (⇑(Kernel.swap Ω Ω) : (a : Ω × Ω) → Measure (Ω × Ω)) ∘ₘ μ ⊗ₘ Kernel.id
⊢ Eq (α := Measure (Ω × Ω)) (((⇑Kernel.id : (a : Ω) → Measure Ω) ∘ₘ μ) ⊗ₘ Kernel.id)
    ((⇑(Kernel.swap Ω Ω) : (a : Ω × Ω) → Measure (Ω × Ω)) ∘ₘ μ ⊗ₘ Kernel.id)
have rw₁ : Eq (α := Measure (Ω × Ω)) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
  (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
    (⇑(Kernel.swap Ω Ω) : (a : Ω × Ω) → Measure (Ω × Ω)))
Tactic: rw [Measure.id_comp, Measure.compProd_id_eq_copy_comp, Measure.comp_assoc, Kernel.swap_copy]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
rw : μ ⊗ₘ Kernel.id = (⇑(Kernel.swap Ω Ω) : (a : Ω × Ω) → Measure (Ω × Ω)) ∘ₘ μ ⊗ₘ Kernel.id
rw₁ :
  Eq (α := Measure (Ω × Ω)) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.swap Ω Ω) : (a : Ω × Ω) → Measure (Ω × Ω)))
⊢ Eq (α := Measure (Ω × Ω)) (((⇑Kernel.id : (a : Ω) → Measure Ω) ∘ₘ μ) ⊗ₘ Kernel.id)
    ((⇑(Kernel.swap Ω Ω) : (a : Ω × Ω) → Measure (Ω × Ω)) ∘ₘ μ ⊗ₘ Kernel.id)
have rw₂ : Eq (α := Measure (Ω × Ω)) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
  ((⇑(Kernel.swap Ω Ω ∘ₖ Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
Tactic: rw [Measure.id_comp, Measure.compProd_id_eq_copy_comp, Measure.comp_assoc, Kernel.swap_copy]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
rw : μ ⊗ₘ Kernel.id = (⇑(Kernel.swap Ω Ω) : (a : Ω × Ω) → Measure (Ω × Ω)) ∘ₘ μ ⊗ₘ Kernel.id
rw₁ :
  Eq (α := Measure (Ω × Ω)) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.swap Ω Ω) : (a : Ω × Ω) → Measure (Ω × Ω)))
rw₂ :
  Eq (α := Measure (Ω × Ω)) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
    ((⇑(Kernel.swap Ω Ω ∘ₖ Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
⊢ Eq (α := Measure (Ω × Ω)) (((⇑Kernel.id : (a : Ω) → Measure Ω) ∘ₘ μ) ⊗ₘ Kernel.id)
    ((⇑(Kernel.swap Ω Ω) : (a : Ω × Ω) → Measure (Ω × Ω)) ∘ₘ μ ⊗ₘ Kernel.id)
have rw₃ : Eq (α := Measure (Ω × Ω)) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
  ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
Tactic: rw [Measure.id_comp, Measure.compProd_id_eq_copy_comp, Measure.comp_assoc, Kernel.swap_copy]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ (ae (F := Measure 𝓧) (Measure.map f μ)).EventuallyEq (β := Measure 𝓧)
    (⇑(Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) : (a : 𝓧) → Measure 𝓧)
    (⇑Kernel.id : (a : 𝓧) → Measure 𝓧)
have refine : Measure.map f μ ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) = Measure.map f μ ⊗ₘ Kernel.id
Tactic: refine Kernel.ae_eq_of_compProd_eq ?_