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 : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
simp_rw :
  Tendsto
    (fun (m : ℕ) ↦
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
        (SProd.sprod (α := Set γ) univ (seq m)))
    atTop (𝓝 (Measure.real (α := γ × β) (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) univ))
⊢ Tendsto (fun (m : ℕ) ↦ @integral _ _ _ _ mγ ((ν : (a : α) → Measure γ) a) fun (x : γ) ↦ κ.density ν a x (seq m)) atTop
    (𝓝 (Measure.real (α := γ × β) (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) univ))

Tactic:
simp_rw [integral_density hκν a (hseq_meas _)]

Premises used: ProbabilityTheory.Kernel.integral_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 : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
refine_2 :
  ∀
    (h_cont :
      ContinuousAt ENNReal.toReal
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ)),
    Tendsto
      (fun (m : ℕ) ↦
        Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
          (SProd.sprod (α := Set γ) univ (seq m)))
      atTop (𝓝 (Measure.real (α := γ × β) (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) univ))
refine_1 :
  Membership.mem (γ := Filter ℝ≥0∞)
    (𝓝 ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ) : Filter ℝ≥0∞)
    {a : ℝ≥0∞ | a ≠ ∞}
⊢ Tendsto
    (fun (m : ℕ) ↦
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
        (SProd.sprod (α := Set γ) univ (seq m)))
    atTop (𝓝 (Measure.real (α := γ × β) (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) univ))

Tactic:
have h_cont := ENNReal.continuousOn_toReal.continuousAt (x := κ a 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 : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
refine_1 :
  ∃ t ⊆ {a : ℝ≥0∞ | a ≠ ∞},
    IsOpen t ∧
      Membership.mem (α := ℝ≥0∞) t
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ Membership.mem (γ := Filter ℝ≥0∞)
    (𝓝 ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ) : Filter ℝ≥0∞)
    {a : ℝ≥0∞ | a ≠ ∞}

Tactic:
rw [mem_nhds_iff]

Premises used: mem_nhds_iff
-- 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 : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
⊢ ∃ t ⊆ {a : ℝ≥0∞ | a ≠ ∞},
    IsOpen t ∧
      Membership.mem (α := ℝ≥0∞) t
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
⟨Iio (κ a univ + 1), fun x hx ↦ ne_top_of_lt (?_ : x < κ a univ + 1), isOpen_Iio, ?_⟩

Premises used: Set.univ, isOpen_Iio, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat, Set.Iio, ne_top_of_lt, 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 ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
refine_1 :
  ∀ (x : ℝ≥0∞)
    (hx :
      x ∈
        Iio
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
            ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ : ℝ≥0∞)
            (1 : ℝ≥0∞))),
    x <
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
refine_1₁ :
  Membership.mem (α := ℝ≥0∞)
    (Iio
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)))
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ∃ t ⊆ {a : ℝ≥0∞ | a ≠ ∞},
    IsOpen t ∧
      Membership.mem (α := ℝ≥0∞) t
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
refine ⟨Iio (κ a univ + 1), fun x hx ↦ ne_top_of_lt (?_ : x < κ a univ + 1), isOpen_Iio, ?_⟩
-- 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 : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
x : ℝ≥0∞
hx :
  x ∈
    Iio
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞))
⊢ x <
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simpa using hx
-- 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 : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
⊢ (((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ <
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
ENNReal.lt_add_right (measure_ne_top _ _) one_ne_zero

Premises used: ENNReal.lt_add_right, MeasureTheory.measure_ne_top, one_ne_zero
-- 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 : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
⊢ (((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ <
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
exact ENNReal.lt_add_right (measure_ne_top _ _) one_ne_zero

Premises used: ENNReal.lt_add_right, MeasureTheory.measure_ne_top, one_ne_zero
-- 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 : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont :
  ContinuousAt ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ)
⊢ Tendsto
    (fun (m : ℕ) ↦
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
        (SProd.sprod (α := Set γ) univ (seq m)))
    atTop (𝓝 (Measure.real (α := γ × β) (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) univ))

Tactic:
h_cont.tendsto.comp ?_

Premises used: MeasureTheory.Measure.real, ENNReal.toReal, ContinuousAt.tendsto, Filter.Tendsto.comp, NNReal.toReal
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
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)
this : IsFiniteKernel κ
h_cont :
  ContinuousAt ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ)
refine_2 :
  Tendsto (β := ℝ≥0∞)
    (fun (m : ℕ) ↦
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (α := Set γ) univ (seq m)) :
        ℝ≥0∞))
    atTop (𝓝 ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ) : Filter ℝ≥0∞)
⊢ Tendsto
    (fun (m : ℕ) ↦
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
        (SProd.sprod (α := Set γ) univ (seq m)))
    atTop (𝓝 (Measure.real (α := γ × β) (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) univ))

Tactic:
refine h_cont.tendsto.comp ?_

Premises used: ContinuousAt.tendsto, Filter.Tendsto.comp
-- 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 : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont :
  ContinuousAt ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ)
⊢ Tendsto (α := ℕ) (β := ℝ≥0∞)
    (Function.comp (β := Set (γ × β))
        (⇑((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) fun (x : ℕ) ↦
        SProd.sprod (α := Set γ) univ (seq x) :
      ℕ → ℝ≥0∞)
    atTop
    (𝓝
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (⋃ (n : ℕ), SProd.sprod (α := Set γ) univ (seq n))) :
      Filter ℝ≥0∞)

Tactic:
tendsto_measure_iUnion_atTop (monotone_const.set_prod hseq)

Premises used: monotone_const, MeasureTheory.tendsto_measure_iUnion_atTop, Monotone.set_prod
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
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)
this : IsFiniteKernel κ
h_cont :
  ContinuousAt ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ)
h : Eq (α := Set (γ × β)) univ (⋃ (n : ℕ), SProd.sprod (α := Set γ) univ (seq n))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (m : ℕ) ↦
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (α := Set γ) univ (seq m)) :
        ℝ≥0∞))
    atTop (𝓝 ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ) : Filter ℝ≥0∞)

Tactic:
convert! tendsto_measure_iUnion_atTop (monotone_const.set_prod hseq)

Premises used: monotone_const, MeasureTheory.tendsto_measure_iUnion_atTop, Monotone.set_prod
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
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)
this : IsFiniteKernel κ
h_cont :
  ContinuousAt ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ)
h : univ = SProd.sprod (α := Set γ) (β := Set β) univ (⋃ (i : ℕ), seq i)
h₁ : univ = SProd.sprod (α := Set γ) (β := Set β) univ univ
h₂ h₃ : Eq (α := Set (γ × β)) univ univ
⊢ Eq (α := Set (γ × β)) univ (⋃ (n : ℕ), SProd.sprod (α := Set γ) univ (seq n))

Tactic:
rw [← prod_iUnion, hseq_iUnion, univ_prod_univ]

Premises used: Set.prod_iUnion, Set.univ_prod_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 : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ 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 : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
simp_rw :
  Tendsto (β := ℝ)
    (fun (m : ℕ) ↦
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
        (SProd.sprod (α := Set γ) univ (seq m)))
    atTop (𝓝 0)
⊢ Tendsto (β := ℝ)
    (fun (m : ℕ) ↦ @integral _ _ _ _ mγ ((ν : (a : α) → Measure γ) a) fun (x : γ) ↦ κ.density ν a x (seq m)) atTop (𝓝 0)

Tactic:
simp_rw [integral_density hκν a (hseq_meas _)]

Premises used: ProbabilityTheory.Kernel.integral_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 : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
⊢ ContinuousAt ENNReal.toReal 0

Tactic:
have h_cont := ENNReal.continuousAt_toReal ENNReal.zero_ne_top
-- 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 : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal 0
⊢ Tendsto
    (fun (m : ℕ) ↦
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
        (SProd.sprod (α := Set γ) univ (seq m)))
    atTop (𝓝 (ENNReal.toReal 0))

Tactic:
h_cont.tendsto.comp ?_

Premises used: MeasureTheory.Measure.real, ENNReal.toReal, ContinuousAt.tendsto, Filter.Tendsto.comp, NNReal.toReal
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal 0
refine :
  Tendsto (β := ℝ≥0∞)
    (fun (m : ℕ) ↦
      (((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set γ) univ (seq m)))
    atTop (𝓝 0)
⊢ Tendsto
    (fun (m : ℕ) ↦
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
        (SProd.sprod (α := Set γ) univ (seq m)))
    atTop (𝓝 (ENNReal.toReal 0))

Tactic:
refine h_cont.tendsto.comp ?_

Premises used: ContinuousAt.tendsto, Filter.Tendsto.comp
-- 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 : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal 0
hs : ∀ (i : ℕ), NullMeasurableSet (SProd.sprod (α := Set γ) univ (seq i)) ((κ : (a : α) → Measure (γ × β)) a)
hm : Antitone (β := Set (γ × β)) fun (m : ℕ) ↦ SProd.sprod (α := Set γ) univ (seq m)
hf :
  ∃ (i : ℕ),
    Ne (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (α := Set γ) univ (seq i)) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (m : ℕ) ↦
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (α := Set γ) univ (seq m)) :
        ℝ≥0∞))
    atTop
    (𝓝
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (⋂ (n : ℕ), (fun (m : ℕ) ↦ SProd.sprod (α := Set γ) univ (seq m)) n)) :
      Filter ℝ≥0∞)

Tactic:
apply tendsto_measure_iInter_atTop

Premises used: MeasureTheory.tendsto_measure_iInter_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 ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal 0
⊢ ∀ (i : ℕ), NullMeasurableSet (SProd.sprod (α := Set γ) univ (seq i)) ((κ : (a : α) → Measure (γ × β)) a)

Tactic:
measurability
-- 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 : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal 0
⊢ Antitone (β := Set (γ × β)) fun (m : ℕ) ↦ SProd.sprod (α := Set γ) univ (seq m)

Tactic:
antitone_const.set_prod hseq

Premises used: Antitone.set_prod, antitone_const
-- 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 : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal 0
⊢ Antitone (β := Set (γ × β)) fun (m : ℕ) ↦ SProd.sprod (α := Set γ) univ (seq m)

Tactic:
exact antitone_const.set_prod hseq

Premises used: Antitone.set_prod, antitone_const
-- 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 : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal 0
⊢ ∃ (i : ℕ),
    Ne (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (α := Set γ) univ (seq i)) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)

Tactic:
⟨0, measure_ne_top _ _⟩

Premises used: MeasureTheory.measure_ne_top, Exists.intro, OfNat.ofNat
-- 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 : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal 0
⊢ ∃ (i : ℕ),
    Ne (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (α := Set γ) univ (seq i)) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)

Tactic:
exact ⟨0, measure_ne_top _ _⟩
-- 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 : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal 0
⊢ Tendsto (β := ℝ≥0∞)
    (fun (m : ℕ) ↦
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (α := Set γ) univ (seq m)) :
        ℝ≥0∞))
    atTop
    (𝓝
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (⋂ (n : ℕ), (fun (m : ℕ) ↦ SProd.sprod (α := Set γ) univ (seq m)) n)) :
      Filter ℝ≥0∞)

Tactic:
have h : Tendsto (fun m ↦ κ a (univ ×ˢ seq m)) atTop
      (𝓝 ((κ a) (⋂ n, (fun m ↦ univ ×ˢ seq m) n))) := by
    apply tendsto_measure_iInter_atTop
    · measurability
    · exact antitone_const.set_prod hseq
    · exact ⟨0, measure_ne_top _ _⟩