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 α γ
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 :
  Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Tendsto
    (fun (m : ℕ) ↦
      ENNReal.toReal
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n x ×ˢ seq m)) /
        ENNReal.toReal 0)
    atTop
    (𝓝
      (ENNReal.toReal
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (SProd.sprod (β := Set β) (countablePartitionSet n x) ∅)) /
        ENNReal.toReal 0))

Tactic:
simp
-- 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 α γ
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (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∞)
          ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)).toReal)
    atTop
    (𝓝
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (SProd.sprod (β := Set β) (countablePartitionSet n x) ∅) :
            ℝ≥0∞)
          ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)).toReal)

Tactic:
(ENNReal.tendsto_toReal ?_).comp ?_

Premises used: ENNReal.tendsto_toReal, ENNReal.toReal, 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 α γ
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
neg :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (β := Set β) (countablePartitionSet n x) ∅) :
        ℝ≥0∞)
      ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞) ≠
    ∞
neg₁ :
  Tendsto
    (fun (m : ℕ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n x ×ˢ seq m) :
          ℝ≥0∞)
        ((((ν : (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) ∅) :
          ℝ≥0∞)
        ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)))
⊢ Tendsto
    (fun (m : ℕ) ↦
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (countablePartitionSet n x ×ˢ seq m) :
            ℝ≥0∞)
          ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)).toReal)
    atTop
    (𝓝
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (SProd.sprod (β := Set β) (countablePartitionSet n x) ∅) :
            ℝ≥0∞)
          ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)).toReal)

Tactic:
refine (ENNReal.tendsto_toReal ?_).comp ?_

Premises used: ENNReal.tendsto_toReal, 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 α γ
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
neg :
  ¬(Ne (α := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (SProd.sprod (β := Set β) (countablePartitionSet n x) ∅) :
            ℝ≥0∞)
          (0 : ℝ≥0∞) ∧
        Eq (α := ℝ≥0∞)
          ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
          (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (SProd.sprod (β := Set β) (countablePartitionSet n x) ∅) :
            ℝ≥0∞)
          (∞ : ℝ≥0∞) ∧
        Ne (α := ℝ≥0∞)
          ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
          (∞ : ℝ≥0∞))
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (β := Set β) (countablePartitionSet n x) ∅) :
        ℝ≥0∞)
      ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞) ≠
    ∞

Tactic:
rw [ne_eq, ENNReal.div_eq_top]

Premises used: ne_eq, ENNReal.div_eq_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 α γ
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
neg :
  (∀
      (_ :
        Ne (α := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (SProd.sprod (β := Set β) (countablePartitionSet n x) ∅) :
            ℝ≥0∞)
          (0 : ℝ≥0∞)),
      Ne (α := ℝ≥0∞)
        ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
        (0 : ℝ≥0∞)) ∧
    ∀
      (_ :
        Eq (α := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (SProd.sprod (β := Set β) (countablePartitionSet n x) ∅) :
            ℝ≥0∞)
          (∞ : ℝ≥0∞)),
      Eq (α := ℝ≥0∞)
        ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ¬(Ne (α := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (SProd.sprod (β := Set β) (countablePartitionSet n x) ∅) :
            ℝ≥0∞)
          (0 : ℝ≥0∞) ∧
        Eq (α := ℝ≥0∞)
          ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
          (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (SProd.sprod (β := Set β) (countablePartitionSet n x) ∅) :
            ℝ≥0∞)
          (∞ : ℝ≥0∞) ∧
        Ne (α := ℝ≥0∞)
          ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
          (∞ : ℝ≥0∞))

Tactic:
push Not

Premises used: Not
-- 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 α γ
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ (∀
      (_ :
        Ne (α := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (SProd.sprod (β := Set β) (countablePartitionSet n x) ∅) :
            ℝ≥0∞)
          (0 : ℝ≥0∞)),
      Ne (α := ℝ≥0∞)
        ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
        (0 : ℝ≥0∞)) ∧
    ∀
      (_ :
        Eq (α := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (SProd.sprod (β := Set β) (countablePartitionSet n x) ∅) :
            ℝ≥0∞)
          (∞ : ℝ≥0∞)),
      Eq (α := ℝ≥0∞)
        ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- 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 α γ
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (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∞)
        ((((ν : (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) ∅) :
          ℝ≥0∞)
        ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)))

Tactic:
ENNReal.Tendsto.div_const ?_ (.inr h0)

Premises used: ENNReal.Tendsto.div_const, Or.inr
-- 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 α γ
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (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) ∅)) :
      Filter ℝ≥0∞)
⊢ Tendsto
    (fun (m : ℕ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n x ×ˢ seq m) :
          ℝ≥0∞)
        ((((ν : (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) ∅) :
          ℝ≥0∞)
        ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)))

Tactic:
refine ENNReal.Tendsto.div_const ?_ (.inr h0)

Premises used: ENNReal.Tendsto.div_const, Or.inr
-- 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 α γ
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
hs : ∀ (i : ℕ), NullMeasurableSet (countablePartitionSet n x ×ˢ seq i) ((κ : (a : α) → Measure (γ × β)) a)
hm : Antitone (β := Set (γ × β)) fun (m : ℕ) ↦ countablePartitionSet n x ×ˢ seq m
hf :
  ∃ (i : ℕ),
    Ne (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ seq i) :
        ℝ≥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∞)
          (⋂ (n_1 : ℕ), countablePartitionSet n x ×ˢ seq n_1)) :
      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 α γ
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ ∀ (i : ℕ), NullMeasurableSet (countablePartitionSet n x ×ˢ 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 α γ
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Antitone (β := Set (γ × β)) fun (m : ℕ) ↦ countablePartitionSet n x ×ˢ seq m

Tactic:
fun _ _ h ↦ prod_mono_right <| hseq h

Premises used: Set.prod_mono_right, Antitone
-- 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 α γ
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Antitone (β := Set (γ × β)) fun (m : ℕ) ↦ countablePartitionSet n x ×ˢ seq m

Tactic:
exact fun _ _ h ↦ prod_mono_right <| hseq h

Premises used: Set.prod_mono_right
-- 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 α γ
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ ∃ (i : ℕ),
    Ne (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ 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 α γ
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ ∃ (i : ℕ),
    Ne (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ 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 α γ
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (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∞)
          (⋂ (n_1 : ℕ), countablePartitionSet n x ×ˢ seq n_1)) :
      Filter ℝ≥0∞)

Tactic:
have : Tendsto (fun m ↦ κ a (countablePartitionSet n x ×ˢ seq m)) atTop
      (𝓝 ((κ a) (⋂ n_1, countablePartitionSet n x ×ˢ seq n_1))) := by
    apply tendsto_measure_iInter_atTop
    · measurability
    · exact fun _ _ h ↦ prod_mono_right <| hseq h
    · 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 α γ
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
this :
  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∞)
          (⋂ (n_1 : ℕ), countablePartitionSet n x ×ˢ seq n_1)) :
      Filter ℝ≥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) ∅)) :
      Filter ℝ≥0∞)

Tactic:
simpa only [← prod_iInter, hseq_iInter] using this

Premises used: Set.prod_iInter
-- 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 α γ
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
rw : Tendsto (fun (m : ℕ) ↦ κ.densityProcess ν n a x (seq m)) atTop (𝓝 (κ.densityProcess ν n a x ∅))
⊢ Tendsto (β := ℝ) (fun (m : ℕ) ↦ κ.densityProcess ν n a x (seq m)) atTop (𝓝 0)

Tactic:
rw [← densityProcess_empty κ ν n a x]

Premises used: ProbabilityTheory.Kernel.densityProcess_empty
-- 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 α γ
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (fun (m : ℕ) ↦ κ.densityProcess ν n a x (seq m)) atTop (𝓝 (κ.densityProcess ν n a x ∅))

Tactic:
tendsto_densityProcess_atTop_empty_of_antitone κ ν n a x seq hseq hseq_iInter hseq_meas

Premises used: ProbabilityTheory.Kernel.tendsto_densityProcess_atTop_empty_of_antitone
-- 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 α γ
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (fun (m : ℕ) ↦ κ.densityProcess ν n a x (seq m)) atTop (𝓝 (κ.densityProcess ν n a x ∅))

Tactic:
exact tendsto_densityProcess_atTop_empty_of_antitone κ ν n a x seq hseq hseq_iInter hseq_meas

Premises used: ProbabilityTheory.Kernel.tendsto_densityProcess_atTop_empty_of_antitone
-- 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
⊢ ∀ᵐ (x : γ) ∂((ν : (a : α) → Measure γ) a : Measure γ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ κ.densityProcess ν n a x s) atTop
      (𝓝
        (Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
          ((ν : (a : α) → Measure γ) a) x))

Tactic:
Submartingale.ae_tendsto_limitProcess (martingale_densityProcess hκν a hs).submartingale
    (R := (ν a univ).toNNReal) (fun n ↦ ?_)

Premises used: MeasureTheory.Martingale.submartingale, ProbabilityTheory.Kernel.martingale_densityProcess, MeasureTheory.Submartingale.ae_tendsto_limitProcess