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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  ¬Eq (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Tendsto
    (fun (m : ℕ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n x ×ˢ seq m) :
          ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞))
    atTop
    (𝓝
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
          ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)))
have neg : Tendsto (β := ℝ≥0∞)
  (fun (m : ℕ) ↦
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ seq m) :
      ℝ≥0∞))
  atTop
  (𝓝
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (β := Set β) (countablePartitionSet n x) univ)) :
    Filter ℝ≥0∞)
Tactic: refine ENNReal.Tendsto.div_const ?_ ?_
-- 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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  ¬Eq (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
neg :
  Tendsto (β := ℝ≥0∞)
    (fun (m : ℕ) ↦
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ seq m) :
        ℝ≥0∞))
    atTop
    (𝓝
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (β := Set β) (countablePartitionSet n x) univ)) :
      Filter ℝ≥0∞)
⊢ Tendsto
    (fun (m : ℕ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n x ×ˢ seq m) :
          ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞))
    atTop
    (𝓝
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
          ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)))
have neg₁ : Ne (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
      ℝ≥0∞)
    (0 : ℝ≥0∞) ∨
  Ne (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ENNReal.Tendsto.div_const ?_ ?_
-- 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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  ¬Eq (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (m : ℕ) ↦
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ seq m) :
        ℝ≥0∞))
    atTop
    (𝓝
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (β := Set β) (countablePartitionSet n x) univ)) :
      Filter ℝ≥0∞)
have h : SProd.sprod (β := Set β) (countablePartitionSet n x) univ = ⋃ (n_1 : ℕ), countablePartitionSet n x ×ˢ seq n_1
Tactic: convert! tendsto_measure_iUnion_atTop (monotone_const.set_prod hseq)
-- 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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  ¬Eq (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ SProd.sprod (β := Set β) (countablePartitionSet n x) univ = ⋃ (n_1 : ℕ), countablePartitionSet n x ×ˢ seq n_1
have h : SProd.sprod (β := Set β) (countablePartitionSet n x) univ =
  SProd.sprod (β := Set β) (countablePartitionSet n x) (⋃ (i : ℕ), seq i)
Tactic: rw [← prod_iUnion, hseq_iUnion]
-- 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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  ¬Eq (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
h :
  SProd.sprod (β := Set β) (countablePartitionSet n x) univ =
    SProd.sprod (β := Set β) (countablePartitionSet n x) (⋃ (i : ℕ), seq i)
⊢ SProd.sprod (β := Set β) (countablePartitionSet n x) univ = ⋃ (n_1 : ℕ), countablePartitionSet n x ×ˢ seq n_1
have h₁ : SProd.sprod (β := Set β) (countablePartitionSet n x) univ = SProd.sprod (β := Set β) (countablePartitionSet n x) univ
Tactic: rw [← prod_iUnion, hseq_iUnion]
-- 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 α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
⊢ ∀ᵐ (x : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ),
    Tendsto (β := ℝ) (fun (m : ℕ) ↦ κ.densityProcess κ.fst n a x (seq m)) atTop (𝓝 1)
have h : ∀ (x : γ) (hx : κ.densityProcess κ.fst n a x univ = 1),
  Tendsto (β := ℝ) (fun (m : ℕ) ↦ κ.densityProcess κ.fst n a x (seq m)) atTop (𝓝 1)
Tactic: filter_upwards [densityProcess_fst_univ_ae κ n a] with x 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 α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
x : γ
hx : κ.densityProcess κ.fst n a x univ = 1
⊢ Tendsto (β := ℝ) (fun (m : ℕ) ↦ κ.densityProcess κ.fst n a x (seq m)) atTop (𝓝 1)
have h : Tendsto (fun (m : ℕ) ↦ κ.densityProcess κ.fst n a x (seq m)) atTop (𝓝 (κ.densityProcess κ.fst n a x univ))
Tactic: rw [← hx]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
⊢ ∀ᵐ (x : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ), κ.density κ.fst a x univ = 1
have h : ∀ (n : ℕ), ∀ᵐ (x : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ), κ.densityProcess κ.fst n a x univ = 1
Tactic: have h := fun n ↦ densityProcess_fst_univ_ae κ n a
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
h : ∀ (n : ℕ), ∀ᵐ (x : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ), κ.densityProcess κ.fst n a x univ = 1
⊢ ∀ᵐ (x : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ), κ.density κ.fst a x univ = 1
have h₁ : ∀ᵐ (a_1 : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ), ∀ (i : ℕ), κ.densityProcess κ.fst i a a_1 univ = 1
Tactic: rw [← ae_all_iff] at h
Cleared hypotheses: h
-- 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 α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
h : ∀ᵐ (a_1 : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ), ∀ (i : ℕ), κ.densityProcess κ.fst i a a_1 univ = 1
⊢ ∀ᵐ (x : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ), κ.density κ.fst a x univ = 1
have h₁ : ∀ (x : γ) (hx : ∀ (i : ℕ), κ.densityProcess κ.fst i a x univ = 1), κ.density κ.fst a x univ = 1
Tactic: filter_upwards [h] with x 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 α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ∀ᵐ (x : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ),
    Tendsto (β := ℝ) (fun (m : ℕ) ↦ κ.density κ.fst a x (seq m)) atTop (𝓝 1)
have refine_1 : ∀ (n : ℕ), @Integrable ℝ _ _ _ mγ (fun (x : γ) ↦ κ.density κ.fst a x (seq n)) ((κ.fst : (a : α) → Measure γ) a)
Tactic: refine tendsto_of_integral_tendsto_of_monotone ?_ (integrable_const _) ?_ ?_ ?_
-- 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 α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
refine_1 :
  ∀ (n : ℕ), @Integrable ℝ _ _ _ mγ (fun (x : γ) ↦ κ.density κ.fst a x (seq n)) ((κ.fst : (a : α) → Measure γ) a)
⊢ ∀ᵐ (x : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ),
    Tendsto (β := ℝ) (fun (m : ℕ) ↦ κ.density κ.fst a x (seq m)) atTop (𝓝 1)
have refine_2 : Tendsto (β := ℝ)
  (fun (i : ℕ) ↦ @integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (a_1 : γ) ↦ κ.density κ.fst a a_1 (seq i))
  atTop (𝓝 (@integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (a : γ) ↦ 1))
Tactic: refine tendsto_of_integral_tendsto_of_monotone ?_ (integrable_const _) ?_ ?_ ?_
-- 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 α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
refine_1 :
  ∀ (n : ℕ), @Integrable ℝ _ _ _ mγ (fun (x : γ) ↦ κ.density κ.fst a x (seq n)) ((κ.fst : (a : α) → Measure γ) a)
refine_2 :
  Tendsto (β := ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (a_1 : γ) ↦ κ.density κ.fst a a_1 (seq i))
    atTop (𝓝 (@integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (a : γ) ↦ 1))
⊢ ∀ᵐ (x : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ),
    Tendsto (β := ℝ) (fun (m : ℕ) ↦ κ.density κ.fst a x (seq m)) atTop (𝓝 1)
have refine_3 : ∀ᵐ (a_1 : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ),
  Monotone (β := ℝ) fun (i : ℕ) ↦ κ.density κ.fst a a_1 (seq i)
Tactic: refine tendsto_of_integral_tendsto_of_monotone ?_ (integrable_const _) ?_ ?_ ?_
-- 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 α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
refine_1 :
  ∀ (n : ℕ), @Integrable ℝ _ _ _ mγ (fun (x : γ) ↦ κ.density κ.fst a x (seq n)) ((κ.fst : (a : α) → Measure γ) a)
refine_2 :
  Tendsto (β := ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (a_1 : γ) ↦ κ.density κ.fst a a_1 (seq i))
    atTop (𝓝 (@integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (a : γ) ↦ 1))
refine_3 :
  ∀ᵐ (a_1 : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ),
    Monotone (β := ℝ) fun (i : ℕ) ↦ κ.density κ.fst a a_1 (seq i)
⊢ ∀ᵐ (x : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ),
    Tendsto (β := ℝ) (fun (m : ℕ) ↦ κ.density κ.fst a x (seq m)) atTop (𝓝 1)
have refine_4 : ∀ᵐ (a_1 : γ) ∂((κ.fst : (a : α) → Measure γ) a : Measure γ), ∀ (i : ℕ), κ.density κ.fst a a_1 (seq i) ≤ 1
Tactic: refine tendsto_of_integral_tendsto_of_monotone ?_ (integrable_const _) ?_ ?_ ?_
-- 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 α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (β := ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (a_1 : γ) ↦ κ.density κ.fst a a_1 (seq i))
    atTop (𝓝 (@integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (a : γ) ↦ 1))
have refine_2 : Tendsto
  (fun (i : ℕ) ↦ @integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (a_1 : γ) ↦ κ.density κ.fst a a_1 (seq i))
  atTop (𝓝 (Measure.real.{u_3} (α := γ) (m := mγ) ((κ.fst : (a : α) → Measure γ) a) univ))
Tactic: rw [MeasureTheory.integral_const, smul_eq_mul, mul_one]
-- 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 α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto
    (fun (i : ℕ) ↦ @integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (a_1 : γ) ↦ κ.density κ.fst a a_1 (seq i))
    atTop (𝓝 (Measure.real.{u_3} (α := γ) (m := mγ) ((κ.fst : (a : α) → Measure γ) a) univ))
have h : Measure.real.{u_3} (α := γ) (m := mγ) ((κ.fst : (a : α) → Measure γ) a) univ =
  Measure.real (α := γ × β) (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) univ
Tactic: convert! tendsto_integral_density_of_monotone (κ := κ) le_rfl a seq hseq hseq_iUnion hseq_meas
-- 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 α (γ × β)
inst_1 : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ENNReal.toReal ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ) =
    ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ)
have h : ENNReal.toReal
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
      {p : γ × β | Membership.mem (γ := Set γ) univ p.1}) =
  ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ)
Tactic: rw [fst_apply' _ _ MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_4 : IsFiniteKernel κ
a : α
s : Set (β × Ω)
hs : MeasurableSet s
| ((((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ((((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← κ.disintegrate κ.condKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_4 : IsFiniteKernel κ
a : α
s : Set (β × Ω)
hs : MeasurableSet s
⊢ ∫⁻ (x : β),
      (((κ.condKernel : (a : α × β) → Measure Ω) (a, x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk x ⁻¹' s) ∂(κ.fst : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) s
have conv_rhs : ∫⁻ (x : β),
    (((κ.condKernel : (a : α × β) → Measure Ω) (a, x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
      (Prod.mk x ⁻¹' s) ∂(κ.fst : (a : α) → Measure β) a =
  (((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) s
Tactic: conv_rhs => rw [← κ.disintegrate κ.condKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_4 : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
    ((((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) (s ×ˢ t) :
      ℝ≥0∞)
have e_a : κ = κ.fst ⊗ₖ κ.condKernel
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (hypothesis)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_4 : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β) in s,
      (((κ.condKernel : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        t ∂(κ.fst : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) (s ×ˢ t)
have this : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
  ((((κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) (s ×ˢ t) :
    ℝ≥0∞)
Tactic: have : κ a (s ×ˢ t) = (Kernel.fst κ ⊗ₖ Kernel.condKernel κ) a (s ×ˢ t) := by
    congr; exact (κ.disintegrate _).symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_4 : IsFiniteKernel κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
| ∫⁻ (x : β × Ω), f x ∂(κ : (a : α) → Measure (β × Ω)) a
have rw : ∫⁻ (x : β × Ω), f x ∂(κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a
Tactic: rw [← κ.disintegrate κ.condKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_4 : IsFiniteKernel κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a =
    ∫⁻ (x : β × Ω), f x ∂(κ : (a : α) → Measure (β × Ω)) a
have conv_rhs : ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a =
  ∫⁻ (x : β × Ω), f x ∂(κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a
Tactic: conv_rhs => rw [← κ.disintegrate κ.condKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_4 : IsFiniteKernel κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a =
    ∫⁻ (x : β × Ω), f x ∂(κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a
have rw : ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a =
  ∫⁻ (b : β), ∫⁻ (c : Ω), f (b, c) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a
Tactic: rw [Kernel.lintegral_compProd _ _ _ hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_4 : IsFiniteKernel κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
| ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂(κ : (a : α) → Measure (β × Ω)) a
have rw : ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂(κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a
Tactic: rw [← κ.disintegrate κ.condKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_4 : IsFiniteKernel κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β) in s,
      ∫⁻ (ω : Ω) in t, f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a =
    ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂(κ : (a : α) → Measure (β × Ω)) a
have conv_rhs : ∫⁻ (b : β) in s,
    ∫⁻ (ω : Ω) in t, f (b, ω) ∂(κ.condKernel : (a : α × β) → Measure Ω) (a, b) ∂(κ.fst : (a : α) → Measure β) a =
  ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂(κ.fst ⊗ₖ κ.condKernel : (a : α) → Measure (β × Ω)) a
Tactic: conv_rhs => rw [← κ.disintegrate κ.condKernel]