awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Posterior
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 rw₁ :
  Eq (α := Measure (𝓧 × Ω)) ((⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ)
    ((⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ)
⊢ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ = (⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ

Tactic:
rw [compProd_posterior_eq_swap_comp]

Premises used: ProbabilityTheory.compProd_posterior_eq_swap_comp
-- Module: Mathlib.Probability.Kernel.Posterior
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 rw₁ :
  Eq (α := Measure (𝓧 × Ω))
    (Measure.bind (α := Ω × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
        (⇑(Kernel.id ∥ₖ κ) : (a : Ω × Ω) → Measure (Ω × 𝓧)))
      (⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)))
    (Measure.bind (α := Ω × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
        (⇑(Kernel.id ∥ₖ κ) : (a : Ω × Ω) → Measure (Ω × 𝓧)))
      (⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)))
⊢ Eq (α := Measure (𝓧 × Ω)) ((⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ)
    (Measure.bind (α := Ω × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
        (⇑(Kernel.id ∥ₖ κ) : (a : Ω × Ω) → Measure (Ω × 𝓧)))
      (⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)))

Tactic:
rw [Measure.compProd_eq_parallelComp_comp_copy_comp]

Premises used: MeasureTheory.Measure.compProd_eq_parallelComp_comp_copy_comp
-- Module: Mathlib.Probability.Kernel.Posterior
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
rw :
  Eq (α := Measure (𝓧 × Ω))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(Kernel.swap Ω 𝓧 ∘ₖ (Kernel.id ∥ₖ κ)) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
rw₁ :
  Eq (α := Measure (𝓧 × Ω))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap Ω Ω) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
rw₂ :
  Eq (α := Measure (𝓧 × Ω)) ((⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap Ω Ω ∘ₖ Kernel.copy Ω) : (a : Ω) → Measure (𝓧 × Ω)) ∘ₘ μ)
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
rw₃ :
  Eq (α := Measure (𝓧 × Ω)) ((⇑(κ ∥ₖ Kernel.id ∘ₖ (Kernel.swap Ω Ω ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓧 × Ω)) ∘ₘ μ)
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
rw₄ :
  Eq (α := Measure (𝓧 × Ω)) ((⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω) : (a : Ω) → Measure (𝓧 × Ω)) ∘ₘ μ)
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))
rw₅ rw₆ :
  Eq (α := Measure (𝓧 × Ω)) ((⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω) : (a : Ω) → Measure (𝓧 × Ω)) ∘ₘ μ)
    ((⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω) : (a : Ω) → Measure (𝓧 × Ω)) ∘ₘ μ)
⊢ Eq (α := Measure (𝓧 × Ω))
    (Measure.bind (α := Ω × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
        (⇑(Kernel.id ∥ₖ κ) : (a : Ω × Ω) → Measure (Ω × 𝓧)))
      (⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)))
    (Measure.bind (α := Ω × Ω) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : Ω × Ω) → Measure (𝓧 × Ω)))

Tactic:
rw [Measure.comp_assoc, Kernel.swap_parallelComp, Measure.comp_assoc, Kernel.comp_assoc,
      Kernel.swap_copy, Measure.comp_assoc]

Premises used: ProbabilityTheory.Kernel.comp_assoc, ProbabilityTheory.Kernel.swap_copy, MeasureTheory.Measure.comp_assoc, ProbabilityTheory.Kernel.swap_parallelComp
-- Module: Mathlib.Probability.Kernel.Posterior
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 (𝓧 × Ω)))
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 (𝓧 × Ω)))
⊢ 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 (𝓧 × Ω)))

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]

Premises used: MeasureTheory.Measure.bind, ProbabilityTheory.Kernel.id, ProbabilityTheory.posterior, ProbabilityTheory.Kernel.swap, ProbabilityTheory.Kernel.parallelComp, MeasureTheory.Measure.compProd, DFunLike.coe, ProbabilityTheory.Kernel.copy
-- Module: Mathlib.Probability.Kernel.Posterior
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 (Ω × 𝓧)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ κ
rw₆ rw₇ : μ ⊗ₘ κ = μ ⊗ₘ κ
⊢ Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ ×ₖ 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]

Premises used: ProbabilityTheory.Kernel.swap_swap, ProbabilityTheory.Kernel.swap_prod, MeasureTheory.Measure.compProd_eq_comp_prod, MeasureTheory.Measure.comp_assoc, MeasureTheory.Measure.id_comp, ProbabilityTheory.compProd_posterior_eq_swap_comp
-- Module: Mathlib.Probability.Kernel.Posterior
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 𝓧) ∘ₘ μ) ⊗ₘ η = Measure.map Prod.swap (μ ⊗ₘ κ)
⊢ Filter.EventuallyEq.{u_2, u_1} (β := Measure Ω) (ae (F := Measure 𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ))
    (⇑η : (a : 𝓧) → Measure Ω) (⇑(κ†μ) : (a : 𝓧) → Measure Ω)

Tactic:
(Kernel.ae_eq_of_compProd_eq (compProd_posterior_eq_map_swap.trans h.symm)).symm

Premises used: ProbabilityTheory.compProd_posterior_eq_map_swap, ProbabilityTheory.Kernel.ae_eq_of_compProd_eq, Eq.symm, Filter.EventuallyEq.symm, Eq.trans
-- Module: Mathlib.Probability.Kernel.Posterior
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 (μ ⊗ₘ κ))
rw₁ rw₂ : Eq (α := Measure (𝓧 × Ω)) (Measure.map Prod.swap (μ ⊗ₘ κ)) (Measure.map Prod.swap (μ ⊗ₘ κ))
⊢ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ η = Measure.map Prod.swap (μ ⊗ₘ κ)

Tactic:
rw [h, Measure.swap_comp]

Premises used: MeasureTheory.Measure.swap_comp
-- Module: Mathlib.Probability.Kernel.Posterior
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 = μ
rw₃ rw₄ : μ = μ
⊢ Measure.bind.{u_2, u_1} (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ) : (a : 𝓧) → Measure Ω) = μ

Tactic:
rw [← Measure.snd_compProd, compProd_posterior_eq_map_swap, Measure.snd_map_swap,
    Measure.fst_compProd]

Premises used: ProbabilityTheory.compProd_posterior_eq_map_swap, MeasureTheory.Measure.snd_map_swap, MeasureTheory.Measure.fst_compProd, MeasureTheory.Measure.snd_compProd
-- Module: Mathlib.Probability.Kernel.Posterior
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 Ω)

Tactic:
rw [Measure.id_comp] at this

Premises used: MeasureTheory.Measure.id_comp
-- Module: Mathlib.Probability.Kernel.Posterior
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 Ω)
a : Ω
ha :
  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:
ha.symm

Premises used: Eq.symm
-- Module: Mathlib.Probability.Kernel.Posterior
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
h₁ h₂ :
  ∀ (a : Ω)
    (ha :
      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 Ω)
⊢ (ae μ).EventuallyEq (β := Measure Ω) (⇑(Kernel.id†μ) : (a : Ω) → Measure Ω) (⇑Kernel.id : (a : Ω) → Measure Ω)

Tactic:
filter_upwards [this] with a ha using ha.symm
-- Module: Mathlib.Probability.Kernel.Posterior
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
suffices :
  (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 Ω)

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
-- Module: Mathlib.Probability.Kernel.Posterior
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 Ω)

Tactic:
ae_eq_posterior_of_compProd_eq_swap_comp Kernel.id ?_

Premises used: ProbabilityTheory.ae_eq_posterior_of_compProd_eq_swap_comp, ProbabilityTheory.Kernel.id
-- Module: Mathlib.Probability.Kernel.Posterior
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
refine :
  Eq (α := Measure (Ω × Ω)) (((⇑Kernel.id : (a : Ω) → Measure Ω) ∘ₘ μ) ⊗ₘ Kernel.id)
    ((⇑(Kernel.swap Ω Ω) : (a : Ω × Ω) → Measure (Ω × Ω)) ∘ₘ μ ⊗ₘ Kernel.id)
⊢ (ae (F := Measure Ω) ((⇑Kernel.id : (a : Ω) → Measure Ω) ∘ₘ μ)).EventuallyEq (β := Measure Ω)
    (⇑Kernel.id : (a : Ω) → Measure Ω) (⇑(Kernel.id†μ) : (a : Ω) → Measure Ω)

Tactic:
refine ae_eq_posterior_of_compProd_eq_swap_comp Kernel.id ?_

Premises used: ProbabilityTheory.ae_eq_posterior_of_compProd_eq_swap_comp, ProbabilityTheory.Kernel.id
-- Module: Mathlib.Probability.Kernel.Posterior
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 (Ω × Ω)) ∘ₘ μ)
rw₃ rw₄ :
  Eq (α := Measure (Ω × Ω)) ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
    ((⇑(Kernel.copy Ω) : (a : Ω) → Measure (Ω × Ω)) ∘ₘ μ)
⊢ Eq (α := Measure (Ω × Ω)) (((⇑Kernel.id : (a : Ω) → Measure Ω) ∘ₘ μ) ⊗ₘ 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]

Premises used: MeasureTheory.Measure.compProd_id_eq_copy_comp, ProbabilityTheory.Kernel.swap_copy, MeasureTheory.Measure.comp_assoc, MeasureTheory.Measure.id_comp
-- Module: Mathlib.Probability.Kernel.Posterior
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 𝓧)

Tactic:
Kernel.ae_eq_of_compProd_eq ?_

Premises used: ProbabilityTheory.Kernel.ae_eq_of_compProd_eq
-- Module: Mathlib.Probability.Kernel.Posterior
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
refine : Measure.map f μ ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) = Measure.map f μ ⊗ₘ Kernel.id
⊢ (ae (F := Measure 𝓧) (Measure.map f μ)).EventuallyEq (β := Measure 𝓧)
    (⇑(Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) : (a : 𝓧) → Measure 𝓧)
    (⇑Kernel.id : (a : 𝓧) → Measure 𝓧)

Tactic:
refine Kernel.ae_eq_of_compProd_eq ?_

Premises used: ProbabilityTheory.Kernel.ae_eq_of_compProd_eq
-- Module: Mathlib.Probability.Kernel.Posterior
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 rw₁ :
  Measure.map f μ ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) =
    Measure.map f μ ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ)
⊢ 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:
rw [Measure.deterministic_comp_eq_map]

Premises used: MeasureTheory.Measure.deterministic_comp_eq_map
-- Module: Mathlib.Probability.Kernel.Posterior
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 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 (𝓧 × 𝓧)))
⊢ 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 (𝓧 × 𝓧)))

Tactic:
rw [parallelProd_posterior_comp_copy_comp]

Premises used: ProbabilityTheory.parallelProd_posterior_comp_copy_comp