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 ≤ ν
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))

Tactic:
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

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.tendsto_setIntegral_of_L1', ProbabilityTheory.Kernel.integrable_densityProcess, Filter.Eventually.of_forall, ProbabilityTheory.Kernel.integrable_density, ProbabilityTheory.Kernel.density
-- 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 ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
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)
⊢ 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:
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

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.tendsto_setIntegral_of_L1', ProbabilityTheory.Kernel.integrable_densityProcess, Filter.Eventually.of_forall, ProbabilityTheory.Kernel.integrable_density, ProbabilityTheory.Kernel.density
-- 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 ν
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)

Tactic:
(tendsto_congr fun n ↦ ?_).mp (tendsto_eLpNorm_one_densityProcess_limitProcess hκν a hs)

Premises used: Filter.tendsto_congr, ProbabilityTheory.Kernel.tendsto_eLpNorm_one_densityProcess_limitProcess, Iff.mp
-- 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 ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
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)
⊢ 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_congr fun n ↦ ?_).mp (tendsto_eLpNorm_one_densityProcess_limitProcess hκν a hs)

Premises used: Filter.tendsto_congr, ProbabilityTheory.Kernel.tendsto_eLpNorm_one_densityProcess_limitProcess, Iff.mp
-- 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 ν
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)

Tactic:
eLpNorm_congr_ae ?_

Premises used: MeasureTheory.eLpNorm_congr_ae
-- 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 ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
n : ℕ
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
⊢ @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 eLpNorm_congr_ae ?_

Premises used: MeasureTheory.eLpNorm_congr_ae
-- 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 ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
n : ℕ
⊢ 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:
EventuallyEq.rfl.sub (density_ae_eq_limitProcess hκν a hs).symm

Premises used: ProbabilityTheory.Kernel.density_ae_eq_limitProcess, Filter.EventuallyEq.rfl, Filter.EventuallyEq.sub, Filter.EventuallyEq.symm
-- 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 ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
n : ℕ
⊢ 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:
exact EventuallyEq.rfl.sub (density_ae_eq_limitProcess hκν a hs).symm

Premises used: ProbabilityTheory.Kernel.density_ae_eq_limitProcess, Filter.EventuallyEq.rfl, Filter.EventuallyEq.sub, Filter.EventuallyEq.symm
-- 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
A : Set γ
hA : MeasurableSet A
this :
  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)
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)

Tactic:
this ▸ setIntegral_densityProcess hκν _ _ hs hA

Premises used: Eq.rec, ProbabilityTheory.Kernel.setIntegral_densityProcess, Eq.symm
-- 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
A : Set γ
hA : MeasurableSet A
this :
  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)
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)

Tactic:
exact this ▸ setIntegral_densityProcess hκν _ _ hs hA
-- 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
A : Set γ
hA : MeasurableSet A
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)
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ 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
-- 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
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)
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)
⊢ 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:
rw [this, ← limsup_const (α := ℕ) (f := atTop) (∫ x in A, densityProcess κ ν n a x s ∂(ν a)),
      limsup_congr]

Premises used: Filter.limsup_const, MeasureTheory.Measure.restrict, ProbabilityTheory.Kernel.densityProcess, MeasureTheory.integral, Filter.limsup_congr, 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 ≤ ν
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)
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)
⊢ ∀ᶠ (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:
simp only [eventually_atTop]

Premises used: Filter.eventually_atTop
-- 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
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)

Tactic:
⟨n, fun m hnm ↦ ?_⟩

Premises used: Exists.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
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)
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)
⊢ ∃ (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:
refine ⟨n, fun m hnm ↦ ?_⟩
-- 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
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
rw₁ rw₂ :
  Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ 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)

Tactic:
rw [setIntegral_densityProcess_of_le hκν hnm _ hs hA,
      setIntegral_densityProcess hκν _ _ hs hA]

Premises used: ProbabilityTheory.Kernel.setIntegral_densityProcess_of_le, ProbabilityTheory.Kernel.setIntegral_densityProcess
-- 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
A : Set γ
hA : MeasurableSet A
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)
⊢ 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)
      = 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]
-- 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
A : Set γ
hA : MeasurableSet A
⊢ 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
-- 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
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))
rw 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)
⊢ 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:
rw [h.limsup_eq]

Premises used: Filter.Tendsto.limsup_eq
-- 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 ν
a : α
s : Set β
hs : MeasurableSet s
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)
rw₁ 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)
⊢ (@integral _ _ _ _ mγ ((ν : (a : α) → Measure γ) a) 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]

Premises used: ProbabilityTheory.Kernel.setIntegral_density_of_measurableSet, OfNat.ofNat, MeasureTheory.setIntegral_univ, MeasurableSet.univ
-- 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 ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
⊢ 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 ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : IsFiniteKernel κ
rw : mγ = generateFrom (⋃ (i : ℕ), {x : Set γ | MeasurableSet x})
rw₁ : mγ = ⨆ (n : ℕ), (↑(countableFiltration γ) : ℕ → MeasurableSpace γ) n
rw₂ rw₃ : mγ = mγ
⊢ mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}

Tactic:
rw [setOf_exists, generateFrom_iUnion_measurableSet (countableFiltration γ),
      iSup_countableFiltration]

Premises used: MeasureTheory.Filtration.seq, MeasurableSpace.generateFrom_iUnion_measurableSet, ProbabilityTheory.countableFiltration, Set.setOf_exists, ProbabilityTheory.iSup_countableFiltration