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 α γ
s : Set β
hs : MeasurableSet s
a : α
⊢ Measurable (β := ℝ) fun (x : γ) ↦ κ.density ν a x s
have change : Measurable.{u_3, 0} (α := γ) (β := ℝ) ((fun (p : α × γ) ↦ κ.density ν p.1 p.2 s) ∘ fun (x : γ) ↦ (a, x))
Tactic: change Measurable ((fun (p : α × γ) ↦ density κ ν p.1 p.2 s) ∘ (fun x ↦ (a, x)))
-- 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 ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ κ.density ν a x s ≤ κ.density ν a x s'
have refine_1 : EventuallyLE (β := ℝ) atTop (fun (n : ℕ) ↦ κ.densityProcess ν n a x s) fun (n : ℕ) ↦ κ.densityProcess ν n a x s'
Tactic: refine limsup_le_limsup ?_ ?_ ?_
-- 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 ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
refine_1 :
  EventuallyLE (β := ℝ) atTop (fun (n : ℕ) ↦ κ.densityProcess ν n a x s) fun (n : ℕ) ↦ κ.densityProcess ν n a x s'
⊢ κ.density ν a x s ≤ κ.density ν a x s'
have refine_2 : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ κ.densityProcess ν n a x s
Tactic: refine limsup_le_limsup ?_ ?_ ?_
-- 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 ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
refine_1 :
  EventuallyLE (β := ℝ) atTop (fun (n : ℕ) ↦ κ.densityProcess ν n a x s) fun (n : ℕ) ↦ κ.densityProcess ν n a x s'
refine_2 : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ κ.densityProcess ν n a x s
⊢ κ.density ν a x s ≤ κ.density ν a x s'
have refine_3 : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ κ.densityProcess ν n a x s'
Tactic: refine limsup_le_limsup ?_ ?_ ?_
-- 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 ≤ ν
a : α
x : γ
s : Set β
⊢ 0 ≤ κ.density ν a x s
have refine_1 : ∃ᶠ (i : ℕ) in atTop, 0 ≤ κ.densityProcess ν i a x s
Tactic: refine le_limsup_of_frequently_le ?_ ?_
-- 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 ≤ ν
a : α
x : γ
s : Set β
refine_1 : ∃ᶠ (i : ℕ) in atTop, 0 ≤ κ.densityProcess ν i a x s
⊢ 0 ≤ κ.density ν a x s
have refine_2 : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ κ.densityProcess ν n a x s
Tactic: refine le_limsup_of_frequently_le ?_ ?_
-- 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 ≤ ν
a : α
x : γ
s : Set β
⊢ κ.density ν a x s ≤ 1
have refine_1 : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ κ.densityProcess ν n a x s
Tactic: refine limsup_le_of_le ?_ ?_
-- 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 ≤ ν
a : α
x : γ
s : Set β
refine_1 : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ κ.densityProcess ν n a x s
⊢ κ.density ν a x s ≤ 1
have refine_2 : ∀ᶠ (n : ℕ) in atTop, κ.densityProcess ν n a x s ≤ 1
Tactic: refine limsup_le_of_le ?_ ?_
-- 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 ≤ ν
a : α
s : Set β
⊢ @eLpNorm _ ℝ _ mγ (fun (x : γ) ↦ κ.density ν a x s) 1 ((ν : (a : α) → Measure γ) a) ≤
    (((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ
have refine_1 : ∀ (t : γ), ‖κ.density ν a t s‖ ≤ 1
Tactic: refine (eLpNorm_le_of_ae_bound (C := 1) (ae_of_all _ (fun t ↦ ?_))).trans ?_
-- 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 ≤ ν
a : α
s : Set β
refine_1 : ∀ (t : γ), ‖κ.density ν a t s‖ ≤ 1
⊢ @eLpNorm _ ℝ _ mγ (fun (x : γ) ↦ κ.density ν a x s) 1 ((ν : (a : α) → Measure γ) a) ≤
    (((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ
have 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
Tactic: refine (eLpNorm_le_of_ae_bound (C := 1) (ae_of_all _ (fun t ↦ ?_))).trans ?_
-- 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 ν
a : α
s : Set β
hs : MeasurableSet s
⊢ @Integrable ℝ _ _ _ mγ (fun (x : γ) ↦ κ.density ν a x s) ((ν : (a : α) → Measure γ) a)
have rw : MemLp (ε := ℝ) (m0 := mγ) (fun (x : γ) ↦ κ.density ν a x s) 1 ((ν : (a : α) → Measure γ) a)
Tactic: rw [← memLp_one_iff_integrable]
-- 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 ν
a : α
s : Set β
hs : MeasurableSet s
⊢ MemLp (ε := ℝ) (m0 := mγ) (fun (x : γ) ↦ κ.density ν a x s) 1 ((ν : (a : α) → Measure γ) a)
have refine_1 : Measurable (β := ℝ) fun (x : γ) ↦ κ.density ν a x s
Tactic: refine ⟨Measurable.aestronglyMeasurable ?_, ?_⟩
-- 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 ν
a : α
s : Set β
hs : MeasurableSet s
refine_1 : Measurable (β := ℝ) fun (x : γ) ↦ κ.density ν a x s
⊢ MemLp (ε := ℝ) (m0 := mγ) (fun (x : γ) ↦ κ.density ν a x s) 1 ((ν : (a : α) → Measure γ) a)
have refine_2 : @eLpNorm _ ℝ _ mγ (fun (x : γ) ↦ κ.density ν a x s) 1 ((ν : (a : α) → Measure γ) a) < ∞
Tactic: refine ⟨Measurable.aestronglyMeasurable ?_, ?_⟩
-- 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 ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
⊢ Tendsto (β := ℝ)
    (fun (i : ℕ) ↦
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.densityProcess ν i a x s)
    atTop (𝓝 (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s))
have refine : Tendsto (β := ℝ≥0∞)
  (fun (i : ℕ) ↦
    @eLpNorm _ _ _ mγ
      (HSub.hSub (α := γ → ℝ) ((fun (i : ℕ) (x : γ) ↦ κ.densityProcess ν i a x s) i) fun (x : γ) ↦ κ.density ν a x s) 1
      ((ν : (a : α) → Measure γ) a))
  atTop (𝓝 0)
Tactic: refine tendsto_setIntegral_of_L1' (μ := ν a) (fun x ↦ density κ ν a x s)
    (integrable_density hκν a hs).aestronglyMeasurable
    (F := fun i x ↦ densityProcess κ ν i a x s) (l := atTop)
    (Eventually.of_forall (fun n ↦ integrable_densityProcess hκν _ _ hs)) ?_ A
-- 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 ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
⊢ Tendsto (β := ℝ≥0∞)
    (fun (i : ℕ) ↦
      @eLpNorm _ _ _ mγ
        (HSub.hSub (α := γ → ℝ) ((fun (i : ℕ) (x : γ) ↦ κ.densityProcess ν i a x s) i) fun (x : γ) ↦ κ.density ν a x s)
        1 ((ν : (a : α) → Measure γ) a))
    atTop (𝓝 0)
have refine : ∀ (n : ℕ),
  @eLpNorm _ _ _ mγ
      (HSub.hSub (α := (x : γ) → ℝ) (fun (x : γ) ↦ κ.densityProcess ν n a x s)
        (Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
          ((ν : (a : α) → Measure γ) a)))
      1 ((ν : (a : α) → Measure γ) a) =
    @eLpNorm _ _ _ mγ
      (HSub.hSub (α := γ → ℝ) ((fun (i : ℕ) (x : γ) ↦ κ.densityProcess ν i a x s) n) fun (x : γ) ↦ κ.density ν a x s) 1
      ((ν : (a : α) → Measure γ) a)
Tactic: refine (tendsto_congr fun n ↦ ?_).mp (tendsto_eLpNorm_one_densityProcess_limitProcess hκν a hs)
-- 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 ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
n : ℕ
⊢ @eLpNorm _ _ _ mγ
      (HSub.hSub (α := (x : γ) → ℝ) (fun (x : γ) ↦ κ.densityProcess ν n a x s)
        (Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
          ((ν : (a : α) → Measure γ) a)))
      1 ((ν : (a : α) → Measure γ) a) =
    @eLpNorm _ _ _ mγ
      (HSub.hSub (α := γ → ℝ) ((fun (i : ℕ) (x : γ) ↦ κ.densityProcess ν i a x s) n) fun (x : γ) ↦ κ.density ν a x s) 1
      ((ν : (a : α) → Measure γ) a)
have refine : HSub.hSub (α := (x : γ) → ℝ) (fun (x : γ) ↦ κ.densityProcess ν n a x s)
    (Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
      ((ν : (a : α) → Measure γ) a)) =ᶠ[ae (F := Measure γ) ((ν : (a : α) → Measure γ) a : Measure γ)]
  HSub.hSub (α := γ → ℝ) ((fun (i : ℕ) (x : γ) ↦ κ.densityProcess ν i a x s) n) fun (x : γ) ↦ κ.density ν a x s
Tactic: refine eLpNorm_congr_ae ?_
-- 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
A : Set γ
hA : MeasurableSet A
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)
have suffices : Eq (α := ℝ) (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s)
  (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.densityProcess ν n a x s)
Tactic: suffices ∫ x in A, density κ ν a x s ∂(ν a) = ∫ x in A, densityProcess κ ν n a x s ∂(ν a) by
    exact this ▸ setIntegral_densityProcess hκν _ _ hs hA
-- 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
A : Set γ
hA : MeasurableSet A
this :
  Eq (α := ℝ) (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s)
    (limsup
      (fun (i : ℕ) ↦
        @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦
          κ.densityProcess ν i a x s)
      atTop)
⊢ Eq (α := ℝ) (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s)
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.densityProcess ν n a x s)
have rw : ∀ᶠ (a_1 : ℕ) in atTop,
  Eq (α := ℝ)
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.densityProcess ν a_1 a x s)
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.densityProcess ν n a x s)
Tactic: rw [this, ← limsup_const (α := ℕ) (f := atTop) (∫ x in A, densityProcess κ ν n a x s ∂(ν a)),
      limsup_congr]
-- 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
A : Set γ
hA : MeasurableSet A
this :
  Eq (α := ℝ) (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s)
    (limsup
      (fun (i : ℕ) ↦
        @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦
          κ.densityProcess ν i a x s)
      atTop)
⊢ ∀ᶠ (a_1 : ℕ) in atTop,
    Eq (α := ℝ)
      (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦
        κ.densityProcess ν a_1 a x s)
      (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.densityProcess ν n a x s)
have simp : ∃ (a_1 : ℕ),
  ∀ b ≥ a_1,
    Eq (α := ℝ)
      (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.densityProcess ν b a x s)
      (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.densityProcess ν n a x s)
Tactic: simp only [eventually_atTop]
-- 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
A : Set γ
hA : MeasurableSet A
this :
  Eq (α := ℝ) (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s)
    (limsup
      (fun (i : ℕ) ↦
        @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦
          κ.densityProcess ν i a x s)
      atTop)
⊢ ∃ (a_1 : ℕ),
    ∀ b ≥ a_1,
      Eq (α := ℝ)
        (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦
          κ.densityProcess ν b a x s)
        (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦
          κ.densityProcess ν n a x s)
have refine : ∀ (m : ℕ) (hnm : m ≥ n),
  Eq (α := ℝ)
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.densityProcess ν m a x s)
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.densityProcess ν n a x s)
Tactic: refine ⟨n, fun m hnm ↦ ?_⟩
-- 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
A : Set γ
hA : MeasurableSet A
this :
  Eq (α := ℝ) (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s)
    (limsup
      (fun (i : ℕ) ↦
        @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦
          κ.densityProcess ν i a x s)
      atTop)
m : ℕ
hnm : m ≥ n
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.densityProcess ν m a x s)
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.densityProcess ν n a x s)
have rw : Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s) =
  @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.densityProcess ν n a x s
Tactic: rw [setIntegral_densityProcess_of_le hκν hnm _ hs hA,
      setIntegral_densityProcess hκν _ _ hs hA]
-- 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
A : Set γ
hA : MeasurableSet A
this :
  Eq (α := ℝ) (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s)
    (limsup
      (fun (i : ℕ) ↦
        @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦
          κ.densityProcess ν i a x s)
      atTop)
m : ℕ
hnm : m ≥ n
rw :
  Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s) =
    @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.densityProcess ν n a x s
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.densityProcess ν m a x s)
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.densityProcess ν n a x s)
have rw₁ : Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s) =
  Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)
Tactic: rw [setIntegral_densityProcess_of_le hκν hnm _ hs hA,
      setIntegral_densityProcess hκν _ _ hs hA]
-- 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
A : Set γ
hA : MeasurableSet A
⊢ Eq (α := ℝ) (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s)
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.densityProcess ν n a x s)
have suffices : Eq (α := ℝ) (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s)
  (limsup
    (fun (i : ℕ) ↦
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.densityProcess ν i a x s)
    atTop)
Tactic: suffices ∫ x in A, density κ ν a x s ∂(ν a)
      = limsup (fun i ↦ ∫ x in A, densityProcess κ ν i a x s ∂(ν a)) atTop by
    rw [this, ← limsup_const (α := ℕ) (f := atTop) (∫ x in A, densityProcess κ ν n a x s ∂(ν a)),
      limsup_congr]
    simp only [eventually_atTop]
    refine ⟨n, fun m hnm ↦ ?_⟩
    rw [setIntegral_densityProcess_of_le hκν hnm _ hs hA,
      setIntegral_densityProcess hκν _ _ hs hA]
-- 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 α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
⊢ Eq (α := ℝ) (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s)
    (limsup
      (fun (i : ℕ) ↦
        @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦
          κ.densityProcess ν i a x s)
      atTop)
have h : Tendsto (β := ℝ)
  (fun (i : ℕ) ↦
    @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.densityProcess ν i a x s)
  atTop (𝓝 (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s))
Tactic: have h := tendsto_setIntegral_densityProcess hκν a hs A
-- 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
A : Set γ
hA : MeasurableSet A
h :
  Tendsto (β := ℝ)
    (fun (i : ℕ) ↦
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.densityProcess ν i a x s)
    atTop (𝓝 (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s))
⊢ Eq (α := ℝ) (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s)
    (limsup
      (fun (i : ℕ) ↦
        @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦
          κ.densityProcess ν i a x s)
      atTop)
have rw : Eq (α := ℝ) (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s)
  (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s)
Tactic: rw [h.limsup_eq]
-- 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 ν
a : α
s : Set β
hs : MeasurableSet s
⊢ (@integral _ _ _ _ mγ ((ν : (a : α) → Measure γ) a) fun (x : γ) ↦ κ.density ν 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 : γ) ↦ κ.density ν a x s) =
  Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)
Tactic: rw [← setIntegral_univ, setIntegral_density_of_measurableSet hκν 0 a hs MeasurableSet.univ]