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 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ Measure.map f μ ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) =
    ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ
      (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ)
have rw : Measure.map f μ ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) =
  Measure.map f μ ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ)
Tactic: rw [Measure.deterministic_comp_eq_map]
-- 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
⊢ ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ
      (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) =
    Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ)
          (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
        (⇑(Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)))
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : 𝓧 × Ω) → Measure (𝓧 × 𝓧))
have rw : Eq (α := Measure (𝓧 × 𝓧))
  (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
    (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ)
      (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
    (⇑(Kernel.id ∥ₖ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ)) : (a : 𝓧 × 𝓧) → Measure (𝓧 × 𝓧)))
  (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
    (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
      (⇑(Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)))
    (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : 𝓧 × Ω) → Measure (𝓧 × 𝓧)))
Tactic: rw [Measure.compProd_eq_parallelComp_comp_copy_comp,
      ← Kernel.parallelComp_id_left_comp_parallelComp, ← Measure.comp_assoc]
-- 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
rw :
  Eq (α := Measure (𝓧 × 𝓧))
    (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
      (⇑(Kernel.id ∥ₖ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ)) : (a : 𝓧 × 𝓧) → Measure (𝓧 × 𝓧)))
    (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ)
          (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
        (⇑(Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)))
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : 𝓧 × Ω) → Measure (𝓧 × 𝓧)))
⊢ ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ
      (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) =
    Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ)
          (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
        (⇑(Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)))
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : 𝓧 × Ω) → Measure (𝓧 × 𝓧))
have rw₁ : Eq (α := Measure (𝓧 × 𝓧))
  (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
    (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ)
      (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
    (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf ∘ₖ (Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ)) :
      (a : 𝓧 × 𝓧) → Measure (𝓧 × 𝓧)))
  (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
    (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
      (⇑(Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)))
    (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : 𝓧 × Ω) → Measure (𝓧 × 𝓧)))
Tactic: rw [Measure.compProd_eq_parallelComp_comp_copy_comp,
      ← Kernel.parallelComp_id_left_comp_parallelComp, ← Measure.comp_assoc]
-- 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
⊢ Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧))
    (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
        (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ)
          (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
        (⇑(Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)))
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : 𝓧 × Ω) → Measure (𝓧 × 𝓧)))
    (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
        (⇑(Kernel.deterministic f hf ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : 𝓧 × Ω) → Measure (𝓧 × 𝓧)))
have rw : Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧))
  (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.deterministic f hf ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
    (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : 𝓧 × Ω) → Measure (𝓧 × 𝓧)))
  (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.deterministic f hf ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
    (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (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
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧))
    (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
        (⇑(Kernel.deterministic f hf ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : 𝓧 × Ω) → Measure (𝓧 × 𝓧)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) : (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
have rw : Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧))
  (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
    (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf ∥ₖ Kernel.id)) :
      (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
  (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
    (⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) : (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
Tactic: rw [Measure.comp_assoc, Kernel.parallelComp_comp_parallelComp, Kernel.id_comp, Kernel.comp_id]
-- 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
rw :
  Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf ∥ₖ Kernel.id)) :
        (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) : (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
⊢ Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧))
    (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
        (⇑(Kernel.deterministic f hf ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : 𝓧 × Ω) → Measure (𝓧 × 𝓧)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) : (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
have rw₁ : Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧))
  (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
    (⇑(Kernel.id ∘ₖ Kernel.deterministic f hf ∥ₖ (Kernel.deterministic f hf ∘ₖ Kernel.id)) :
      (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
  (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
    (⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) : (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
Tactic: rw [Measure.comp_assoc, Kernel.parallelComp_comp_parallelComp, Kernel.id_comp, Kernel.comp_id]
-- 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
rw :
  Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf ∥ₖ Kernel.id)) :
        (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) : (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
rw₁ :
  Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.id ∘ₖ Kernel.deterministic f hf ∥ₖ (Kernel.deterministic f hf ∘ₖ Kernel.id)) :
        (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) : (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
⊢ Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧))
    (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
        (⇑(Kernel.deterministic f hf ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : 𝓧 × Ω) → Measure (𝓧 × 𝓧)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) : (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
have rw₂ : Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧))
  (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
    (⇑(Kernel.deterministic f hf ∥ₖ (Kernel.deterministic f hf ∘ₖ Kernel.id)) : (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
  (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
    (⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) : (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
Tactic: rw [Measure.comp_assoc, Kernel.parallelComp_comp_parallelComp, Kernel.id_comp, Kernel.comp_id]
-- 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
rw :
  Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf ∥ₖ Kernel.id)) :
        (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) : (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
rw₁ :
  Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.id ∘ₖ Kernel.deterministic f hf ∥ₖ (Kernel.deterministic f hf ∘ₖ Kernel.id)) :
        (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) : (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
rw₂ :
  Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.deterministic f hf ∥ₖ (Kernel.deterministic f hf ∘ₖ Kernel.id)) : (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) : (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
⊢ Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧))
    (Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
        (⇑(Kernel.deterministic f hf ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : 𝓧 × Ω) → Measure (𝓧 × 𝓧)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) : (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
have rw₃ : Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧))
  (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
    (⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) : (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
  (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
    (⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) : (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
Tactic: rw [Measure.comp_assoc, Kernel.parallelComp_comp_parallelComp, Kernel.id_comp, Kernel.comp_id]
-- 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
⊢ Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) : (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
    ((⇑(Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) : (a : Ω) → Measure (𝓧 × 𝓧)) ∘ₘ μ)
have rw : Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧))
  ((⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf ∘ₖ Kernel.copy Ω) : (a : Ω) → Measure (𝓧 × 𝓧)) ∘ₘ μ)
  ((⇑(Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) : (a : Ω) → Measure (𝓧 × 𝓧)) ∘ₘ μ)
Tactic: rw [Measure.comp_assoc, Kernel.parallelComp_self_comp_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
rw :
  Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧))
    ((⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf ∘ₖ Kernel.copy Ω) : (a : Ω) → Measure (𝓧 × 𝓧)) ∘ₘ μ)
    ((⇑(Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) : (a : Ω) → Measure (𝓧 × 𝓧)) ∘ₘ μ)
⊢ Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) : (a : Ω × Ω) → Measure (𝓧 × 𝓧)))
    ((⇑(Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) : (a : Ω) → Measure (𝓧 × 𝓧)) ∘ₘ μ)
have rw₁ : Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧)) ((⇑(Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) : (a : Ω) → Measure (𝓧 × 𝓧)) ∘ₘ μ)
  ((⇑(Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) : (a : Ω) → Measure (𝓧 × 𝓧)) ∘ₘ μ)
Tactic: rw [Measure.comp_assoc, Kernel.parallelComp_self_comp_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
⊢ Eq (α := Measure (𝓧 × 𝓧)) ((⇑(Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) : (a : Ω) → Measure (𝓧 × 𝓧)) ∘ₘ μ)
    (Measure.map f μ ⊗ₘ Kernel.id)
have rw : Eq (α := Measure (𝓧 × 𝓧)) ((⇑(Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) : (a : Ω) → Measure (𝓧 × 𝓧)) ∘ₘ μ)
  (Measure.bind (mα := m𝓧) (Measure.map f μ) (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
Tactic: rw [Measure.compProd_id_eq_copy_comp, ← Measure.comp_assoc,
      Measure.deterministic_comp_eq_map]
-- 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
rw :
  Eq (α := Measure (𝓧 × 𝓧)) ((⇑(Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) : (a : Ω) → Measure (𝓧 × 𝓧)) ∘ₘ μ)
    (Measure.bind (mα := m𝓧) (Measure.map f μ) (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
⊢ Eq (α := Measure (𝓧 × 𝓧)) ((⇑(Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) : (a : Ω) → Measure (𝓧 × 𝓧)) ∘ₘ μ)
    (Measure.map f μ ⊗ₘ Kernel.id)
have rw₁ : Eq (α := Measure (𝓧 × 𝓧))
  (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ)
    (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
  (Measure.bind (mα := m𝓧) (Measure.map f μ) (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
Tactic: rw [Measure.compProd_id_eq_copy_comp, ← Measure.comp_assoc,
      Measure.deterministic_comp_eq_map]
-- 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
rw :
  Eq (α := Measure (𝓧 × 𝓧)) ((⇑(Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) : (a : Ω) → Measure (𝓧 × 𝓧)) ∘ₘ μ)
    (Measure.bind (mα := m𝓧) (Measure.map f μ) (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
rw₁ :
  Eq (α := Measure (𝓧 × 𝓧))
    (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ)
      (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
    (Measure.bind (mα := m𝓧) (Measure.map f μ) (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
⊢ Eq (α := Measure (𝓧 × 𝓧)) ((⇑(Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) : (a : Ω) → Measure (𝓧 × 𝓧)) ∘ₘ μ)
    (Measure.map f μ ⊗ₘ Kernel.id)
have rw₂ : Eq (α := Measure (𝓧 × 𝓧)) (Measure.bind (mα := m𝓧) (Measure.map f μ) (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
  (Measure.bind (mα := m𝓧) (Measure.map f μ) (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
Tactic: rw [Measure.compProd_id_eq_copy_comp, ← Measure.comp_assoc,
      Measure.deterministic_comp_eq_map]
-- 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
⊢ Measure.map f μ ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) = Measure.map f μ ⊗ₘ Kernel.id
have calc : Measure.map f μ ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) =
  ((⇑(Kernel.deterministic f hf) : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ
    (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ)
Tactic: calc μ.map f ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ)
  _ = (Kernel.deterministic f hf ∘ₘ μ)
      ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) := by
    rw [Measure.deterministic_comp_eq_map]
  _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ) ∘ₘ
      Kernel.copy 𝓧 ∘ₘ Kernel.deterministic f hf ∘ₘ μ := by
    rw [Measure.compProd_eq_parallelComp_comp_copy_comp,
      ← Kernel.parallelComp_id_left_comp_parallelComp, ← Measure.comp_assoc]
  _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (Kernel.deterministic f hf ∥ₖ Kernel.id) ∘ₘ
      Kernel.copy Ω ∘ₘ μ := by rw [parallelProd_posterior_comp_copy_comp]
  _ = (Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) ∘ₘ Kernel.copy Ω ∘ₘ μ := by
    rw [Measure.comp_assoc, Kernel.parallelComp_comp_parallelComp, Kernel.id_comp, Kernel.comp_id]
  _ = (Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) ∘ₘ μ := by -- `deterministic` is used here
    rw [Measure.comp_assoc, Kernel.parallelComp_self_comp_copy]
  _ = μ.map f ⊗ₘ Kernel.id := by
    rw [Measure.compProd_id_eq_copy_comp, ← Measure.comp_assoc,
      Measure.deterministic_comp_eq_map]