awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 η
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 (𝓨 × Ω)))
⊢ ((⇑(η ∘ₖ κ) : (a : Ω) → Measure 𝓨) ∘ₘ μ) ⊗ₘ (κ†μ ∘ₖ η†((⇑κ : (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]

Premises used: ProbabilityTheory.Kernel.parallelComp_comp_copy, MeasureTheory.Measure.compProd_eq_comp_prod, MeasureTheory.Measure.comp_assoc, ProbabilityTheory.Kernel.parallelComp_id_left_comp_parallelComp
-- 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 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 (𝓨 × Ω)))
⊢ 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:
rw [parallelProd_posterior_comp_copy_comp]

Premises used: ProbabilityTheory.parallelProd_posterior_comp_copy_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 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 (𝓨 × Ω)))
⊢ 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 (𝓨 × Ω)))

Tactic:
rw [parallelProd_posterior_comp_copy_comp]

Premises used: ProbabilityTheory.parallelProd_posterior_comp_copy_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 η
simp_rw :
  Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(Kernel.swap Ω 𝓨 ∘ₖ (Kernel.id ∥ₖ η ∘ₖ (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.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.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 η
rw : (⇑(Kernel.swap Ω 𝓨 ∘ₖ (Kernel.id ∥ₖ η) ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ
| (⇑(Kernel.swap Ω 𝓨 ∘ₖ (Kernel.id ∥ₖ η ∘ₖ (Kernel.id ∥ₖ κ ∘ₖ Kernel.copy Ω))) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ

Tactic:
rw [← Kernel.comp_assoc]

Premises used: ProbabilityTheory.Kernel.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 η
conv_rhs :
  Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(Kernel.swap Ω 𝓨 ∘ₖ (Kernel.id ∥ₖ η) ∘ₖ (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 (𝓨 × Ω)) ∘ₘ μ)

Tactic:
conv_rhs => rw [← Kernel.comp_assoc]

Premises used: ProbabilityTheory.Kernel.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 η
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 (𝓨 × Ω)) ∘ₘ μ)
rw₅ rw₆ :
  Eq (α := Measure (𝓨 × Ω)) ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) : (a : Ω) → Measure (𝓨 × Ω)) ∘ₘ μ)
    ((⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ 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 (𝓨 × Ω)) ∘ₘ μ)

Tactic:
rw [Kernel.swap_parallelComp, Kernel.comp_assoc, ← Kernel.comp_assoc (Kernel.swap Ω 𝓧),
      Kernel.swap_parallelComp, Kernel.comp_assoc, Kernel.swap_copy]

Premises used: ProbabilityTheory.Kernel.comp_assoc, ProbabilityTheory.Kernel.swap_copy, ProbabilityTheory.Kernel.swap, 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 Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (b : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ, (κ†μ : (a : 𝓧) → Measure Ω) b ≪ μ
this : μ ⊗ₘ κ ≪ μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)

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 Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (b : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ, (κ†μ : (a : 𝓧) → Measure Ω) b ≪ μ
this : μ ⊗ₘ κ ≪ μ ⊗ₘ Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)

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 Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (b : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ, (κ†μ : (a : 𝓧) → Measure Ω) b ≪ μ
suffices : μ ⊗ₘ κ ≪ μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)

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 Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (b : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ, (κ†μ : (a : 𝓧) → Measure Ω) b ≪ μ
this : ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ ≪ Measure.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) μ
rw :
  Measure.AbsolutelyContinuous (_m0 := Prod.instMeasurableSpace)
    (Measure.map Prod.swap (((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ))
    (Measure.map Prod.swap (Measure.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) μ))
⊢ μ ⊗ₘ κ ≪ μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)

Tactic:
rw [← swap_compProd_posterior, ← Measure.prod_swap, Measure.swap_comp]

Premises used: MeasureTheory.Measure.swap_comp, MeasureTheory.Measure.prod_swap, ProbabilityTheory.swap_compProd_posterior
-- 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 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (b : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ, (κ†μ : (a : 𝓧) → Measure Ω) b ≪ μ
this : ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ ≪ Measure.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) μ
⊢ Measure.AbsolutelyContinuous (_m0 := Prod.instMeasurableSpace)
    (Measure.map Prod.swap (((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ))
    (Measure.map Prod.swap (Measure.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) μ))

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 Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (b : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ, (κ†μ : (a : 𝓧) → Measure Ω) b ≪ μ
this : ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ ≪ Measure.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) μ
⊢ Measure.AbsolutelyContinuous (_m0 := Prod.instMeasurableSpace)
    (Measure.map Prod.swap (((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ))
    (Measure.map Prod.swap (Measure.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) μ))

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 Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (b : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ, (κ†μ : (a : 𝓧) → Measure Ω) b ≪ μ
suffices : ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ ≪ Measure.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) μ
⊢ μ ⊗ₘ κ ≪ μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)

Tactic:
suffices (κ ∘ₘ μ) ⊗ₘ κ†μ ≪ (κ ∘ₘ μ).prod μ by
    rw [← swap_compProd_posterior, ← Measure.prod_swap, Measure.swap_comp]
    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 Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (b : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ, (κ†μ : (a : 𝓧) → Measure Ω) b ≪ μ
rw : ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ ≪ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ Kernel.const 𝓧 μ
⊢ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ ≪ Measure.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) μ

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 Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (b : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ, (κ†μ : (a : 𝓧) → Measure Ω) b ≪ μ
⊢ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ ≪ ((⇑κ : (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 Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (b : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ, (κ†μ : (a : 𝓧) → Measure Ω) b ≪ μ
refine :
  ∀ᵐ (a : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
    Measure.AbsolutelyContinuous.{u_1} (α := Ω) (_m0 := mΩ) ((κ†μ : (a : 𝓧) → Measure Ω) a)
      (((Kernel.const 𝓧 μ : Kernel 𝓧 Ω) : (a : 𝓧) → Measure Ω) a)
⊢ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ ≪ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ 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 Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (b : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ, (κ†μ : (a : 𝓧) → Measure Ω) b ≪ μ
⊢ ∀ᵐ (a : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
    Measure.AbsolutelyContinuous.{u_1} (α := Ω) (_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 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
⊢ (∀ᵐ (b : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ, (κ†μ : (a : 𝓧) → Measure Ω) b ≪ μ) ↔
    ∀ᵐ (ω : Ω) ∂μ,
      Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
        ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)

Tactic:
⟨absolutelyContinuous_of_posterior, absolutelyContinuous_posterior⟩

Premises used: ProbabilityTheory.absolutelyContinuous_of_posterior, Iff.intro, ProbabilityTheory.absolutelyContinuous_posterior
-- 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 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
ν : Measure 𝓧
inst_5 : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, (κ : (a : Ω) → Measure 𝓧) ω ≪ ν
rw : ∀ᵐ (b : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ, (κ†μ : (a : 𝓧) → Measure Ω) b ≪ μ
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)

Tactic:
rw [← absolutelyContinuous_posterior_iff]

Premises used: ProbabilityTheory.absolutelyContinuous_posterior_iff
-- 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 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
ν : Measure 𝓧
inst_5 : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, (κ : (a : Ω) → Measure 𝓧) ω ≪ ν
⊢ ∀ᵐ (b : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ, (κ†μ : (a : 𝓧) → Measure Ω) b ≪ μ

Tactic:
absolutelyContinuous_posterior h_ac

Premises used: ProbabilityTheory.absolutelyContinuous_posterior
-- 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 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
ν : Measure 𝓧
inst_5 : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, (κ : (a : Ω) → Measure 𝓧) ω ≪ ν
⊢ ∀ᵐ (b : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ, (κ†μ : (a : 𝓧) → Measure Ω) b ≪ μ

Tactic:
exact absolutelyContinuous_posterior h_ac

Premises used: ProbabilityTheory.absolutelyContinuous_posterior
-- 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 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac :
  ∀ᵐ (ω : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
⊢ AEMeasurable (β := ℝ≥0∞) (_m := Prod.instMeasurableSpace) (fun (x : Ω × 𝓧) ↦ (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1)
    (Measure.restrict (μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) (s ×ˢ t))

Tactic:
fun_prop