awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst_6 : IsFiniteKernel η
⊢ Eq (α := Measure (𝓨 × Ω))
    (Measure.bind (α := 𝓨 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
          (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
        (⇑(η ∥ₖ Kernel.id) : (a : 𝓧 × 𝓧) → Measure (𝓨 × 𝓧)))
      (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓨 × 𝓧) → Measure (𝓨 × Ω)))
    (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
          (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
        (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)))
      (⇑(η ∥ₖ Kernel.id) : (a : 𝓧 × Ω) → Measure (𝓨 × Ω)))
have rw : Eq (α := Measure (𝓨 × Ω))
  (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
    (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
    (⇑(Kernel.id ∥ₖ κ†μ ∘ₖ (η ∥ₖ Kernel.id)) : (a : 𝓧 × 𝓧) → Measure (𝓨 × Ω)))
  (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
    (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
      (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)))
    (⇑(η ∥ₖ Kernel.id) : (a : 𝓧 × Ω) → Measure (𝓨 × Ω)))
Tactic: rw [Measure.comp_assoc, Kernel.parallelComp_comm, ← Measure.comp_assoc]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst_6 : IsFiniteKernel η
rw :
  Eq (α := Measure (𝓨 × Ω))
    (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
      (⇑(Kernel.id ∥ₖ κ†μ ∘ₖ (η ∥ₖ Kernel.id)) : (a : 𝓧 × 𝓧) → Measure (𝓨 × Ω)))
    (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
          (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
        (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)))
      (⇑(η ∥ₖ Kernel.id) : (a : 𝓧 × Ω) → Measure (𝓨 × Ω)))
⊢ Eq (α := Measure (𝓨 × Ω))
    (Measure.bind (α := 𝓨 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
          (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
        (⇑(η ∥ₖ Kernel.id) : (a : 𝓧 × 𝓧) → Measure (𝓨 × 𝓧)))
      (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓨 × 𝓧) → Measure (𝓨 × Ω)))
    (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
          (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
        (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)))
      (⇑(η ∥ₖ Kernel.id) : (a : 𝓧 × Ω) → Measure (𝓨 × Ω)))
have rw₁ : Eq (α := Measure (𝓨 × Ω))
  (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
    (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
    (⇑(η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ†μ)) : (a : 𝓧 × 𝓧) → Measure (𝓨 × Ω)))
  (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
    (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
      (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)))
    (⇑(η ∥ₖ Kernel.id) : (a : 𝓧 × Ω) → Measure (𝓨 × Ω)))
Tactic: rw [Measure.comp_assoc, Kernel.parallelComp_comm, ← Measure.comp_assoc]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst_6 : IsFiniteKernel η
⊢ Eq (α := Measure (𝓨 × Ω))
    (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
          (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
        (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)))
      (⇑(η ∥ₖ Kernel.id) : (a : 𝓧 × Ω) → Measure (𝓨 × Ω)))
    (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
        (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
      (⇑(η ∥ₖ Kernel.id) : (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.id) : (a : 𝓧 × Ω) → Measure (𝓨 × Ω)))
  (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
    (⇑(η ∥ₖ Kernel.id) : (a : 𝓧 × Ω) → Measure (𝓨 × Ω)))
Tactic: rw [parallelProd_posterior_comp_copy_comp]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst_6 : IsFiniteKernel η
⊢ Eq (α := Measure (𝓨 × Ω))
    (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
        (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
      (⇑(η ∥ₖ Kernel.id) : (a : 𝓧 × Ω) → Measure (𝓨 × Ω)))
    (Measure.bind (α := Ω × 𝓨) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × 𝓧) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace)
          ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ) (⇑(Kernel.id ∥ₖ κ) : (a : Ω × Ω) → Measure (Ω × 𝓧)))
        (⇑(Kernel.id ∥ₖ η) : (a : Ω × 𝓧) → Measure (Ω × 𝓨)))
      (⇑(Kernel.swap Ω 𝓨) : (a : Ω × 𝓨) → Measure (𝓨 × Ω)))
have simp_rw : Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
  ((⇑(Kernel.swap Ω 𝓨 ∘ₖ (Kernel.id ∥ₖ η ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω))) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
Tactic: simp_rw [Measure.comp_assoc]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst_6 : IsFiniteKernel η
| (⇑(Kernel.swap Ω 𝓨 ∘ₖ (Kernel.id ∥ₖ η ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω))) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ
have rw : (⇑(Kernel.swap Ω 𝓨 ∘ₖ (Kernel.id ∥ₖ η) ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ
Tactic: rw [← Kernel.comp_assoc]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst_6 : IsFiniteKernel η
⊢ Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(Kernel.swap Ω 𝓨 ∘ₖ (Kernel.id ∥ₖ η ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω))) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
have conv_rhs : Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
  ((⇑(Kernel.swap Ω 𝓨 ∘ₖ (Kernel.id ∥ₖ η) ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
Tactic: conv_rhs => rw [← Kernel.comp_assoc]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst_6 : IsFiniteKernel η
⊢ Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(Kernel.swap Ω 𝓨 ∘ₖ (Kernel.id ∥ₖ η) ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
have rw : Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
  ((⇑(η ∥ₖ Kernel.id ∘ₖ Kernel.swap Ω 𝓧 ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
Tactic: rw [Kernel.swap_parallelComp, Kernel.comp_assoc, ← Kernel.comp_assoc (Kernel.swap Ω 𝓧),
      Kernel.swap_parallelComp, Kernel.comp_assoc, Kernel.swap_copy]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst_6 : IsFiniteKernel η
rw :
  Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(η ∥ₖ Kernel.id ∘ₖ Kernel.swap Ω 𝓧 ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
⊢ Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(Kernel.swap Ω 𝓨 ∘ₖ (Kernel.id ∥ₖ η) ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
have rw₁ : Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
  ((⇑(η ∥ₖ Kernel.id ∘ₖ (Kernel.swap Ω 𝓧 ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω))) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
Tactic: rw [Kernel.swap_parallelComp, Kernel.comp_assoc, ← Kernel.comp_assoc (Kernel.swap Ω 𝓧),
      Kernel.swap_parallelComp, Kernel.comp_assoc, Kernel.swap_copy]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst_6 : IsFiniteKernel η
rw :
  Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(η ∥ₖ Kernel.id ∘ₖ Kernel.swap Ω 𝓧 ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
rw₁ :
  Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(η ∥ₖ Kernel.id ∘ₖ (Kernel.swap Ω 𝓧 ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω))) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
⊢ Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(Kernel.swap Ω 𝓨 ∘ₖ (Kernel.id ∥ₖ η) ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
have rw₂ : Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
  ((⇑(η ∥ₖ Kernel.id ∘ₖ (Kernel.swap Ω 𝓧 ∘ₖ (Kernel.id ∥ₖ κ) ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
Tactic: rw [Kernel.swap_parallelComp, Kernel.comp_assoc, ← Kernel.comp_assoc (Kernel.swap Ω 𝓧),
      Kernel.swap_parallelComp, Kernel.comp_assoc, Kernel.swap_copy]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst_6 : IsFiniteKernel η
rw :
  Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(η ∥ₖ Kernel.id ∘ₖ Kernel.swap Ω 𝓧 ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
rw₁ :
  Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(η ∥ₖ Kernel.id ∘ₖ (Kernel.swap Ω 𝓧 ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω))) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
rw₂ :
  Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(η ∥ₖ Kernel.id ∘ₖ (Kernel.swap Ω 𝓧 ∘ₖ (Kernel.id ∥ₖ κ) ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
⊢ Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(Kernel.swap Ω 𝓨 ∘ₖ (Kernel.id ∥ₖ η) ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
have rw₃ : Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
  ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.swap Ω Ω ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
Tactic: rw [Kernel.swap_parallelComp, Kernel.comp_assoc, ← Kernel.comp_assoc (Kernel.swap Ω 𝓧),
      Kernel.swap_parallelComp, Kernel.comp_assoc, Kernel.swap_copy]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst_6 : IsFiniteKernel η
rw :
  Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(η ∥ₖ Kernel.id ∘ₖ Kernel.swap Ω 𝓧 ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
rw₁ :
  Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(η ∥ₖ Kernel.id ∘ₖ (Kernel.swap Ω 𝓧 ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω))) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
rw₂ :
  Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(η ∥ₖ Kernel.id ∘ₖ (Kernel.swap Ω 𝓧 ∘ₖ (Kernel.id ∥ₖ κ) ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
rw₃ :
  Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.swap Ω Ω ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
⊢ Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(Kernel.swap Ω 𝓨 ∘ₖ (Kernel.id ∥ₖ η) ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
have rw₄ : Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
  ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ (Kernel.swap Ω Ω ∘ₖ Kernel.copy Ω))) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
Tactic: rw [Kernel.swap_parallelComp, Kernel.comp_assoc, ← Kernel.comp_assoc (Kernel.swap Ω 𝓧),
      Kernel.swap_parallelComp, Kernel.comp_assoc, Kernel.swap_copy]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst_6 : IsFiniteKernel η
rw :
  Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(η ∥ₖ Kernel.id ∘ₖ Kernel.swap Ω 𝓧 ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
rw₁ :
  Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(η ∥ₖ Kernel.id ∘ₖ (Kernel.swap Ω 𝓧 ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω))) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
rw₂ :
  Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(η ∥ₖ Kernel.id ∘ₖ (Kernel.swap Ω 𝓧 ∘ₖ (Kernel.id ∥ₖ κ) ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
rw₃ :
  Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.swap Ω Ω ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
rw₄ :
  Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ (Kernel.swap Ω Ω ∘ₖ Kernel.copy Ω))) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
⊢ Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(Kernel.swap Ω 𝓨 ∘ₖ (Kernel.id ∥ₖ η) ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
have rw₅ : Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
  ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
Tactic: rw [Kernel.swap_parallelComp, Kernel.comp_assoc, ← Kernel.comp_assoc (Kernel.swap Ω 𝓧),
      Kernel.swap_parallelComp, Kernel.comp_assoc, Kernel.swap_copy]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
inst_4 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst_6 : IsFiniteKernel η
⊢ Eq (α := Measure (𝓨 × Ω))
    (Measure.bind (α := 𝓨 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓨 × 𝓨) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := 𝓨) (mα := m𝓨)
          (Measure.bind.{u_2, u_3} (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑η : (a : 𝓧) → Measure 𝓨))
          (⇑(Kernel.copy 𝓨) : (a : 𝓨) → Measure (𝓨 × 𝓨)))
        (⇑(Kernel.id ∥ₖ η†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) : (a : 𝓨 × 𝓨) → Measure (𝓨 × 𝓧)))
      (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓨 × 𝓧) → Measure (𝓨 × Ω)))
    (Measure.bind (α := Ω × 𝓨) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × 𝓧) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace)
          ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ) (⇑(Kernel.id ∥ₖ κ) : (a : Ω × Ω) → Measure (Ω × 𝓧)))
        (⇑(Kernel.id ∥ₖ η) : (a : Ω × 𝓧) → Measure (Ω × 𝓨)))
      (⇑(Kernel.swap Ω 𝓨) : (a : Ω × 𝓨) → Measure (𝓨 × Ω)))
have calc : Eq (α := Measure (𝓨 × Ω))
  (Measure.bind (α := 𝓨 × 𝓧) (mα := Prod.instMeasurableSpace)
    (Measure.bind (α := 𝓨 × 𝓨) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓨) (mα := m𝓨)
        (Measure.bind.{u_2, u_3} (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑η : (a : 𝓧) → Measure 𝓨))
        (⇑(Kernel.copy 𝓨) : (a : 𝓨) → Measure (𝓨 × 𝓨)))
      (⇑(Kernel.id ∥ₖ η†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) : (a : 𝓨 × 𝓨) → Measure (𝓨 × 𝓧)))
    (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓨 × 𝓧) → Measure (𝓨 × Ω)))
  (Measure.bind (α := 𝓨 × 𝓧) (mα := Prod.instMeasurableSpace)
    (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
      (⇑(η ∥ₖ Kernel.id) : (a : 𝓧 × 𝓧) → Measure (𝓨 × 𝓧)))
    (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓨 × 𝓧) → Measure (𝓨 × Ω)))
Tactic: calc (Kernel.id ∥ₖ κ†μ) ∘ₘ (Kernel.id ∥ₖ η†(κ ∘ₘ μ)) ∘ₘ (Kernel.copy 𝓨) ∘ₘ η ∘ₘ κ ∘ₘ μ
  _ = (Kernel.id ∥ₖ κ†μ) ∘ₘ (η ∥ₖ Kernel.id) ∘ₘ Kernel.copy 𝓧 ∘ₘ κ ∘ₘ μ := by
    rw [parallelProd_posterior_comp_copy_comp]
  _ = (η ∥ₖ Kernel.id) ∘ₘ (Kernel.id ∥ₖ κ†μ) ∘ₘ Kernel.copy 𝓧 ∘ₘ κ ∘ₘ μ := by
    rw [Measure.comp_assoc, Kernel.parallelComp_comm, ← Measure.comp_assoc]
  _ = (η ∥ₖ Kernel.id) ∘ₘ (κ ∥ₖ Kernel.id) ∘ₘ Kernel.copy Ω ∘ₘ μ := by
    rw [parallelProd_posterior_comp_copy_comp]
  _ = (Kernel.swap _ _) ∘ₘ (Kernel.id ∥ₖ η) ∘ₘ (Kernel.id ∥ₖ κ) ∘ₘ Kernel.copy Ω ∘ₘ μ := by
    simp_rw [Measure.comp_assoc]
    conv_rhs => rw [← Kernel.comp_assoc]
    rw [Kernel.swap_parallelComp, Kernel.comp_assoc, ← Kernel.comp_assoc (Kernel.swap Ω 𝓧),
      Kernel.swap_parallelComp, Kernel.comp_assoc, Kernel.swap_copy]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (hypothesis)
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 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (b : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ, (κ†μ : (a : 𝓧) → Measure Ω) b ≪ μ
this : μ ⊗ₘ κ ≪ μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
have this₁ : μ ⊗ₘ κ ≪ μ ⊗ₘ Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
Tactic: rw [← Measure.compProd_const] at this
Cleared hypotheses: this
-- 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 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (b : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ, (κ†μ : (a : 𝓧) → Measure Ω) b ≪ μ
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
have suffices : μ ⊗ₘ κ ≪ μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
Tactic: suffices μ ⊗ₘ κ ≪ μ.prod (κ ∘ₘ μ) by
    rw [← Measure.compProd_const] at this
    simpa using this.kernel_of_compProd