awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  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 (𝓧 × 𝓧)))
rw₃ 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 (𝓧 × 𝓧)))
⊢ 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 (𝓧 × 𝓧)))

Tactic:
rw [Measure.comp_assoc, Kernel.parallelComp_comp_parallelComp, Kernel.id_comp, Kernel.comp_id]

Premises used: ProbabilityTheory.Kernel.parallelComp_comp_parallelComp, MeasureTheory.Measure.comp_assoc, ProbabilityTheory.Kernel.id_comp, ProbabilityTheory.Kernel.comp_id
-- 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 :
  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 (𝓧 × 𝓧)) ∘ₘ μ)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := Measure (𝓧 × 𝓧)) ((⇑(Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) : (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 (𝓧 × 𝓧)) ∘ₘ μ)

Tactic:
rw [Measure.comp_assoc, Kernel.parallelComp_self_comp_copy]

Premises used: MeasureTheory.Measure.comp_assoc, ProbabilityTheory.Kernel.parallelComp_self_comp_copy
-- 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 :
  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 (𝓧 × 𝓧)))
rw₂ 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 (𝓧 × 𝓧)))
⊢ Eq (α := Measure (𝓧 × 𝓧)) ((⇑(Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) : (a : Ω) → Measure (𝓧 × 𝓧)) ∘ₘ μ)
    (Measure.map f μ ⊗ₘ Kernel.id)

Tactic:
rw [Measure.compProd_id_eq_copy_comp, ← Measure.comp_assoc,
      Measure.deterministic_comp_eq_map]

Premises used: MeasureTheory.Measure.compProd_id_eq_copy_comp, MeasureTheory.Measure.deterministic_comp_eq_map, MeasureTheory.Measure.comp_assoc
-- 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 Ω
ν : Measure 𝓧
inst_4 : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, (κ : (a : Ω) → Measure 𝓧) ω ≪ ν
this : ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ ≪ ν.prod μ
⊢ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ ≪ ν ⊗ₘ Kernel.const 𝓧 μ

Tactic:
rw [← Measure.compProd_const] at this

Premises used: MeasureTheory.Measure.compProd_const
-- 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 Ω
ν : Measure 𝓧
inst_4 : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, (κ : (a : Ω) → Measure 𝓧) ω ≪ ν
this : ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ ≪ ν ⊗ₘ Kernel.const 𝓧 μ
⊢ ∀ᵐ (b : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ, (κ†μ : (a : 𝓧) → Measure Ω) b ≪ μ

Tactic:
simpa using this.kernel_of_compProd

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.kernel_of_compProd
-- 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 Ω
ν : Measure 𝓧
inst_4 : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, (κ : (a : Ω) → Measure 𝓧) ω ≪ ν
suffices : ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ ≪ ν.prod μ
⊢ ∀ᵐ (b : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ, (κ†μ : (a : 𝓧) → Measure Ω) b ≪ μ

Tactic:
suffices (κ ∘ₘ μ) ⊗ₘ (κ†μ) ≪ ν.prod μ by
    rw [← Measure.compProd_const] at this
    simpa using this.kernel_of_compProd
-- 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 Ω
ν : Measure 𝓧
inst_4 : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, (κ : (a : Ω) → Measure 𝓧) ω ≪ ν
this : μ ⊗ₘ κ ≪ μ.prod ν
rw :
  Measure.AbsolutelyContinuous (_m0 := Prod.instMeasurableSpace) (Measure.map Prod.swap (μ ⊗ₘ κ))
    (Measure.map Prod.swap (μ.prod ν))
⊢ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ ≪ ν.prod μ

Tactic:
rw [compProd_posterior_eq_map_swap, ← Measure.prod_swap]

Premises used: ProbabilityTheory.compProd_posterior_eq_map_swap, MeasureTheory.Measure.prod_swap
-- 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 Ω
ν : Measure 𝓧
inst_4 : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, (κ : (a : Ω) → Measure 𝓧) ω ≪ ν
this : μ ⊗ₘ κ ≪ μ.prod ν
⊢ Measure.AbsolutelyContinuous (_m0 := Prod.instMeasurableSpace) (Measure.map Prod.swap (μ ⊗ₘ κ))
    (Measure.map Prod.swap (μ.prod ν))

Tactic:
this.map measurable_swap

Premises used: measurable_swap, MeasureTheory.Measure.AbsolutelyContinuous.map
-- 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 Ω
ν : Measure 𝓧
inst_4 : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, (κ : (a : Ω) → Measure 𝓧) ω ≪ ν
this : μ ⊗ₘ κ ≪ μ.prod ν
⊢ Measure.AbsolutelyContinuous (_m0 := Prod.instMeasurableSpace) (Measure.map Prod.swap (μ ⊗ₘ κ))
    (Measure.map Prod.swap (μ.prod ν))

Tactic:
exact this.map measurable_swap

Premises used: measurable_swap, MeasureTheory.Measure.AbsolutelyContinuous.map
-- 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 Ω
ν : Measure 𝓧
inst_4 : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, (κ : (a : Ω) → Measure 𝓧) ω ≪ ν
suffices : μ ⊗ₘ κ ≪ μ.prod ν
⊢ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ ≪ ν.prod μ

Tactic:
suffices μ ⊗ₘ κ ≪ μ.prod ν by
    rw [compProd_posterior_eq_map_swap, ← Measure.prod_swap]
    exact this.map measurable_swap
-- 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 Ω
ν : Measure 𝓧
inst_4 : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, (κ : (a : Ω) → Measure 𝓧) ω ≪ ν
rw : μ ⊗ₘ κ ≪ μ ⊗ₘ Kernel.const Ω ν
⊢ μ ⊗ₘ κ ≪ μ.prod ν

Tactic:
rw [← Measure.compProd_const]

Premises used: MeasureTheory.Measure.compProd_const
-- 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 Ω
ν : Measure 𝓧
inst_4 : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, (κ : (a : Ω) → Measure 𝓧) ω ≪ ν
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ Kernel.const Ω ν

Tactic:
Measure.AbsolutelyContinuous.compProd_right ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.compProd_right
-- 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 Ω
ν : Measure 𝓧
inst_4 : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, (κ : (a : Ω) → Measure 𝓧) ω ≪ ν
refine :
  ∀ᵐ (a : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) a)
      (((Kernel.const Ω ν : Kernel Ω 𝓧) : (a : Ω) → Measure 𝓧) a)
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ Kernel.const Ω ν

Tactic:
refine Measure.AbsolutelyContinuous.compProd_right ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.compProd_right
-- 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 Ω
ν : Measure 𝓧
inst_4 : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, (κ : (a : Ω) → Measure 𝓧) ω ≪ ν
⊢ ∀ᵐ (a : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) a)
      (((Kernel.const Ω ν : Kernel Ω 𝓧) : (a : Ω) → Measure 𝓧) a)

Tactic:
simpa
-- 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 : 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 𝓧)

Tactic:
rw [posterior_comp_self] at this

Premises used: ProbabilityTheory.posterior_comp_self
-- 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 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
inst_6 : IsMarkovKernel κ
this :
  Filter.EventuallyEq.{u_1, u_2} (β := Measure 𝓧) (ae μ) (⇑κ : (a : Ω) → Measure 𝓧)
    (⇑((κ†μ)†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) : (a : Ω) → Measure 𝓧)
a : Ω
h :
  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:
h.symm

Premises used: Eq.symm
-- 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 : 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
h₁ h₂ :
  ∀ (a : Ω)
    (h :
      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 𝓧)
⊢ Filter.EventuallyEq.{u_1, u_2} (β := Measure 𝓧) (ae μ)
    (⇑((κ†μ)†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) : (a : Ω) → Measure 𝓧) (⇑κ : (a : Ω) → Measure 𝓧)

Tactic:
filter_upwards [this] with a h using h.symm
-- 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 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
inst_6 : IsMarkovKernel κ
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 𝓧)
⊢ Filter.EventuallyEq.{u_1, u_2} (β := Measure 𝓧) (ae μ)
    (⇑((κ†μ)†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) : (a : Ω) → Measure 𝓧) (⇑κ : (a : Ω) → Measure 𝓧)

Tactic:
suffices κ =ᵐ[κ†μ ∘ₘ κ ∘ₘ μ] (κ†μ)†(κ ∘ₘ μ) by
    rw [posterior_comp_self] at this
    filter_upwards [this] with a h using h.symm
-- 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 : 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 𝓧)

Tactic:
ae_eq_posterior_of_compProd_eq_swap_comp κ ?_

Premises used: ProbabilityTheory.ae_eq_posterior_of_compProd_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 Ω
inst_4 : StandardBorelSpace 𝓧
inst_5 : Nonempty 𝓧
inst_6 : IsMarkovKernel κ
refine :
  Measure.bind.{u_2, u_1} (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ) : (a : 𝓧) → Measure Ω) ⊗ₘ κ =
    (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) ∘ₘ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ
⊢ 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:
refine ae_eq_posterior_of_compProd_eq_swap_comp κ ?_

Premises used: ProbabilityTheory.ae_eq_posterior_of_compProd_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 Ω
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 (Ω × 𝓧)) ∘ₘ μ ⊗ₘ κ
rw₄ rw₅ : μ ⊗ₘ κ = μ ⊗ₘ κ
⊢ Measure.bind.{u_2, u_1} (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) (⇑(κ†μ) : (a : 𝓧) → Measure Ω) ⊗ₘ κ =
    (⇑(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]

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

Tactic:
rw [Measure.comp_assoc]

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

Tactic:
(ae_eq_posterior_of_compProd_eq_swap_comp ((κ†μ) ∘ₖ η†(κ ∘ₘ μ)) ?_).symm

Premises used: ProbabilityTheory.Kernel.comp, ProbabilityTheory.ae_eq_posterior_of_compProd_eq_swap_comp, MeasureTheory.Measure.bind, ProbabilityTheory.posterior, DFunLike.coe, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Kernel.Posterior
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 η
refine :
  ((⇑(η ∘ₖ κ) : (a : Ω) → Measure 𝓨) ∘ₘ μ) ⊗ₘ (κ†μ ∘ₖ η†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) =
    (⇑(Kernel.swap Ω 𝓨) : (a : Ω × 𝓨) → Measure (𝓨 × Ω)) ∘ₘ μ ⊗ₘ (η ∘ₖ κ)
⊢ Filter.EventuallyEq.{u_3, u_1} (β := Measure Ω) (ae (F := Measure 𝓨) ((⇑(η ∘ₖ κ) : (a : Ω) → Measure 𝓨) ∘ₘ μ))
    (⇑((η ∘ₖ κ)†μ) : (a : 𝓨) → Measure Ω) (⇑(κ†μ ∘ₖ η†((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) : (a : 𝓨) → Measure Ω)

Tactic:
refine (ae_eq_posterior_of_compProd_eq_swap_comp ((κ†μ) ∘ₖ η†(κ ∘ₘ μ)) ?_).symm

Premises used: ProbabilityTheory.Kernel.comp, ProbabilityTheory.ae_eq_posterior_of_compProd_eq_swap_comp, MeasureTheory.Measure.bind, ProbabilityTheory.posterior, DFunLike.coe, Filter.EventuallyEq.symm