awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
h_disj : Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))
rw :
  Eq (α := ℝ)
    (∑' (n_1 : (↑(↑S : Set (Set γ)) : Type u_3)),
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (↑n_1 : Set γ)) fun (x : γ) ↦
        κ.densityProcess ν n a x s)
    (∑' (a_1 : (↑(↑S : Set (Set γ)) : Type u_3)),
      ENNReal.toReal
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑a_1 : Set γ) ×ˢ s)))
⊢ (@integral _ _ _ _ mγ
      (Measure.restrict ((ν : (a : α) → Measure γ) a) (⋃ (i : (↑(↑S : Set (Set γ)) : Type u_3)), (↑i : Set γ)))
      fun (x : γ) ↦ κ.densityProcess ν n a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
      (SProd.sprod (α := Set γ) (⋃ (i : (↑(↑S : Set (Set γ)) : Type u_3)), (↑i : Set γ)) s)
have hn : Pairwise.{u_3} (α := (↑(↑S : Set (Set γ)) : Type u_3))
  (Function.onFun (β := Set (γ × β)) Disjoint fun (i : (↑(↑S : Set (Set γ)) : Type u_3)) ↦ (↑i : Set γ) ×ˢ s)
Tactic: rw [integral_iUnion, iUnion_prod_const, measureReal_def, measure_iUnion,
      ENNReal.tsum_toReal_eq (fun _ ↦ measure_ne_top _ _)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
h_disj : Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))
rw :
  Eq (α := ℝ)
    (∑' (n_1 : (↑(↑S : Set (Set γ)) : Type u_3)),
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (↑n_1 : Set γ)) fun (x : γ) ↦
        κ.densityProcess ν n a x s)
    (∑' (a_1 : (↑(↑S : Set (Set γ)) : Type u_3)),
      ENNReal.toReal
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑a_1 : Set γ) ×ˢ s)))
hn :
  Pairwise.{u_3} (α := (↑(↑S : Set (Set γ)) : Type u_3))
    (Function.onFun (β := Set (γ × β)) Disjoint fun (i : (↑(↑S : Set (Set γ)) : Type u_3)) ↦ (↑i : Set γ) ×ˢ s)
⊢ (@integral _ _ _ _ mγ
      (Measure.restrict ((ν : (a : α) → Measure γ) a) (⋃ (i : (↑(↑S : Set (Set γ)) : Type u_3)), (↑i : Set γ)))
      fun (x : γ) ↦ κ.densityProcess ν n a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
      (SProd.sprod (α := Set γ) (⋃ (i : (↑(↑S : Set (Set γ)) : Type u_3)), (↑i : Set γ)) s)
have h : ∀ (i : (↑(↑S : Set (Set γ)) : Type u_3)), MeasurableSet ((↑i : Set γ) ×ˢ s)
Tactic: rw [integral_iUnion, iUnion_prod_const, measureReal_def, measure_iUnion,
      ENNReal.tsum_toReal_eq (fun _ ↦ measure_ne_top _ _)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
h_disj : Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))
rw :
  Eq (α := ℝ)
    (∑' (n_1 : (↑(↑S : Set (Set γ)) : Type u_3)),
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (↑n_1 : Set γ)) fun (x : γ) ↦
        κ.densityProcess ν n a x s)
    (∑' (a_1 : (↑(↑S : Set (Set γ)) : Type u_3)),
      ENNReal.toReal
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑a_1 : Set γ) ×ˢ s)))
hn :
  Pairwise.{u_3} (α := (↑(↑S : Set (Set γ)) : Type u_3))
    (Function.onFun (β := Set (γ × β)) Disjoint fun (i : (↑(↑S : Set (Set γ)) : Type u_3)) ↦ (↑i : Set γ) ×ˢ s)
h : ∀ (i : (↑(↑S : Set (Set γ)) : Type u_3)), MeasurableSet ((↑i : Set γ) ×ˢ s)
⊢ (@integral _ _ _ _ mγ
      (Measure.restrict ((ν : (a : α) → Measure γ) a) (⋃ (i : (↑(↑S : Set (Set γ)) : Type u_3)), (↑i : Set γ)))
      fun (x : γ) ↦ κ.densityProcess ν n a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
      (SProd.sprod (α := Set γ) (⋃ (i : (↑(↑S : Set (Set γ)) : Type u_3)), (↑i : Set γ)) s)
have hm : ∀ (i : (↑(↑S : Set (Set γ)) : Type u_3)), MeasurableSet (↑i : Set γ)
Tactic: rw [integral_iUnion, iUnion_prod_const, measureReal_def, measure_iUnion,
      ENNReal.tsum_toReal_eq (fun _ ↦ measure_ne_top _ _)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
h_disj : Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))
rw :
  Eq (α := ℝ)
    (∑' (n_1 : (↑(↑S : Set (Set γ)) : Type u_3)),
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (↑n_1 : Set γ)) fun (x : γ) ↦
        κ.densityProcess ν n a x s)
    (∑' (a_1 : (↑(↑S : Set (Set γ)) : Type u_3)),
      ENNReal.toReal
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑a_1 : Set γ) ×ˢ s)))
hn :
  Pairwise.{u_3} (α := (↑(↑S : Set (Set γ)) : Type u_3))
    (Function.onFun (β := Set (γ × β)) Disjoint fun (i : (↑(↑S : Set (Set γ)) : Type u_3)) ↦ (↑i : Set γ) ×ˢ s)
h : ∀ (i : (↑(↑S : Set (Set γ)) : Type u_3)), MeasurableSet ((↑i : Set γ) ×ˢ s)
hm : ∀ (i : (↑(↑S : Set (Set γ)) : Type u_3)), MeasurableSet (↑i : Set γ)
⊢ (@integral _ _ _ _ mγ
      (Measure.restrict ((ν : (a : α) → Measure γ) a) (⋃ (i : (↑(↑S : Set (Set γ)) : Type u_3)), (↑i : Set γ)))
      fun (x : γ) ↦ κ.densityProcess ν n a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
      (SProd.sprod (α := Set γ) (⋃ (i : (↑(↑S : Set (Set γ)) : Type u_3)), (↑i : Set γ)) s)
have hd : Pairwise.{u_3} (α := (↑(↑S : Set (Set γ)) : Type u_3))
  (Disjoint on Subtype.val (p := fun (x : Set γ) ↦ x ∈ (↑S : Set (Set γ))))
Tactic: rw [integral_iUnion, iUnion_prod_const, measureReal_def, measure_iUnion,
      ENNReal.tsum_toReal_eq (fun _ ↦ measure_ne_top _ _)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
h_disj : Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))
rw :
  Eq (α := ℝ)
    (∑' (n_1 : (↑(↑S : Set (Set γ)) : Type u_3)),
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (↑n_1 : Set γ)) fun (x : γ) ↦
        κ.densityProcess ν n a x s)
    (∑' (a_1 : (↑(↑S : Set (Set γ)) : Type u_3)),
      ENNReal.toReal
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑a_1 : Set γ) ×ˢ s)))
hn :
  Pairwise.{u_3} (α := (↑(↑S : Set (Set γ)) : Type u_3))
    (Function.onFun (β := Set (γ × β)) Disjoint fun (i : (↑(↑S : Set (Set γ)) : Type u_3)) ↦ (↑i : Set γ) ×ˢ s)
h : ∀ (i : (↑(↑S : Set (Set γ)) : Type u_3)), MeasurableSet ((↑i : Set γ) ×ˢ s)
hm : ∀ (i : (↑(↑S : Set (Set γ)) : Type u_3)), MeasurableSet (↑i : Set γ)
hd :
  Pairwise.{u_3} (α := (↑(↑S : Set (Set γ)) : Type u_3))
    (Disjoint on Subtype.val (p := fun (x : Set γ) ↦ x ∈ (↑S : Set (Set γ))))
⊢ (@integral _ _ _ _ mγ
      (Measure.restrict ((ν : (a : α) → Measure γ) a) (⋃ (i : (↑(↑S : Set (Set γ)) : Type u_3)), (↑i : Set γ)))
      fun (x : γ) ↦ κ.densityProcess ν n a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
      (SProd.sprod (α := Set γ) (⋃ (i : (↑(↑S : Set (Set γ)) : Type u_3)), (↑i : Set γ)) s)
have hfi : IntegrableOn (ε := ℝ) (mα := mγ) (fun (x : γ) ↦ κ.densityProcess ν n a x s)
  (⋃ (i : (↑(↑S : Set (Set γ)) : Type u_3)), (↑i : Set γ)) ((ν : (a : α) → Measure γ) a)
Tactic: rw [integral_iUnion, iUnion_prod_const, measureReal_def, measure_iUnion,
      ENNReal.tsum_toReal_eq (fun _ ↦ measure_ne_top _ _)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
h_disj : Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))
⊢ Eq (α := ℝ)
    (∑' (n_1 : (↑(↑S : Set (Set γ)) : Type u_3)),
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (↑n_1 : Set γ)) fun (x : γ) ↦
        κ.densityProcess ν n a x s)
    (∑' (a_1 : (↑(↑S : Set (Set γ)) : Type u_3)),
      ENNReal.toReal
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑a_1 : Set γ) ×ˢ s)))
have e_f : ∀ (u : (↑(↑S : Set (Set γ)) : Type u_3)),
  (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (↑u : Set γ)) fun (x : γ) ↦
      κ.densityProcess ν n a x s) =
    ENNReal.toReal
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑u : Set γ) ×ˢ s))
Tactic: congr with u
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
h_disj : Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))
u : (↑(↑S : Set (Set γ)) : Type u_3)
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (↑u : Set γ)) fun (x : γ) ↦
      κ.densityProcess ν n a x s) =
    ENNReal.toReal
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑u : Set γ) ×ˢ s))
have e_f : Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) ((↑u : Set γ) ×ˢ s) =
  ENNReal.toReal
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑u : Set γ) ×ˢ s))
Tactic: rw [setIntegral_densityProcess_of_mem hκν _ _ hs (hS_subset (by simp))]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
h_disj : Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))
u v : (↑(↑S : Set (Set γ)) : Type u_3)
huv : u ≠ v
⊢ Function.onFun (β := Set (γ × β)) Disjoint (fun (i : (↑(↑S : Set (Set γ)) : Type u_3)) ↦ (↑i : Set γ) ×ˢ s) u v
have hn : Disjoint (↑u : Set γ) (↑v : Set γ) ∨ s = ⊥
Tactic: simp only [Finset.coe_sort_coe, Set.disjoint_prod, disjoint_self]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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
⊢ (@integral _ _ _ _ mγ ((ν : (a : α) → Measure γ) a) fun (x : γ) ↦ κ.densityProcess ν n a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)
have rw : (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) univ) fun (x : γ) ↦ κ.densityProcess ν n a x s) =
  Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)
Tactic: rw [← setIntegral_univ, setIntegral_densityProcess hκν _ _ hs MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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 :
  (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) univ) fun (x : γ) ↦
      κ.densityProcess ν n a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)
⊢ (@integral _ _ _ _ mγ ((ν : (a : α) → Measure γ) a) fun (x : γ) ↦ κ.densityProcess ν n a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)
have rw₁ : Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s) =
  Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)
Tactic: rw [← setIntegral_univ, setIntegral_densityProcess hκν _ _ hs MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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 ν
i j : ℕ
hij : i ≤ j
a : α
s : Set β
hs : MeasurableSet s
⊢ (ae (F := Measure γ) ((ν : (a : α) → Measure γ) a : Measure γ)).EventuallyEq (β := ℝ)
    (condExp ((↑(countableFiltration γ) : ℕ → MeasurableSpace γ) i) (m₀ := mγ) ((ν : (a : α) → Measure γ) a)
      fun (x : γ) ↦ κ.densityProcess ν j a x s)
    fun (x : γ) ↦ κ.densityProcess ν i a x s
have refine_1 : @Integrable ℝ _ _ _ mγ (fun (x : γ) ↦ κ.densityProcess ν j a x s) ((ν : (a : α) → Measure γ) a)
Tactic: refine (ae_eq_condExp_of_forall_setIntegral_eq ?_ ?_ ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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 ν
i j : ℕ
hij : i ≤ j
a : α
s : Set β
hs : MeasurableSet s
refine_1 : @Integrable ℝ _ _ _ mγ (fun (x : γ) ↦ κ.densityProcess ν j a x s) ((ν : (a : α) → Measure γ) a)
⊢ (ae (F := Measure γ) ((ν : (a : α) → Measure γ) a : Measure γ)).EventuallyEq (β := ℝ)
    (condExp ((↑(countableFiltration γ) : ℕ → MeasurableSpace γ) i) (m₀ := mγ) ((ν : (a : α) → Measure γ) a)
      fun (x : γ) ↦ κ.densityProcess ν j a x s)
    fun (x : γ) ↦ κ.densityProcess ν i a x s
have refine_2 : ∀ (s_1 : Set γ),
  MeasurableSet s_1 →
    LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
      IntegrableOn (ε := ℝ) (mα := mγ) (fun (x : γ) ↦ κ.densityProcess ν i a x s) s_1 ((ν : (a : α) → Measure γ) a)
Tactic: refine (ae_eq_condExp_of_forall_setIntegral_eq ?_ ?_ ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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 ν
i j : ℕ
hij : i ≤ j
a : α
s : Set β
hs : MeasurableSet s
refine_1 : @Integrable ℝ _ _ _ mγ (fun (x : γ) ↦ κ.densityProcess ν j a x s) ((ν : (a : α) → Measure γ) a)
refine_2 :
  ∀ (s_1 : Set γ),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (ε := ℝ) (mα := mγ) (fun (x : γ) ↦ κ.densityProcess ν i a x s) s_1 ((ν : (a : α) → Measure γ) a)
⊢ (ae (F := Measure γ) ((ν : (a : α) → Measure γ) a : Measure γ)).EventuallyEq (β := ℝ)
    (condExp ((↑(countableFiltration γ) : ℕ → MeasurableSpace γ) i) (m₀ := mγ) ((ν : (a : α) → Measure γ) a)
      fun (x : γ) ↦ κ.densityProcess ν j a x s)
    fun (x : γ) ↦ κ.densityProcess ν i a x s
have refine_3 : ∀ (s_1 : Set γ),
  MeasurableSet s_1 →
    LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
      Eq (α := ℝ)
        (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) s_1) fun (x : γ) ↦
          κ.densityProcess ν i a x s)
        (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) s_1) fun (x : γ) ↦
          κ.densityProcess ν j a x s)
Tactic: refine (ae_eq_condExp_of_forall_setIntegral_eq ?_ ?_ ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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 ν
i j : ℕ
hij : i ≤ j
a : α
s : Set β
hs : MeasurableSet s
refine_1 : @Integrable ℝ _ _ _ mγ (fun (x : γ) ↦ κ.densityProcess ν j a x s) ((ν : (a : α) → Measure γ) a)
refine_2 :
  ∀ (s_1 : Set γ),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (ε := ℝ) (mα := mγ) (fun (x : γ) ↦ κ.densityProcess ν i a x s) s_1 ((ν : (a : α) → Measure γ) a)
refine_3 :
  ∀ (s_1 : Set γ),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ)
          (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) s_1) fun (x : γ) ↦
            κ.densityProcess ν i a x s)
          (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) s_1) fun (x : γ) ↦
            κ.densityProcess ν j a x s)
⊢ (ae (F := Measure γ) ((ν : (a : α) → Measure γ) a : Measure γ)).EventuallyEq (β := ℝ)
    (condExp ((↑(countableFiltration γ) : ℕ → MeasurableSpace γ) i) (m₀ := mγ) ((ν : (a : α) → Measure γ) a)
      fun (x : γ) ↦ κ.densityProcess ν j a x s)
    fun (x : γ) ↦ κ.densityProcess ν i a x s
have refine_4 : AEStronglyMeasurable (β := ℝ) (m₀ := mγ) (fun (x : γ) ↦ κ.densityProcess ν i a x s) ((ν : (a : α) → Measure γ) a)
Tactic: refine (ae_eq_condExp_of_forall_setIntegral_eq ?_ ?_ ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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 ν
i j : ℕ
hij : i ≤ j
a : α
s : Set β
hs : MeasurableSet s
x : Set γ
hx : MeasurableSet x
h : LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) x : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) x) fun (x : γ) ↦ κ.densityProcess ν i a x s)
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) x) fun (x : γ) ↦ κ.densityProcess ν j a x s)
have refine_3 : Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (x ×ˢ s) =
  @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) x) fun (x : γ) ↦ κ.densityProcess ν j a x s
Tactic: rw [setIntegral_densityProcess hκν i a hs hx,
      setIntegral_densityProcess_of_le hκν hij a hs hx]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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 ν
i j : ℕ
hij : i ≤ j
a : α
s : Set β
hs : MeasurableSet s
x : Set γ
hx : MeasurableSet x
h : LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) x : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_3 :
  Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (x ×ˢ s) =
    @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) x) fun (x : γ) ↦ κ.densityProcess ν j a x s
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) x) fun (x : γ) ↦ κ.densityProcess ν i a x s)
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) x) fun (x : γ) ↦ κ.densityProcess ν j a x s)
have refine_3₁ : Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (x ×ˢ s) =
  Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (x ×ˢ s)
Tactic: rw [setIntegral_densityProcess hκν i a hs hx,
      setIntegral_densityProcess_of_le hκν hij a hs hx]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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 s' : Set β
h : s ⊆ s'
⊢ (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 ≤
    (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
have inl : ∀
  (h₀ :
    Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)),
  (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 ≤
    (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
Tactic: obtain h₀ | h₀ := eq_or_ne (ν a (countablePartitionSet n x)) 0