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 Ω
inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac :
  ∀ᵐ (ω : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
h1 :
  ∀ {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t),
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
      (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t)
h2 :
  ∀ {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t),
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t,
        κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x.1 x.2 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
      (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t)
refine_1 : ∫⁻ (x : Ω × 𝓧), (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) < ∞
⊢ ∫⁻ (x : Ω × 𝓧), (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ≠ ∞

Tactic:
refine ne_of_lt ?_

Premises used: ne_of_lt
-- 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 𝓧) ∘ₘ μ)
h1 :
  ∀ {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t),
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
      (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t)
h2 :
  ∀ {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t),
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t,
        κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x.1 x.2 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
      (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t)
rw :
  ∫⁻ (x : Ω × 𝓧) in Set.univ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
    (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) Set.univ
rw₁ :
  ∫⁻ (x : Ω × 𝓧) in SProd.sprod (α := Set Ω) (β := Set 𝓧) Set.univ Set.univ,
      (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
    (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (SProd.sprod (α := Set Ω) (β := Set 𝓧) Set.univ Set.univ)
rw₂ rw₃ :
  Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (SProd.sprod (α := Set Ω) (β := Set 𝓧) Set.univ Set.univ) : ℝ≥0∞)
    ((μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (SProd.sprod (α := Set Ω) (β := Set 𝓧) Set.univ Set.univ) : ℝ≥0∞)
⊢ ∫⁻ (x : Ω × 𝓧), (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
    (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) Set.univ

Tactic:
rw [← setLIntegral_univ, ← Set.univ_prod_univ, h1 .univ .univ]

Premises used: Set.univ_prod_univ, MeasurableSet.univ, MeasureTheory.setLIntegral_univ
-- 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 𝓧) ∘ₘ μ)
h1 :
  ∀ {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t),
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
      (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t)
h2 :
  ∀ {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t),
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t,
        κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x.1 x.2 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
      (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t)
⊢ LT.lt (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_lt_top _ _

Premises used: MeasureTheory.measure_lt_top
-- 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 𝓧) ∘ₘ μ)
h1 :
  ∀ {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t),
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
      (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t)
h2 :
  ∀ {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t),
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t,
        κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x.1 x.2 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
      (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t)
calc :
  ∫⁻ (x : Ω × 𝓧), (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
    (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) Set.univ
⊢ ∫⁻ (x : Ω × 𝓧), (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) < ∞

Tactic:
calc ∫⁻ x, (κ†μ).rnDeriv (Kernel.const _ μ) x.2 x.1 ∂μ.prod (κ ∘ₘ μ)
    _ = (μ ⊗ₘ κ) Set.univ := by rw [← setLIntegral_univ, ← Set.univ_prod_univ, h1 .univ .univ]
    _ < ⊤ := measure_lt_top _ _

Premises used: MeasureTheory.measure_lt_top, Set.univ, MeasureTheory.Measure.bind, MeasureTheory.Measure.prod, MeasureTheory.Measure.compProd, DFunLike.coe
-- 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 𝓧) ∘ₘ μ)
h1 :
  ∀ {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t),
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
      (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t)
h2 :
  ∀ {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t),
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t,
        κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x.1 x.2 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
      (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t)
s : Set Ω
hs : MeasurableSet s
t : Set 𝓧
ht : MeasurableSet t
refine_2 :
  (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t) =
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t,
      κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x.1 x.2 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
refine_2₁ refine_2₂ :
  Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
    ((μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
⊢ ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t,
      κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x.1 x.2 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)

Tactic:
rw [h1 hs ht, h2 hs ht]
-- 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 𝓧) ∘ₘ μ)
⊢ ∀ᵐ (x : Ω) ∂μ,
    ∀ᵐ (y : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
      (κ†μ).rnDeriv (Kernel.const 𝓧 μ) (x, y).2 (x, y).1 =
        κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) (x, y).1 (x, y).2

Tactic:
Measure.ae_ae_of_ae_prod
      (rnDeriv_posterior_ae_prod h_ac)

Premises used: MeasureTheory.Measure.ae_ae_of_ae_prod, ProbabilityTheory.rnDeriv_posterior_ae_prod
-- 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 𝓧) ∘ₘ μ)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    ∀ᵐ (x : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
      (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x

Tactic:
convert!
    Measure.ae_ae_of_ae_prod
      (rnDeriv_posterior_ae_prod h_ac)

Premises used: MeasureTheory.Measure.ae_ae_of_ae_prod, ProbabilityTheory.rnDeriv_posterior_ae_prod
-- 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 𝓧) ∘ₘ μ)
rw :
  ∀ᵐ (y : Ω) ∂μ,
    ∀ᵐ (x : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
      (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x y = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) y x
rw₁ :
  MeasurableSet (α := 𝓧 × Ω)
    {x : 𝓧 × Ω |
      (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.1 x.2 = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x.2 x.1}
⊢ ∀ᵐ (x : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
    ∀ᵐ (ω : Ω) ∂μ,
      (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x

Tactic:
rw [Measure.ae_ae_comm]

Premises used: MeasureTheory.Measure.ae_ae_comm
-- 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 𝓧) ∘ₘ μ)
⊢ ∀ᵐ (y : Ω) ∂μ,
    ∀ᵐ (x : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
      (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x y = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) y x

Tactic:
rnDeriv_posterior h_ac

Premises used: ProbabilityTheory.rnDeriv_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 𝓧) ∘ₘ μ)
⊢ ∀ᵐ (y : Ω) ∂μ,
    ∀ᵐ (x : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
      (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x y = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) y x

Tactic:
exact rnDeriv_posterior h_ac

Premises used: ProbabilityTheory.rnDeriv_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 𝓧) ∘ₘ μ)
⊢ MeasurableSet (α := 𝓧 × Ω)
    {x : 𝓧 × Ω |
      (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.1 x.2 = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x.2 x.1}

Tactic:
measurability
-- 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 𝓧) ∘ₘ μ)
h :
  ∀ (x : 𝓧)
    (h :
      ∀ᵐ (ω : Ω) ∂μ,
        (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x)
    (h_ac' : (κ†μ : (a : 𝓧) → Measure Ω) x ≪ μ),
    (κ†μ : (a : 𝓧) → Measure Ω) x =
      μ.withDensity fun (ω : Ω) ↦ κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
⊢ ∀ᵐ (x : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
    (κ†μ : (a : 𝓧) → Measure Ω) x =
      μ.withDensity fun (ω : Ω) ↦ κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x

Tactic:
filter_upwards [rnDeriv_posterior_symm h_ac, absolutelyContinuous_posterior h_ac] with x h h_ac'

Premises used: ProbabilityTheory.rnDeriv_posterior_symm, 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 𝓧) ∘ₘ μ)
x : 𝓧
h :
  ∀ᵐ (ω : Ω) ∂μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
h_ac' : (κ†μ : (a : 𝓧) → Measure Ω) x ≪ μ
h₁ :
  ∀ (s : Set Ω) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((κ†μ : (a : 𝓧) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      ((μ.withDensity fun (ω : Ω) ↦ κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x :
            (a : Set Ω) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ (κ†μ : (a : 𝓧) → Measure Ω) x =
    μ.withDensity fun (ω : Ω) ↦ κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x

Tactic:
ext s hs
-- 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 𝓧) ∘ₘ μ)
x : 𝓧
h :
  ∀ᵐ (ω : Ω) ∂μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
h_ac' : (κ†μ : (a : 𝓧) → Measure Ω) x ≪ μ
s : Set Ω
hs : MeasurableSet s
h₁ :
  ∫⁻ (x_1 : Ω) in s, (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) x_1 ∂μ =
    ∫⁻ (a : Ω) in s, κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) a x ∂μ
⊢ Eq (α := ℝ≥0∞) ((((κ†μ : (a : 𝓧) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.withDensity fun (ω : Ω) ↦ κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x : (a : Set Ω) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
rw [← Measure.setLIntegral_rnDeriv h_ac', withDensity_apply _ hs]

Premises used: MeasureTheory.Measure.setLIntegral_rnDeriv, MeasureTheory.withDensity_apply
-- 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 𝓧) ∘ₘ μ)
x : 𝓧
h :
  ∀ᵐ (ω : Ω) ∂μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
h_ac' : (κ†μ : (a : 𝓧) → Measure Ω) x ≪ μ
s : Set Ω
hs : MeasurableSet s
⊢ ∫⁻ (x_1 : Ω) in s, (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) x_1 ∂μ =
    ∫⁻ (a : Ω) in s, κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) a x ∂μ

Tactic:
setLIntegral_congr_fun_ae hs ?_

Premises used: MeasureTheory.setLIntegral_congr_fun_ae
-- 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 𝓧) ∘ₘ μ)
x : 𝓧
h :
  ∀ᵐ (ω : Ω) ∂μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
h_ac' : (κ†μ : (a : 𝓧) → Measure Ω) x ≪ μ
s : Set Ω
hs : MeasurableSet s
h₁ :
  ∀ᵐ (x_1 : Ω) ∂μ,
    x_1 ∈ s →
      (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) x_1 = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x_1 x
⊢ ∫⁻ (x_1 : Ω) in s, (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) x_1 ∂μ =
    ∫⁻ (a : Ω) in s, κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) a x ∂μ

Tactic:
refine setLIntegral_congr_fun_ae hs ?_

Premises used: MeasureTheory.setLIntegral_congr_fun_ae
-- 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 𝓧) ∘ₘ μ)
x : 𝓧
h :
  ∀ᵐ (ω : Ω) ∂μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
h_ac' : (κ†μ : (a : 𝓧) → Measure Ω) x ≪ μ
s : Set Ω
hs : MeasurableSet s
h₁ :
  ∀ (ω : Ω)
    (h : (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x)
    (h_eq :
      (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω =
        Measure.rnDeriv (m := mΩ) ((κ†μ : (a : 𝓧) → Measure Ω) x)
          (((Kernel.const 𝓧 μ : Kernel 𝓧 Ω) : (a : 𝓧) → Measure Ω) x) ω)
    (hωs : ω ∈ s),
    (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
⊢ ∀ᵐ (x_1 : Ω) ∂μ,
    x_1 ∈ s →
      (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) x_1 = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x_1 x

Tactic:
filter_upwards [h, Kernel.rnDeriv_eq_rnDeriv_measure (κ := κ†μ) (η := Kernel.const 𝓧 μ) (a := x)]
    with ω h h_eq hωs

Premises used: ProbabilityTheory.Kernel.rnDeriv_eq_rnDeriv_measure
-- 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 𝓧) ∘ₘ μ)
x : 𝓧
h_1 :
  ∀ᵐ (ω : Ω) ∂μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
h_ac' : (κ†μ : (a : 𝓧) → Measure Ω) x ≪ μ
s : Set Ω
hs : MeasurableSet s
ω : Ω
h : (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x
h_eq :
  (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω =
    Measure.rnDeriv (m := mΩ) ((κ†μ : (a : 𝓧) → Measure Ω) x)
      (((Kernel.const 𝓧 μ : Kernel 𝓧 Ω) : (a : 𝓧) → Measure Ω) x) ω
hωs : ω ∈ s
h₁ : (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) ω = (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω
h₂ :
  (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) ω =
    Measure.rnDeriv (m := mΩ) ((κ†μ : (a : 𝓧) → Measure Ω) x)
      (((Kernel.const 𝓧 μ : Kernel 𝓧 Ω) : (a : 𝓧) → Measure Ω) x) ω
h₃ h₄ : (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) ω = (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) ω
⊢ (∂(κ†μ : (a : 𝓧) → Measure Ω) x/∂μ) ω = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x

Tactic:
rw [← h, h_eq, Kernel.const_apply]

Premises used: ProbabilityTheory.Kernel.const_apply
-- Module: Mathlib.Probability.Kernel.Posterior
Goal:
𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
Ω : Type u_5
inst : Countable Ω
inst_1 : MeasurableSpace Ω
inst_2 : Nonempty Ω
inst_3 : StandardBorelSpace Ω
κ : Kernel Ω 𝓧
inst_4 : IsFiniteKernel κ
μ : Measure Ω
inst_5 : IsFiniteMeasure μ
⊢ ∀ (ω : Ω),
    κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ))
        ω =ᶠ[ae (F := Measure 𝓧)
        ((Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) : (a : Ω) → Measure 𝓧) ω : Measure 𝓧)]
      Measure.rnDeriv (m := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
        ((Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) : (a : Ω) → Measure 𝓧) ω)

Tactic:
have h_rnDeriv ω := Kernel.rnDeriv_eq_rnDeriv_measure (κ := κ) (η := Kernel.const Ω (κ ∘ₘ μ))
    (a := ω)
-- Module: Mathlib.Probability.Kernel.Posterior
Goal:
𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
Ω : Type u_5
inst : Countable Ω
inst_1 : MeasurableSpace Ω
inst_2 : Nonempty Ω
inst_3 : StandardBorelSpace Ω
κ : Kernel Ω 𝓧
inst_4 : IsFiniteKernel κ
μ : Measure Ω
inst_5 : IsFiniteMeasure μ
h_rnDeriv :
  ∀ (ω : Ω),
    ∀ᵐ (x : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
      κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x =
        Measure.rnDeriv (m := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) x
⊢ ∀ᵐ (a : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
    ∀ (i : Ω),
      κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) i a =
        Measure.rnDeriv (m := m𝓧) ((κ : (a : Ω) → Measure 𝓧) i) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) a

Tactic:
rw [← ae_all_iff] at h_rnDeriv

Premises used: MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.Kernel.Posterior
Goal:
𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
Ω : Type u_5
inst : Countable Ω
inst_1 : MeasurableSpace Ω
inst_2 : Nonempty Ω
inst_3 : StandardBorelSpace Ω
κ : Kernel Ω 𝓧
inst_4 : IsFiniteKernel κ
μ : Measure Ω
inst_5 : IsFiniteMeasure μ
h_rnDeriv :
  ∀ᵐ (a : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
    ∀ (i : Ω),
      κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) i a =
        Measure.rnDeriv (m := m𝓧) ((κ : (a : Ω) → Measure 𝓧) i) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) a
h :
  ∀ (x : 𝓧)
    (hx :
      (κ†μ : (a : 𝓧) → Measure Ω) x =
        μ.withDensity fun (ω : Ω) ↦ κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω x)
    (hx_all :
      ∀ (i : Ω),
        κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) i x =
          Measure.rnDeriv (m := m𝓧) ((κ : (a : Ω) → Measure 𝓧) i) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) x),
    (κ†μ : (a : 𝓧) → Measure Ω) x =
      μ.withDensity fun (ω : Ω) ↦
        Measure.rnDeriv (m := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) x
⊢ ∀ᵐ (x : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
    (κ†μ : (a : 𝓧) → Measure Ω) x =
      μ.withDensity fun (ω : Ω) ↦
        Measure.rnDeriv (m := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) x

Tactic:
filter_upwards [posterior_eq_withDensity Measure.absolutelyContinuous_comp_of_countable,
    h_rnDeriv] with x hx hx_all

Premises used: ProbabilityTheory.posterior_eq_withDensity, MeasureTheory.Measure.absolutelyContinuous_comp_of_countable