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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
pos :
  ∀
    (h0 :
      Eq (α := ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
        (0 : ℝ≥0∞)),
    Tendsto
      (fun (m : ℕ) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (countablePartitionSet n x ×ˢ seq m) :
            ℝ≥0∞)
          ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞))
      atTop
      (𝓝
        (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
            ℝ≥0∞)
          ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)))
neg :
  ∀
    (h0 :
      ¬Eq (α := ℝ≥0∞)
          ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
          (0 : ℝ≥0∞)),
    Tendsto
      (fun (m : ℕ) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (countablePartitionSet n x ×ˢ seq m) :
            ℝ≥0∞)
          ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞))
      atTop
      (𝓝
        (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
            ℝ≥0∞)
          ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)))
⊢ Tendsto
    (fun (m : ℕ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n x ×ˢ seq m) :
          ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞))
    atTop
    (𝓝
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
          ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)))

Tactic:
by_cases h0 : fst κ a (countablePartitionSet n x) = 0

Premises used: MeasurableSpace.countablePartitionSet, DFunLike.coe, ProbabilityTheory.Kernel.fst
-- 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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  Eq (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞) (0 : ℝ≥0∞)
pos :
  ∀
    (h0 :
      Eq (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            {p : γ × β | p.1 ∈ 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∞)
              {p : γ × β | p.1 ∈ countablePartitionSet n x} :
            ℝ≥0∞))
      atTop
      (𝓝
        (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
            ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              {p : γ × β | p.1 ∈ countablePartitionSet n x} :
            ℝ≥0∞)))
⊢ Tendsto
    (fun (m : ℕ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n x ×ˢ seq m) :
          ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞))
    atTop
    (𝓝
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
          ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)))

Tactic:
rw [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)] at h0 ⊢

Premises used: MeasurableSpace.measurableSet_countablePartitionSet, ProbabilityTheory.Kernel.fst_apply'
-- 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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        {p : γ × β | p.1 ∈ countablePartitionSet n x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
this :
  ∀ (m : ℕ),
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ seq m) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
simp :
  0 =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
        ℝ≥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∞)
            {p : γ × β | p.1 ∈ countablePartitionSet n x} :
          ℝ≥0∞))
    atTop
    (𝓝
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
          ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            {p : γ × β | p.1 ∈ countablePartitionSet n x} :
          ℝ≥0∞)))

Tactic:
simp only [this, h0, ENNReal.zero_div, tendsto_const_nhds_iff]

Premises used: ENNReal.zero_div, tendsto_const_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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        {p : γ × β | p.1 ∈ countablePartitionSet n x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
this_1 :
  ∀ (m : ℕ),
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ seq m) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
this :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ 0 =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
simp only [this, ENNReal.zero_div]

Premises used: ENNReal.zero_div
-- 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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        {p : γ × β | p.1 ∈ countablePartitionSet n x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
this :
  ∀ (m : ℕ),
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ seq m) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
suffices :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ 0 =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
suffices κ a (countablePartitionSet n x ×ˢ univ) = 0 by
        simp only [this, ENNReal.zero_div]
-- 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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        {p : γ × β | p.1 ∈ countablePartitionSet n x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
this :
  ∀ (m : ℕ),
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ seq m) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        {p : γ × β | p.1 ∈ countablePartitionSet n x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
h0
-- 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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        {p : γ × β | p.1 ∈ countablePartitionSet n x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
this :
  ∀ (m : ℕ),
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ seq m) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
h : SProd.sprod (β := Set β) (countablePartitionSet n x) univ = {p : γ × β | p.1 ∈ countablePartitionSet n x}
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
convert! h0
-- 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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        {p : γ × β | p.1 ∈ countablePartitionSet n x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
this :
  ∀ (m : ℕ),
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ seq m) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
h :
  ∀ (x_1 : γ × β),
    x_1 ∈ SProd.sprod (β := Set β) (countablePartitionSet n x) univ ↔
      Membership.mem (γ := Set (γ × β)) {p : γ × β | p.1 ∈ countablePartitionSet n x} x_1
⊢ SProd.sprod (β := Set β) (countablePartitionSet n x) univ = {p : γ × β | p.1 ∈ countablePartitionSet n x}

Tactic:
ext x
-- 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 α (γ × β)
n : ℕ
a : α
x_1 : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        {p : γ × β | p.1 ∈ countablePartitionSet n x_1} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
this :
  ∀ (m : ℕ),
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x_1 ×ˢ seq m) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
x : γ × β
⊢ x ∈ SProd.sprod (β := Set β) (countablePartitionSet n x_1) univ ↔
    Membership.mem (γ := Set (γ × β)) {p : γ × β | p.1 ∈ countablePartitionSet n x_1} x

Tactic:
simp only [mem_prod, mem_univ, and_true, mem_setOf_eq]

Premises used: and_true, Set.mem_setOf_eq, Set.mem_prod, Set.mem_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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        {p : γ × β | p.1 ∈ countablePartitionSet n x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
pos :
  ∀ (m : ℕ),
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ seq m) :
        ℝ≥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∞)
            {p : γ × β | p.1 ∈ countablePartitionSet n x} :
          ℝ≥0∞))
    atTop
    (𝓝
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
          ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            {p : γ × β | p.1 ∈ countablePartitionSet n x} :
          ℝ≥0∞)))

Tactic:
suffices ∀ m, κ a (countablePartitionSet n x ×ˢ seq m) = 0 by
      simp only [this, h0, ENNReal.zero_div, tendsto_const_nhds_iff]
      suffices κ a (countablePartitionSet n x ×ˢ univ) = 0 by
        simp only [this, ENNReal.zero_div]
      convert! h0
      ext x
      simp only [mem_prod, mem_univ, and_true, mem_setOf_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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        {p : γ × β | p.1 ∈ countablePartitionSet n x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ ∀ (m : ℕ),
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ seq m) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
fun m ↦ measure_mono_null (fun x ↦ ?_) h0

Premises used: MeasureTheory.measure_mono_null
-- 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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        {p : γ × β | p.1 ∈ countablePartitionSet n x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
pos :
  ∀ (m : ℕ),
    ∀ x_1 ∈ countablePartitionSet n x ×ˢ seq m,
      Membership.mem (γ := Set (γ × β)) {p : γ × β | p.1 ∈ countablePartitionSet n x} x_1
⊢ ∀ (m : ℕ),
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ seq m) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
refine fun m ↦ measure_mono_null (fun x ↦ ?_) h0

Premises used: MeasureTheory.measure_mono_null
-- 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 α (γ × β)
n : ℕ
a : α
x_1 : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        {p : γ × β | p.1 ∈ countablePartitionSet n x_1} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
m : ℕ
x : γ × β
pos : x.1 ∈ countablePartitionSet n x_1 → x.2 ∈ seq m → x.1 ∈ countablePartitionSet n x_1
⊢ x ∈ countablePartitionSet n x_1 ×ˢ seq m →
    Membership.mem (γ := Set (γ × β)) {p : γ × β | p.1 ∈ countablePartitionSet n x_1} x

Tactic:
simp only [mem_prod, mem_setOf_eq, and_imp]

Premises used: and_imp, Set.mem_setOf_eq, Set.mem_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 α (γ × β)
n : ℕ
a : α
x_1 : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        {p : γ × β | p.1 ∈ countablePartitionSet n x_1} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
m : ℕ
x : γ × β
⊢ x.1 ∈ countablePartitionSet n x_1 → x.2 ∈ seq m → x.1 ∈ countablePartitionSet n x_1

Tactic:
fun h _ ↦ 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 α (γ × β)
n : ℕ
a : α
x_1 : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        {p : γ × β | p.1 ∈ countablePartitionSet n x_1} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
m : ℕ
x : γ × β
⊢ x.1 ∈ countablePartitionSet n x_1 → x.2 ∈ seq m → x.1 ∈ countablePartitionSet n x_1

Tactic:
exact fun h _ ↦ 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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  ¬Eq (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Tendsto
    (fun (m : ℕ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n x ×ˢ seq m) :
          ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞))
    atTop
    (𝓝
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
          ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)))

Tactic:
ENNReal.Tendsto.div_const ?_ ?_

Premises used: ENNReal.Tendsto.div_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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  ¬Eq (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
neg :
  Tendsto (β := ℝ≥0∞)
    (fun (m : ℕ) ↦
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ seq m) :
        ℝ≥0∞))
    atTop
    (𝓝
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (β := Set β) (countablePartitionSet n x) univ)) :
      Filter ℝ≥0∞)
neg₁ :
  Ne (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
        ℝ≥0∞)
      (0 : ℝ≥0∞) ∨
    Ne (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Tendsto
    (fun (m : ℕ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n x ×ˢ seq m) :
          ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞))
    atTop
    (𝓝
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
          ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)))

Tactic:
refine ENNReal.Tendsto.div_const ?_ ?_

Premises used: ENNReal.Tendsto.div_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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
h0 :
  ¬Eq (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Tendsto (α := ℕ) (β := ℝ≥0∞)
    (Function.comp (β := Set (γ × β))
        (⇑((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) fun (x_1 : ℕ) ↦
        countablePartitionSet n x ×ˢ seq x_1 :
      ℕ → ℝ≥0∞)
    atTop
    (𝓝
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (⋃ (n_1 : ℕ), countablePartitionSet n x ×ˢ seq n_1)) :
      Filter ℝ≥0∞)

Tactic:
tendsto_measure_iUnion_atTop (monotone_const.set_prod hseq)

Premises used: monotone_const, MeasureTheory.tendsto_measure_iUnion_atTop, Monotone.set_prod