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
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)†μ)
⊢ Measure.map f μ ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) = Measure.map f μ ⊗ₘ Kernel.id
have calc₁ : ((⇑(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 (𝓧 × 𝓧))
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]
-- 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 Ω
ν : Measure 𝓧
inst_4 : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, (κ : (a : Ω) → Measure 𝓧) ω ≪ ν
this : ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ ≪ ν.prod μ
⊢ ∀ᵐ (b : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ, (κ†μ : (a : 𝓧) → Measure Ω) b ≪ μ
have this₁ : ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ ≪ ν ⊗ₘ Kernel.const 𝓧 μ
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 Ω
ν : Measure 𝓧
inst_4 : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, (κ : (a : Ω) → Measure 𝓧) ω ≪ ν
⊢ ∀ᵐ (b : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ, (κ†μ : (a : 𝓧) → Measure Ω) b ≪ μ
have suffices : ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ ≪ ν.prod μ
Tactic: suffices (κ ∘ₘ μ) ⊗ₘ (κ†μ) ≪ ν.prod μ by
    rw [← Measure.compProd_const] at this
    simpa using this.kernel_of_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 Ω
ν : Measure 𝓧
inst_4 : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, (κ : (a : Ω) → Measure 𝓧) ω ≪ ν
this : μ ⊗ₘ κ ≪ μ.prod ν
⊢ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ ≪ ν.prod μ
have rw : Measure.AbsolutelyContinuous (_m0 := Prod.instMeasurableSpace) (Measure.map Prod.swap (μ ⊗ₘ κ))
  (Measure.map Prod.swap (μ.prod ν))
Tactic: rw [compProd_posterior_eq_map_swap, ← Measure.prod_swap]
-- 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 𝓧
inst_4 : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, (κ : (a : Ω) → Measure 𝓧) ω ≪ ν
⊢ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ ≪ ν.prod μ
have suffices : μ ⊗ₘ κ ≪ μ.prod ν
Tactic: suffices μ ⊗ₘ κ ≪ μ.prod ν by
    rw [compProd_posterior_eq_map_swap, ← Measure.prod_swap]
    exact this.map measurable_swap
-- 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 𝓧
inst_4 : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, (κ : (a : Ω) → Measure 𝓧) ω ≪ ν
⊢ μ ⊗ₘ κ ≪ μ.prod ν
have rw : μ ⊗ₘ κ ≪ μ ⊗ₘ Kernel.const Ω ν
Tactic: rw [← Measure.compProd_const]
-- 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 𝓧
inst_4 : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, (κ : (a : Ω) → Measure 𝓧) ω ≪ ν
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ Kernel.const Ω ν
have refine : ∀ᵐ (a : Ω) ∂μ,
  Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) a)
    (((Kernel.const Ω ν : Kernel Ω 𝓧) : (a : Ω) → Measure 𝓧) a)
Tactic: refine Measure.AbsolutelyContinuous.compProd_right ?_
-- 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 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
inst_6 : IsMarkovKernel κ
this :
  Filter.EventuallyEq.{u_1, u_2} (β := Measure 𝓧)
    (ae (F := Measure Ω)
      (Measure.bind.{u_2, u_1} (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ) : (a : 𝓧) → Measure Ω)))
    (⇑κ : (a : Ω) → Measure 𝓧) (⇑((κ†μ)†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) : (a : Ω) → Measure 𝓧)
⊢ Filter.EventuallyEq.{u_1, u_2} (β := Measure 𝓧) (ae μ)
    (⇑((κ†μ)†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) : (a : Ω) → Measure 𝓧) (⇑κ : (a : Ω) → Measure 𝓧)
have this₁ : Filter.EventuallyEq.{u_1, u_2} (β := Measure 𝓧) (ae μ) (⇑κ : (a : Ω) → Measure 𝓧)
  (⇑((κ†μ)†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) : (a : Ω) → Measure 𝓧)
Tactic: rw [posterior_comp_self] 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 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
inst_6 : IsMarkovKernel κ
this :
  Filter.EventuallyEq.{u_1, u_2} (β := Measure 𝓧) (ae μ) (⇑κ : (a : Ω) → Measure 𝓧)
    (⇑((κ†μ)†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) : (a : Ω) → Measure 𝓧)
⊢ Filter.EventuallyEq.{u_1, u_2} (β := Measure 𝓧) (ae μ)
    (⇑((κ†μ)†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) : (a : Ω) → Measure 𝓧) (⇑κ : (a : Ω) → Measure 𝓧)
have h : ∀ (a : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω)
          {x : Ω |
            (fun (x : Ω) ↦
                Eq.{u_2 + 1} (α := Measure 𝓧) ((κ : (a : Ω) → Measure 𝓧) x : Measure 𝓧)
                  (((κ†μ)†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) : (a : Ω) → Measure 𝓧) x : Measure 𝓧))
              x}
          x →
        Membership.mem (γ := Set Ω)
          {x : Ω |
            (fun (x : Ω) ↦
                Eq.{u_2 + 1} (α := Measure 𝓧)
                  (((κ†μ)†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) : (a : Ω) → Measure 𝓧) x : Measure 𝓧)
                  ((κ : (a : Ω) → Measure 𝓧) x : Measure 𝓧))
              x}
          x}
    a
Tactic: filter_upwards [this] with a h using h.symm
-- 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 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
inst_6 : IsMarkovKernel κ
this :
  Filter.EventuallyEq.{u_1, u_2} (β := Measure 𝓧) (ae μ) (⇑κ : (a : Ω) → Measure 𝓧)
    (⇑((κ†μ)†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) : (a : Ω) → Measure 𝓧)
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (x : Ω) ↦
                  Eq.{u_2 + 1} (α := Measure 𝓧) ((κ : (a : Ω) → Measure 𝓧) x : Measure 𝓧)
                    (((κ†μ)†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) : (a : Ω) → Measure 𝓧) x : Measure 𝓧))
                x}
            x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (x : Ω) ↦
                  Eq.{u_2 + 1} (α := Measure 𝓧)
                    (((κ†μ)†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) : (a : Ω) → Measure 𝓧) x : Measure 𝓧)
                    ((κ : (a : Ω) → Measure 𝓧) x : Measure 𝓧))
                x}
            x}
      a
⊢ Filter.EventuallyEq.{u_1, u_2} (β := Measure 𝓧) (ae μ)
    (⇑((κ†μ)†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) : (a : Ω) → Measure 𝓧) (⇑κ : (a : Ω) → Measure 𝓧)
have h₁ : ∀ (a : Ω),
  Eq.{u_2 + 1} (α := Measure 𝓧) ((κ : (a : Ω) → Measure 𝓧) a : Measure 𝓧)
      (((κ†μ)†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) : (a : Ω) → Measure 𝓧) a : Measure 𝓧) →
    Eq.{u_2 + 1} (α := Measure 𝓧) (((κ†μ)†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) : (a : Ω) → Measure 𝓧) a : Measure 𝓧)
      ((κ : (a : Ω) → Measure 𝓧) a : Measure 𝓧)
Tactic: filter_upwards [this] with a h using h.symm
-- 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 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
inst_6 : IsMarkovKernel κ
⊢ Filter.EventuallyEq.{u_1, u_2} (β := Measure 𝓧) (ae μ)
    (⇑((κ†μ)†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) : (a : Ω) → Measure 𝓧) (⇑κ : (a : Ω) → Measure 𝓧)
have suffices : Filter.EventuallyEq.{u_1, u_2} (β := Measure 𝓧)
  (ae (F := Measure Ω)
    (Measure.bind.{u_2, u_1} (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ) : (a : 𝓧) → Measure Ω)))
  (⇑κ : (a : Ω) → Measure 𝓧) (⇑((κ†μ)†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) : (a : Ω) → Measure 𝓧)
Tactic: suffices κ =ᵐ[κ†μ ∘ₘ κ ∘ₘ μ] (κ†μ)†(κ ∘ₘ μ) by
    rw [posterior_comp_self] at this
    filter_upwards [this] with a h using h.symm
-- 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 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
inst_6 : IsMarkovKernel κ
⊢ Filter.EventuallyEq.{u_1, u_2} (β := Measure 𝓧)
    (ae (F := Measure Ω)
      (Measure.bind.{u_2, u_1} (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ) : (a : 𝓧) → Measure Ω)))
    (⇑κ : (a : Ω) → Measure 𝓧) (⇑((κ†μ)†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) : (a : Ω) → Measure 𝓧)
have refine : Measure.bind.{u_2, u_1} (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ) : (a : 𝓧) → Measure Ω) ⊗ₘ κ =
  (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) ∘ₘ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ
Tactic: refine ae_eq_posterior_of_compProd_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 Ω
inst_4 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
inst_6 : IsMarkovKernel κ
⊢ Measure.bind.{u_2, u_1} (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ) : (a : 𝓧) → Measure Ω) ⊗ₘ κ =
    (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) ∘ₘ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ
have rw : μ ⊗ₘ κ = (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) ∘ₘ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ
Tactic: rw [posterior_comp_self, 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 Ω
inst_4 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
inst_6 : IsMarkovKernel κ
rw : μ ⊗ₘ κ = (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) ∘ₘ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ
⊢ Measure.bind.{u_2, u_1} (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ) : (a : 𝓧) → Measure Ω) ⊗ₘ κ =
    (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) ∘ₘ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ
have rw₁ : μ ⊗ₘ κ =
  Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
    ((⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ)
    (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧))
Tactic: rw [posterior_comp_self, 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 Ω
inst_4 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
inst_6 : IsMarkovKernel κ
rw : μ ⊗ₘ κ = (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) ∘ₘ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ
rw₁ :
  μ ⊗ₘ κ =
    Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ)
      (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧))
⊢ Measure.bind.{u_2, u_1} (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ) : (a : 𝓧) → Measure Ω) ⊗ₘ κ =
    (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) ∘ₘ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ
have rw₂ : μ ⊗ₘ κ = (⇑(Kernel.swap 𝓧 Ω ∘ₖ Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (Ω × 𝓧)) ∘ₘ μ ⊗ₘ κ
Tactic: rw [posterior_comp_self, 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 Ω
inst_4 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
inst_6 : IsMarkovKernel κ
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.{u_2, u_1} (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ) : (a : 𝓧) → Measure Ω) ⊗ₘ κ =
    (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) ∘ₘ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ
have rw₃ : μ ⊗ₘ κ = (⇑Kernel.id : (a : Ω × 𝓧) → Measure (Ω × 𝓧)) ∘ₘ μ ⊗ₘ κ
Tactic: rw [posterior_comp_self, 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 Ω
inst_4 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
inst_6 : IsMarkovKernel κ
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.{u_2, u_1} (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ) : (a : 𝓧) → Measure Ω) ⊗ₘ κ =
    (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) ∘ₘ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ
have rw₄ : μ ⊗ₘ κ = μ ⊗ₘ κ
Tactic: rw [posterior_comp_self, 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
𝓨 : 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 η
⊢ Filter.EventuallyEq.{u_3, u_1} (β := Measure Ω)
    (ae (F := Measure 𝓨)
      (Measure.bind.{u_2, u_3} (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑η : (a : 𝓧) → Measure 𝓨)))
    (⇑((η ∘ₖ κ)†μ) : (a : 𝓨) → Measure Ω) (⇑(κ†μ ∘ₖ η†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) : (a : 𝓨) → Measure Ω)
have rw : Filter.EventuallyEq.{u_3, u_1} (β := Measure Ω) (ae (F := Measure 𝓨) ((⇑(η ∘ₖ κ) : (a : Ω) → Measure 𝓨) ∘ₘ μ))
  (⇑((η ∘ₖ κ)†μ) : (a : 𝓨) → Measure Ω) (⇑(κ†μ ∘ₖ η†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) : (a : 𝓨) → Measure Ω)
Tactic: 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 η
⊢ Filter.EventuallyEq.{u_3, u_1} (β := Measure Ω) (ae (F := Measure 𝓨) ((⇑(η ∘ₖ κ) : (a : Ω) → Measure 𝓨) ∘ₘ μ))
    (⇑((η ∘ₖ κ)†μ) : (a : 𝓨) → Measure Ω) (⇑(κ†μ ∘ₖ η†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) : (a : 𝓨) → Measure Ω)
have refine : ((⇑(η ∘ₖ κ) : (a : Ω) → Measure 𝓨) ∘ₘ μ) ⊗ₘ (κ†μ ∘ₖ η†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) =
  (⇑(Kernel.swap Ω 𝓨) : (a : Ω × 𝓨) → Measure (𝓨 × Ω)) ∘ₘ μ ⊗ₘ (η ∘ₖ κ)
Tactic: refine (ae_eq_posterior_of_compProd_eq_swap_comp ((κ†μ) ∘ₖ η†(κ ∘ₘ μ)) ?_).symm
-- 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 η
⊢ ((⇑(η ∘ₖ κ) : (a : Ω) → Measure 𝓨) ∘ₘ μ) ⊗ₘ (κ†μ ∘ₖ η†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) =
    (⇑(Kernel.swap Ω 𝓨) : (a : Ω × 𝓨) → Measure (𝓨 × Ω)) ∘ₘ μ ⊗ₘ (η ∘ₖ κ)
have simp_rw : 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 (𝓨 × Ω)))
Tactic: simp_rw [Measure.compProd_eq_comp_prod, ← Kernel.parallelComp_comp_copy,
    ← 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
𝓨 : 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α := 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α := 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 (𝓨 × Ω)))
Tactic: rw [parallelProd_posterior_comp_copy_comp]