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 α γ
κ' : Kernel α (γ × β)
hκκ' : κ ≤ κ'
hκ'ν : κ'.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
h_le :
  LE.le (α := ℝ≥0∞)
    ((((κ' : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ s) :
      ℝ≥0∞)
    ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
neg :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ' : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ s) :
        ℝ≥0∞)
      ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞) ≠
    ∞
neg₁ :
  LE.le (α := Measure (γ × β)) ((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β))
    ((κ' : (a : α) → Measure (γ × β)) a : Measure (γ × β))
⊢ (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n x ×ˢ s) :
          ℝ≥0∞)
        ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)).toReal ≤
    (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ' : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n x ×ˢ s) :
          ℝ≥0∞)
        ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)).toReal

Tactic:
gcongr
-- 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 α γ
κ' : Kernel α (γ × β)
hκκ' : κ ≤ κ'
hκ'ν : κ'.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
h_le :
  LE.le (α := ℝ≥0∞)
    ((((κ' : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ s) :
      ℝ≥0∞)
    ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
neg :
  Eq (α := ℝ≥0∞)
      ((((κ' : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ s) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (∞ : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ' : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ s) :
        ℝ≥0∞)
      ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞) ≠
    ∞

Tactic:
simp only [ne_eq, ENNReal.div_eq_top, h0, and_false, false_or, not_and, not_not]

Premises used: Classical.not_not, false_or, ne_eq, ENNReal.div_eq_top, and_false, not_and
-- 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 α γ
κ' : Kernel α (γ × β)
hκκ' : κ ≤ κ'
hκ'ν : κ'.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
h_le :
  LE.le (α := ℝ≥0∞)
    ((((κ' : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ s) :
      ℝ≥0∞)
    ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
      ((((κ' : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ s) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (∞ : ℝ≥0∞)

Tactic:
fun h_top ↦ eq_top_mono h_le h_top

Premises used: eq_top_mono
-- 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 α γ
κ' : Kernel α (γ × β)
hκκ' : κ ≤ κ'
hκ'ν : κ'.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
h_le :
  LE.le (α := ℝ≥0∞)
    ((((κ' : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ s) :
      ℝ≥0∞)
    ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
      ((((κ' : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ s) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (∞ : ℝ≥0∞)

Tactic:
exact fun h_top ↦ eq_top_mono h_le h_top

Premises used: eq_top_mono
-- 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 α γ
κ' : Kernel α (γ × β)
hκκ' : κ ≤ κ'
hκ'ν : κ'.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
h_le :
  LE.le (α := ℝ≥0∞)
    ((((κ' : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ s) :
      ℝ≥0∞)
    ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
⊢ LE.le (α := Measure (γ × β)) ((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β))
    ((κ' : (a : α) → Measure (γ × β)) a : Measure (γ × β))

Tactic:
apply 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νν' : ν ≤ ν'
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
⊢ LE.le (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ s) :
      ℝ≥0∞)
    ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)

Tactic:
have h_le : κ a (countablePartitionSet n x ×ˢ s) ≤ ν a (countablePartitionSet n x) :=
    meas_countablePartitionSet_le_of_fst_le hκν n a x s
-- 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νν' : ν ≤ ν'
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
h_le :
  LE.le (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ s) :
      ℝ≥0∞)
    ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
pos :
  ∀
    (h0 :
      Eq (α := ℝ≥0∞)
        ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
        (0 : ℝ≥0∞)),
    (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (countablePartitionSet n x ×ˢ s) :
            ℝ≥0∞)
          ((((ν' : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) :
            ℝ≥0∞)).toReal ≤
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (countablePartitionSet n x ×ˢ s) :
            ℝ≥0∞)
          ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)).toReal
neg :
  ∀
    (h0 :
      ¬Eq (α := ℝ≥0∞)
          ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
          (0 : ℝ≥0∞)),
    (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (countablePartitionSet n x ×ˢ s) :
            ℝ≥0∞)
          ((((ν' : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) :
            ℝ≥0∞)).toReal ≤
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (countablePartitionSet n x ×ˢ s) :
            ℝ≥0∞)
          ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)).toReal
⊢ (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n x ×ˢ s) :
          ℝ≥0∞)
        ((((ν' : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)).toReal ≤
    (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n x ×ˢ s) :
          ℝ≥0∞)
        ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)).toReal

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

Premises used: MeasurableSpace.countablePartitionSet, 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νν' : ν ≤ ν'
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
h_le :
  LE.le (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ s) :
      ℝ≥0∞)
    ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
h0 :
  Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n x ×ˢ s) :
          ℝ≥0∞)
        ((((ν' : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)).toReal ≤
    (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n x ×ˢ s) :
          ℝ≥0∞)
        ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)).toReal

Tactic:
simp [nonpos_iff_eq_zero.1 (h_le.trans h0.le), h0]

Premises used: Eq.le, Iff.mp, LE.le.trans, nonpos_iff_eq_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νν' : ν ≤ ν'
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
h_le :
  LE.le (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ s) :
      ℝ≥0∞)
    ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
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∞)
          (countablePartitionSet n x ×ˢ s) :
        ℝ≥0∞)
      ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞) ≠
    ∞
neg₁ : LE.le.{u_3} (α := Measure γ) ((ν : (a : α) → Measure γ) a : Measure γ) ((ν' : (a : α) → Measure γ) a : Measure γ)
⊢ (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n x ×ˢ s) :
          ℝ≥0∞)
        ((((ν' : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)).toReal ≤
    (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n x ×ˢ s) :
          ℝ≥0∞)
        ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)).toReal

Tactic:
gcongr
-- 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νν' : ν ≤ ν'
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
h_le :
  LE.le (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ s) :
      ℝ≥0∞)
    ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
neg :
  Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ s) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (∞ : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ s) :
        ℝ≥0∞)
      ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞) ≠
    ∞

Tactic:
simp only [ne_eq, ENNReal.div_eq_top, h0, and_false, false_or, not_and, not_not]

Premises used: Classical.not_not, false_or, ne_eq, ENNReal.div_eq_top, and_false, not_and
-- 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νν' : ν ≤ ν'
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
h_le :
  LE.le (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ s) :
      ℝ≥0∞)
    ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ s) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (∞ : ℝ≥0∞)

Tactic:
fun h_top ↦ eq_top_mono h_le h_top

Premises used: eq_top_mono
-- 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νν' : ν ≤ ν'
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
h_le :
  LE.le (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ s) :
      ℝ≥0∞)
    ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ s) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (∞ : ℝ≥0∞)

Tactic:
exact fun h_top ↦ eq_top_mono h_le h_top

Premises used: eq_top_mono
-- 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νν' : ν ≤ ν'
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
h_le :
  LE.le (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ s) :
      ℝ≥0∞)
    ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ LE.le.{u_3} (α := Measure γ) ((ν : (a : α) → Measure γ) a : Measure γ) ((ν' : (a : α) → Measure γ) a : Measure γ)

Tactic:
apply 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 α γ
n : ℕ
a : α
x : γ
⊢ κ.densityProcess ν n a x ∅ = 0

Tactic:
simp [densityProcess]

Premises used: ProbabilityTheory.Kernel.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 α γ
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)
pos :
  ∀
    (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)
neg :
  ∀
    (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)
⊢ 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:
by_cases h0 : ν a (countablePartitionSet n x) = 0

Premises used: MeasurableSpace.countablePartitionSet, 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 α γ
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∞)
pos :
  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))
⊢ 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:
simp_rw [h0, ENNReal.toReal_div]

Premises used: ENNReal.toReal_div