awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
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 𝓧) ∘ₘ μ) μ
⊢ μ ⊗ₘ κ ≪ μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
have rw : Measure.AbsolutelyContinuous (_m0 := Prod.instMeasurableSpace)
  (Measure.map Prod.swap (((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ))
  (Measure.map Prod.swap (Measure.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) μ))
Tactic: rw [← swap_compProd_posterior, ← Measure.prod_swap, Measure.swap_comp]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
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 ≪ μ
⊢ μ ⊗ₘ κ ≪ μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
have suffices : ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ ≪ Measure.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) μ
Tactic: suffices (κ ∘ₘ μ) ⊗ₘ κ†μ ≪ (κ ∘ₘ μ).prod μ by
    rw [← swap_compProd_posterior, ← Measure.prod_swap, Measure.swap_comp]
    exact this.map measurable_swap
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
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 𝓧) ∘ₘ μ) ⊗ₘ κ†μ ≪ Measure.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) μ
have rw : ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ ≪ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ Kernel.const 𝓧 μ
Tactic: rw [← Measure.compProd_const]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
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 𝓧 μ
have refine : ∀ᵐ (a : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ,
  Measure.AbsolutelyContinuous.{u_1} (α := Ω) (_m0 := mΩ) ((κ†μ : (a : 𝓧) → Measure Ω) a)
    (((Kernel.const 𝓧 μ : Kernel 𝓧 Ω) : (a : 𝓧) → Measure Ω) a)
Tactic: refine Measure.AbsolutelyContinuous.compProd_right ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
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 𝓧) ω ≪ ν
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Measure.AbsolutelyContinuous.{u_2} (α := 𝓧) (_m0 := m𝓧) ((κ : (a : Ω) → Measure 𝓧) ω)
      ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
have rw : ∀ᵐ (b : 𝓧) ∂(⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ, (κ†μ : (a : 𝓧) → Measure Ω) b ≪ μ
Tactic: rw [← absolutelyContinuous_posterior_iff]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
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)
have 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 𝓧) ∘ₘ μ
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
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 𝓧) ∘ₘ μ
have 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)
Tactic: refine lintegral_congr_ae <| ae_restrict_of_ae ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
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 : 𝓧) ∂(⇑κ : (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)
have 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
Tactic: filter_upwards [absolutelyContinuous_posterior h_ac] with x h_ac'
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
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 ≪ μ
⊢ ∫⁻ (x_1 : Ω) in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x x_1 ∂μ =
    (((κ†μ : (a : 𝓧) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s
have h : ∫⁻ (ω : Ω) in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω ∂((Kernel.const 𝓧 μ : Kernel 𝓧 Ω) : (a : 𝓧) → Measure Ω) x =
  (((κ†μ : (a : 𝓧) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s
Tactic: change ∫⁻ ω in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω ∂(Kernel.const 𝓧 μ x) = _
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
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 ≪ μ
⊢ ∫⁻ (ω : Ω) in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω ∂((Kernel.const 𝓧 μ : Kernel 𝓧 Ω) : (a : 𝓧) → Measure Ω) x =
    (((κ†μ : (a : 𝓧) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s
have h : Eq (α := ℝ≥0∞) ((((κ†μ : (a : 𝓧) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
  ((((κ†μ : (a : 𝓧) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Kernel.setLIntegral_rnDeriv h_ac' hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (hypothesis)
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 𝓧) ∘ₘ μ)
⊢ ∀ᵐ (p : Ω × 𝓧) ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ),
    (κ†μ).rnDeriv (Kernel.const 𝓧 μ) p.2 p.1 = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) p.1 p.2
have 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)
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
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)
have 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 ∂μ
Tactic: rw [setLIntegral_prod _ (by fun_prop), Measure.compProd_apply_prod hs ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
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 ∂μ
have 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)
Tactic: refine lintegral_congr_ae <| ae_restrict_of_ae ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
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 : Ω) ∂μ,
    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)
have 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
Tactic: filter_upwards [h_ac] with ω h_ac
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
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 𝓧) ∘ₘ μ)
⊢ ∫⁻ (x : 𝓧) in t,
      κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) ω
        x ∂(Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) : (a : Ω) → Measure 𝓧) ω =
    (((κ : (a : Ω) → Measure 𝓧) ω : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) t
have h : Eq (α := ℝ≥0∞) ((((κ : (a : Ω) → Measure 𝓧) ω : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) t : ℝ≥0∞)
  ((((κ : (a : Ω) → Measure 𝓧) ω : Measure 𝓧) : (a : Set 𝓧) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [Kernel.setLIntegral_rnDeriv h_ac ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (hypothesis)
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)
⊢ ∀ᵐ (p : Ω × 𝓧) ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ),
    (κ†μ).rnDeriv (Kernel.const 𝓧 μ) p.2 p.1 = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) p.1 p.2
have 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)
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
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)
⊢ ∀ᵐ (p : Ω × 𝓧) ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ),
    (κ†μ).rnDeriv (Kernel.const 𝓧 μ) p.2 p.1 = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) p.1 p.2
have refine_1 : ∫⁻ (x : Ω × 𝓧), (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ≠ ∞
Tactic: refine ae_eq_of_setLIntegral_prod_eq (by fun_prop) (by fun_prop) ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
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 𝓧) ∘ₘ μ) ≠ ∞
⊢ ∀ᵐ (p : Ω × 𝓧) ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ),
    (κ†μ).rnDeriv (Kernel.const 𝓧 μ) p.2 p.1 = κ.rnDeriv (Kernel.const Ω ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)) p.1 p.2
have 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 𝓧) ∘ₘ μ)
Tactic: refine ae_eq_of_setLIntegral_prod_eq (by fun_prop) (by fun_prop) ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
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 𝓧) ∘ₘ μ) ≠ ∞
have refine_1 : ∫⁻ (x : Ω × 𝓧), (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) < ∞
Tactic: refine ne_of_lt ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
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 𝓧) ∘ₘ μ) =
    (μ ⊗ₘ κ : (a : Set (Ω × 𝓧)) → ℝ≥0∞) Set.univ
have rw : ∫⁻ (x : Ω × 𝓧) in Set.univ, (κ†μ).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]