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 𝓧) ∘ₘ μ)
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
rw :
  ∫⁻ (y : 𝓧) in t,
      ∫⁻ (x : Ω) in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) (x, y).2 (x, y).1 ∂μ ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ =
    ∫⁻ (a : 𝓧) in t,
      (((κ†μ : (a : 𝓧) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ
⊢ ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
    (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t)

Tactic:
rw [setLIntegral_prod_symm _ (by fun_prop), ← swap_compProd_posterior, Measure.swap_comp,
      Measure.map_apply measurable_swap (hs.prod ht), Set.preimage_swap_prod,
      Measure.compProd_apply_prod ht hs]

Premises used: MeasureTheory.setLIntegral_prod_symm, MeasureTheory.Measure.swap_comp, MeasureTheory.Measure.map_apply, MeasurableSet.prod, measurable_swap, MeasureTheory.Measure.compProd_apply_prod, ProbabilityTheory.swap_compProd_posterior, Set.preimage_swap_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 𝓧) ∘ₘ μ)
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (y : 𝓧) in t,
      ∫⁻ (x : Ω) in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) (x, y).2 (x, y).1 ∂μ ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ =
    ∫⁻ (a : 𝓧) in t,
      (((κ†μ : (a : 𝓧) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ

Tactic:
lintegral_congr_ae <| ae_restrict_of_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae, MeasureTheory.ae_restrict_of_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 𝓧) ∘ₘ μ)
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
refine :
  ∀ᵐ (x : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
    Eq (α := ℝ≥0∞) ((fun (y : 𝓧) ↦ ∫⁻ (x : Ω) in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) (x, y).2 (x, y).1 ∂μ) x)
      ((fun (a : 𝓧) ↦ ((((κ†μ : (a : 𝓧) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)) x)
⊢ ∫⁻ (y : 𝓧) in t,
      ∫⁻ (x : Ω) in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) (x, y).2 (x, y).1 ∂μ ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ =
    ∫⁻ (a : 𝓧) in t,
      (((κ†μ : (a : 𝓧) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ

Tactic:
refine lintegral_congr_ae <| ae_restrict_of_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae, MeasureTheory.ae_restrict_of_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 𝓧) ∘ₘ μ)
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
h :
  ∀ (x : 𝓧) (h_ac' : (κ†μ : (a : 𝓧) → Measure Ω) x ≪ μ),
    ∫⁻ (x_1 : Ω) in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x x_1 ∂μ =
      (((κ†μ : (a : 𝓧) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s
⊢ ∀ᵐ (x : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
    Eq (α := ℝ≥0∞) ((fun (y : 𝓧) ↦ ∫⁻ (x : Ω) in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) (x, y).2 (x, y).1 ∂μ) x)
      ((fun (a : 𝓧) ↦ ((((κ†μ : (a : 𝓧) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)) x)

Tactic:
filter_upwards [absolutelyContinuous_posterior h_ac] with x 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
x : 𝓧
h_ac' : (κ†μ : (a : 𝓧) → Measure Ω) x ≪ μ
h :
  ∫⁻ (ω : Ω) in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω ∂((Kernel.const 𝓧 μ : Kernel 𝓧 Ω) : (a : 𝓧) → Measure Ω) x =
    (((κ†μ : (a : 𝓧) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s
⊢ ∫⁻ (x_1 : Ω) in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x x_1 ∂μ =
    (((κ†μ : (a : 𝓧) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s

Tactic:
change ∫⁻ ω in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω ∂(Kernel.const 𝓧 μ x) = _

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

Tactic:
rw [Kernel.setLIntegral_rnDeriv h_ac' hs]

Premises used: ProbabilityTheory.Kernel.setLIntegral_rnDeriv
-- 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),
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
      (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t)

Tactic:
have h1 {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t) :
      ∫⁻ x in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const _ μ) x.2 x.1 ∂μ.prod (⇑κ ∘ₘ μ)
        = (μ ⊗ₘ κ) (s ×ˢ t) := by
    rw [setLIntegral_prod_symm _ (by fun_prop), ← swap_compProd_posterior, Measure.swap_comp,
      Measure.map_apply measurable_swap (hs.prod ht), Set.preimage_swap_prod,
      Measure.compProd_apply_prod ht hs]
    refine lintegral_congr_ae <| ae_restrict_of_ae ?_
    filter_upwards [absolutelyContinuous_posterior h_ac] with x h_ac'
    change ∫⁻ ω in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω ∂(Kernel.const 𝓧 μ x) = _
    rw [Kernel.setLIntegral_rnDeriv h_ac' 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 𝓧) ∘ₘ μ)
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)
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
⊢ AEMeasurable (β := ℝ≥0∞) (_m := Prod.instMeasurableSpace)
    (fun (x : Ω × 𝓧) ↦ κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x.1 x.2)
    (Measure.restrict (μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) (s ×ˢ t))

Tactic:
fun_prop
-- 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)
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
rw :
  ∫⁻ (x : Ω) in s,
      ∫⁻ (y : 𝓧) in t,
        κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) (x, y).1
          (x, y).2 ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ ∂μ =
    ∫⁻ (a : Ω) in s, (((κ : (a : Ω) → Measure 𝓧) a : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) t ∂μ
⊢ ∫⁻ (x : Ω × 𝓧) in s ×ˢ t,
      κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) x.1 x.2 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) =
    (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) (s ×ˢ t)

Tactic:
rw [setLIntegral_prod _ (by fun_prop), Measure.compProd_apply_prod hs ht]

Premises used: MeasureTheory.Measure.compProd_apply_prod, MeasureTheory.setLIntegral_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 𝓧) ∘ₘ μ)
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)
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (x : Ω) in s,
      ∫⁻ (y : 𝓧) in t,
        κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) (x, y).1
          (x, y).2 ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ ∂μ =
    ∫⁻ (a : Ω) in s, (((κ : (a : Ω) → Measure 𝓧) a : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) t ∂μ

Tactic:
lintegral_congr_ae <| ae_restrict_of_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae, MeasureTheory.ae_restrict_of_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 𝓧) ∘ₘ μ)
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)
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
refine :
  ∀ᵐ (x : Ω) ∂μ,
    Eq (α := ℝ≥0∞)
      ((fun (x : Ω) ↦
          ∫⁻ (y : 𝓧) in t,
            κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) (x, y).1
              (x, y).2 ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        x)
      ((fun (a : Ω) ↦ ((((κ : (a : Ω) → Measure 𝓧) a : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) t : ℝ≥0∞)) x)
⊢ ∫⁻ (x : Ω) in s,
      ∫⁻ (y : 𝓧) in t,
        κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) (x, y).1
          (x, y).2 ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ ∂μ =
    ∫⁻ (a : Ω) in s, (((κ : (a : Ω) → Measure 𝓧) a : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) t ∂μ

Tactic:
refine lintegral_congr_ae <| ae_restrict_of_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae, MeasureTheory.ae_restrict_of_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 𝓧) ∘ₘ μ)
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)
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
h :
  ∀ (ω : Ω)
    (h_ac :
      Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
        ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)),
    ∫⁻ (y : 𝓧) in t, κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω y ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ =
      (((κ : (a : Ω) → Measure 𝓧) ω : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) t
⊢ ∀ᵐ (x : Ω) ∂μ,
    Eq (α := ℝ≥0∞)
      ((fun (x : Ω) ↦
          ∫⁻ (y : 𝓧) in t,
            κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) (x, y).1
              (x, y).2 ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        x)
      ((fun (a : Ω) ↦ ((((κ : (a : Ω) → Measure 𝓧) a : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) t : ℝ≥0∞)) x)

Tactic:
filter_upwards [h_ac] with ω h_ac
-- 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_1 :
  ∀ᵐ (ω : Ω) ∂μ,
    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)
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
ω : Ω
h_ac :
  Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
    ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
h h₁ :
  Eq (α := ℝ≥0∞) ((((κ : (a : Ω) → Measure 𝓧) ω : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) t : ℝ≥0∞)
    ((((κ : (a : Ω) → Measure 𝓧) ω : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∫⁻ (x : 𝓧) in t,
      κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω
        x ∂(Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) : (a : Ω) → Measure 𝓧) ω =
    (((κ : (a : Ω) → Measure 𝓧) ω : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) t

Tactic:
rw [Kernel.setLIntegral_rnDeriv h_ac ht]

Premises used: ProbabilityTheory.Kernel.setLIntegral_rnDeriv
-- 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)
⊢ ∀ {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)

Tactic:
have h2 {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t) :
  -- Second, the integral of the right-hand side on `s ×ˢ t` is `(μ ⊗ₘ κ) (s ×ˢ t)`.
      ∫⁻ x in s ×ˢ t, κ.rnDeriv (Kernel.const _ (κ ∘ₘ μ)) x.1 x.2 ∂μ.prod (⇑κ ∘ₘ μ)
        = (μ ⊗ₘ κ) (s ×ˢ t) := by
    rw [setLIntegral_prod _ (by fun_prop), Measure.compProd_apply_prod hs ht]
    refine lintegral_congr_ae <| ae_restrict_of_ae ?_
    filter_upwards [h_ac] with ω h_ac
    change ∫⁻ x in t, κ.rnDeriv (Kernel.const Ω (κ ∘ₘ μ)) ω x ∂(Kernel.const Ω (κ ∘ₘ μ) ω) = _
    rw [Kernel.setLIntegral_rnDeriv h_ac 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 𝓧) ∘ₘ μ)
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)
⊢ AEMeasurable (β := ℝ≥0∞) (_m := Prod.instMeasurableSpace) (fun (p : Ω × 𝓧) ↦ (κ†μ).rnDeriv (Kernel.const 𝓧 μ) p.2 p.1)
    (μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ))

Tactic:
fun_prop
-- 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)
⊢ AEMeasurable (β := ℝ≥0∞) (_m := Prod.instMeasurableSpace)
    (fun (p : Ω × 𝓧) ↦ κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) p.1 p.2)
    (μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ))

Tactic:
fun_prop
-- 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 𝓧) ∘ₘ μ) ≠ ∞
refine_2 :
  ∀ ⦃s : Set Ω⦄,
    MeasurableSet s →
      ∀ ⦃t : Set 𝓧⦄,
        MeasurableSet t →
          ∫⁻ (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 𝓧) ∘ₘ μ)
⊢ ∀ᵐ (p : Ω × 𝓧) ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ),
    (κ†μ).rnDeriv (Kernel.const 𝓧 μ) p.2 p.1 = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) p.1 p.2

Tactic:
refine ae_eq_of_setLIntegral_prod_eq (by fun_prop) (by fun_prop) ?_ ?_

Premises used: MeasureTheory.ae_eq_of_setLIntegral_prod_eq
-- 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)
⊢ ∫⁻ (x : Ω × 𝓧), (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ≠ ∞

Tactic:
ne_of_lt ?_

Premises used: ne_of_lt