awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
refine :
  ∀ x_1 ∈ countablePartitionSet n x ×ˢ s,
    Membership.mem (γ := Set (γ × β)) {p : γ × β | p.1 ∈ countablePartitionSet n x} x_1
⊢ LE.le (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ s) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        {p : γ × β | p.1 ∈ countablePartitionSet n x} :
      ℝ≥0∞)

Tactic:
refine measure_mono (fun x ↦ ?_)

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x_1 : γ
s : Set β
x : γ × β
simp : x.1 ∈ countablePartitionSet n x_1 → x.2 ∈ s → x.1 ∈ countablePartitionSet n x_1
⊢ x ∈ countablePartitionSet n x_1 ×ˢ s →
    Membership.mem (γ := Set (γ × β)) {p : γ × β | p.1 ∈ countablePartitionSet n x_1} x

Tactic:
simp only [mem_prod, mem_setOf_eq, and_imp]

Premises used: and_imp, Set.mem_setOf_eq, Set.mem_prod
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x_1 : γ
s : Set β
x : γ × β
⊢ x.1 ∈ countablePartitionSet n x_1 → x.2 ∈ s → x.1 ∈ countablePartitionSet n x_1

Tactic:
fun h _ ↦ h
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x_1 : γ
s : Set β
x : γ × β
⊢ x.1 ∈ countablePartitionSet n x_1 → x.2 ∈ s → x.1 ∈ countablePartitionSet n x_1

Tactic:
exact fun h _ ↦ h
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
⊢ LE.le (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
    ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)

Tactic:
hκν a _
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
calc :
  LE.le (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ s) :
      ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ s) :
      ℝ≥0∞)
    ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)

Tactic:
calc κ a (countablePartitionSet n x ×ˢ s)
    ≤ fst κ a (countablePartitionSet n x) := by
        rw [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)]
        refine measure_mono (fun x ↦ ?_)
        simp only [mem_prod, mem_setOf_eq, and_imp]
        exact fun h _ ↦ h
  _ ≤ ν a (countablePartitionSet n x) := hκν a _

Premises used: SProd.sprod, MeasurableSpace.countablePartitionSet, DFunLike.coe, ProbabilityTheory.Kernel.fst
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
⊢ κ.densityProcess ν n a x s ≤ 1

Tactic:
ENNReal.toReal_le_of_le_ofReal zero_le_one (ENNReal.div_le_of_le_mul ?_)

Premises used: zero_le_one, ProbabilityTheory.Kernel.densityProcess, ENNReal.div_le_of_le_mul, ENNReal.toReal_le_of_le_ofReal
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
refine :
  (((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (countablePartitionSet n x ×ˢ s) ≤
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal 1)
      ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
⊢ κ.densityProcess ν n a x s ≤ 1

Tactic:
refine ENNReal.toReal_le_of_le_ofReal zero_le_one (ENNReal.div_le_of_le_mul ?_)

Premises used: zero_le_one, ENNReal.div_le_of_le_mul, ENNReal.toReal_le_of_le_ofReal
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
rw :
  LE.le (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ s) :
      ℝ≥0∞)
    ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
⊢ (((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (countablePartitionSet n x ×ˢ s) ≤
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal 1)
      ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)

Tactic:
rw [ENNReal.ofReal_one, one_mul]

Premises used: ENNReal.ofReal_one, one_mul
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
⊢ LE.le (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ s) :
      ℝ≥0∞)
    ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)

Tactic:
meas_countablePartitionSet_le_of_fst_le hκν n a x s

Premises used: ProbabilityTheory.Kernel.meas_countablePartitionSet_le_of_fst_le
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
⊢ LE.le (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ s) :
      ℝ≥0∞)
    ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)

Tactic:
exact meas_countablePartitionSet_le_of_fst_le hκν n a x s

Premises used: ProbabilityTheory.Kernel.meas_countablePartitionSet_le_of_fst_le
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
s : Set β
⊢ @eLpNorm _ ℝ _ mγ (fun (x : γ) ↦ κ.densityProcess ν n a x s) 1 ((ν : (a : α) → Measure γ) a) ≤
    (((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ

Tactic:
(eLpNorm_le_of_ae_bound (C := 1) (ae_of_all _ (fun x ↦ ?_))).trans ?_

Premises used: MeasureTheory.ae_of_all, LE.le.trans, MeasureTheory.eLpNorm_le_of_ae_bound
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
s : Set β
refine_1 : ∀ (x : γ), ‖κ.densityProcess ν n a x s‖ ≤ 1
refine_2 :
  HPow.hPow (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
        (ENNReal.toReal 1)⁻¹ *
      ENNReal.ofReal 1 ≤
    (((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ
⊢ @eLpNorm _ ℝ _ mγ (fun (x : γ) ↦ κ.densityProcess ν n a x s) 1 ((ν : (a : α) → Measure γ) a) ≤
    (((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ

Tactic:
refine (eLpNorm_le_of_ae_bound (C := 1) (ae_of_all _ (fun x ↦ ?_))).trans ?_

Premises used: MeasureTheory.ae_of_all, LE.le.trans, MeasureTheory.eLpNorm_le_of_ae_bound
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
s : Set β
x : γ
⊢ ‖κ.densityProcess ν n a x s‖ ≤ 1

Tactic:
simp only [Real.norm_eq_abs, abs_of_nonneg (densityProcess_nonneg κ ν n a x s),
      densityProcess_le_one hκν n a x s]

Premises used: ProbabilityTheory.Kernel.densityProcess_le_one, ProbabilityTheory.Kernel.densityProcess_nonneg, abs_of_nonneg, Real.norm_eq_abs
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
s : Set β
⊢ HPow.hPow (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
        (ENNReal.toReal 1)⁻¹ *
      ENNReal.ofReal 1 ≤
    (((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
rw : MemLp (ε := ℝ) (m0 := mγ) (fun (x : γ) ↦ κ.densityProcess ν n a x s) 1 ((ν : (a : α) → Measure γ) a)
⊢ @Integrable ℝ _ _ _ mγ (fun (x : γ) ↦ κ.densityProcess ν n a x s) ((ν : (a : α) → Measure γ) a)

Tactic:
rw [← memLp_one_iff_integrable]

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ MemLp (ε := ℝ) (m0 := mγ) (fun (x : γ) ↦ κ.densityProcess ν n a x s) 1 ((ν : (a : α) → Measure γ) a)

Tactic:
⟨Measurable.aestronglyMeasurable ?_, ?_⟩

Premises used: Measurable.aestronglyMeasurable, MeasureTheory.MemLp, And.intro
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
refine_1 : Measurable (β := ℝ) fun (x : γ) ↦ κ.densityProcess ν n a x s
refine_2 : @eLpNorm _ ℝ _ mγ (fun (x : γ) ↦ κ.densityProcess ν n a x s) 1 ((ν : (a : α) → Measure γ) a) < ∞
⊢ MemLp (ε := ℝ) (m0 := mγ) (fun (x : γ) ↦ κ.densityProcess ν n a x s) 1 ((ν : (a : α) → Measure γ) a)

Tactic:
refine ⟨Measurable.aestronglyMeasurable ?_, ?_⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ) fun (x : γ) ↦ κ.densityProcess ν n a x s

Tactic:
measurable_densityProcess_right κ ν n a hs

Premises used: ProbabilityTheory.Kernel.measurable_densityProcess_right
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ) fun (x : γ) ↦ κ.densityProcess ν n a x s

Tactic:
exact measurable_densityProcess_right κ ν n a hs

Premises used: ProbabilityTheory.Kernel.measurable_densityProcess_right
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ @eLpNorm _ ℝ _ mγ (fun (x : γ) ↦ κ.densityProcess ν n a x s) 1 ((ν : (a : α) → Measure γ) a) < ∞

Tactic:
(eLpNorm_densityProcess_le hκν n a s).trans_lt (measure_lt_top _ _)

Premises used: MeasureTheory.measure_lt_top, ProbabilityTheory.Kernel.eLpNorm_densityProcess_le, LE.le.trans_lt
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ @eLpNorm _ ℝ _ mγ (fun (x : γ) ↦ κ.densityProcess ν n a x s) 1 ((ν : (a : α) → Measure γ) a) < ∞

Tactic:
exact (eLpNorm_densityProcess_le hκν n a s).trans_lt (measure_lt_top _ _)

Premises used: MeasureTheory.measure_lt_top, ProbabilityTheory.Kernel.eLpNorm_densityProcess_le, LE.le.trans_lt
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
⊢ IsFiniteKernel κ

Tactic:
have : IsFiniteKernel κ := isFiniteKernel_of_isFiniteKernel_fst (h := isFiniteKernel_of_le hκν)
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this : IsFiniteKernel κ
⊢ MeasurableSet u

Tactic:
have hu_meas : MeasurableSet u := measurableSet_countablePartition n hu
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this : IsFiniteKernel κ
hu_meas : MeasurableSet u
rw :
  (∫⁻ (a_1 : γ) in u,
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (countablePartitionSet n a_1 ×ˢ s) :
            ℝ≥0∞)
          ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n a_1) :
            ℝ≥0∞) ∂(ν : (a : α) → Measure γ) a).toReal =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (u ×ˢ s)
hfm :
  AEMeasurable (β := ℝ≥0∞) (_m := mγ)
    (fun (x : γ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n x ×ˢ s) :
          ℝ≥0∞)
        ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞))
    (Measure.restrict ((ν : (a : α) → Measure γ) a) u)
hf :
  ∀ᵐ (x : γ) ∂Measure.restrict ((ν : (a : α) → Measure γ) a) u,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n x ×ˢ s) :
          ℝ≥0∞)
        ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞) <
      ∞
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) u) fun (x : γ) ↦
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (countablePartitionSet n x ×ˢ s) :
            ℝ≥0∞)
          ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) :
            ℝ≥0∞)).toReal) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (u ×ˢ s)

Tactic:
rw [integral_toReal]

Premises used: MeasureTheory.integral_toReal
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this : IsFiniteKernel κ
hu_meas : MeasurableSet u
⊢ AEMeasurable (β := ℝ≥0∞) (_m := mγ)
    (fun (x : γ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n x ×ˢ s) :
          ℝ≥0∞)
        ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞))
    (Measure.restrict ((ν : (a : α) → Measure γ) a) u)

Tactic:
Measurable.aemeasurable ?_

Premises used: Measurable.aemeasurable
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this : IsFiniteKernel κ
hu_meas : MeasurableSet u
hfm :
  Measurable (β := ℝ≥0∞) fun (x : γ) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ s) :
        ℝ≥0∞)
      ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
⊢ AEMeasurable (β := ℝ≥0∞) (_m := mγ)
    (fun (x : γ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n x ×ˢ s) :
          ℝ≥0∞)
        ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞))
    (Measure.restrict ((ν : (a : α) → Measure γ) a) u)

Tactic:
refine Measurable.aemeasurable ?_

Premises used: Measurable.aemeasurable
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this : IsFiniteKernel κ
hu_meas : MeasurableSet u
hfm :
  Measurable.{u_3, 0} (α := γ) (β := ℝ≥0∞)
    ((fun (p : α × γ) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) p.1 : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (countablePartitionSet n p.2 ×ˢ s) :
            ℝ≥0∞)
          ((((ν : (a : α) → Measure γ) p.1 : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n p.2) : ℝ≥0∞)) ∘
      fun (x : γ) ↦ (a, x))
⊢ Measurable (β := ℝ≥0∞) fun (x : γ) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ s) :
        ℝ≥0∞)
      ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)

Tactic:
change Measurable ((fun (p : α × _) ↦ κ p.1 (countablePartitionSet n p.2 ×ˢ s)
      / ν p.1 (countablePartitionSet n p.2)) ∘ (fun x ↦ (a, x)))

Premises used: SProd.sprod, Measurable, MeasurableSpace.countablePartitionSet, Function.comp, HDiv.hDiv, Prod.mk, Prod.fst, Prod.snd, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this : IsFiniteKernel κ
hu_meas : MeasurableSet u
⊢ Measurable.{u_3, 0} (α := γ) (β := ℝ≥0∞)
    ((fun (p : α × γ) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) p.1 : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (countablePartitionSet n p.2 ×ˢ s) :
            ℝ≥0∞)
          ((((ν : (a : α) → Measure γ) p.1 : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n p.2) : ℝ≥0∞)) ∘
      fun (x : γ) ↦ (a, x))

Tactic:
(measurable_densityProcess_aux κ ν n hs).comp measurable_prodMk_left

Premises used: Measurable.comp, ProbabilityTheory.Kernel.measurable_densityProcess_aux, measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this : IsFiniteKernel κ
hu_meas : MeasurableSet u
⊢ Measurable.{u_3, 0} (α := γ) (β := ℝ≥0∞)
    ((fun (p : α × γ) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) p.1 : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (countablePartitionSet n p.2 ×ˢ s) :
            ℝ≥0∞)
          ((((ν : (a : α) → Measure γ) p.1 : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n p.2) : ℝ≥0∞)) ∘
      fun (x : γ) ↦ (a, x))

Tactic:
exact (measurable_densityProcess_aux κ ν n hs).comp measurable_prodMk_left

Premises used: Measurable.comp, ProbabilityTheory.Kernel.measurable_densityProcess_aux, measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this : IsFiniteKernel κ
hu_meas : MeasurableSet u
⊢ ∀ᵐ (x : γ) ∂Measure.restrict ((ν : (a : α) → Measure γ) a) u,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n x ×ˢ s) :
          ℝ≥0∞)
        ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞) <
      ∞

Tactic:
ae_of_all _ (fun x ↦ ?_)

Premises used: MeasureTheory.ae_of_all