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 α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
this_1 :
  Subset.{u_3} (α := Set γ) {x : γ | ¬κ.densityProcess κ.fst n a x univ = 1}
    {x : γ |
      Eq (α := ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
        (0 : ℝ≥0∞)}
this :
  Subset.{u_3} (α := Set γ)
    {x : γ |
      Eq (α := ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
        (0 : ℝ≥0∞)}
    (⋃ u ∈ countablePartition γ n,
      ⋃ (_ : Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)),
        u)
s : Set γ
hs : s ∈ countablePartition γ n
h : Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ MeasurableSet.{u_3} (α := γ)
    (⋃ (_ : Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
      s)

Tactic:
simp [h, measurableSet_countablePartition n hs]

Premises used: MeasurableSpace.measurableSet_countablePartition
-- 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 α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
this_1 :
  Subset.{u_3} (α := Set γ) {x : γ | ¬κ.densityProcess κ.fst n a x univ = 1}
    {x : γ |
      Eq (α := ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
        (0 : ℝ≥0∞)}
this :
  Subset.{u_3} (α := Set γ)
    {x : γ |
      Eq (α := ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
        (0 : ℝ≥0∞)}
    (⋃ u ∈ countablePartition γ n,
      ⋃ (_ : Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)),
        u)
s : Set γ
hs : s ∈ countablePartition γ n
h : ¬Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ MeasurableSet.{u_3} (α := γ)
    (⋃ (_ : Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
      s)

Tactic:
simp [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
⊢ 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∞)).toReal)
    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∞)).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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
refine_1 :
  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∞) ≠
    ∞
refine_2 :
  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∞)).toReal)
    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∞)).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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
refine_1 :
  ¬(Ne (α := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
            ℝ≥0∞)
          (0 : ℝ≥0∞) ∧
        Eq (α := ℝ≥0∞)
          ((((κ.fst : (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) univ) :
            ℝ≥0∞)
          (∞ : ℝ≥0∞) ∧
        Ne (α := ℝ≥0∞)
          ((((κ.fst : (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) univ) :
        ℝ≥0∞)
      ((((κ.fst : (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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
refine_1 :
  (∀
      (_ :
        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∞)) ∧
    ∀
      (_ :
        Eq (α := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
            ℝ≥0∞)
          (∞ : ℝ≥0∞)),
      Eq (α := ℝ≥0∞)
        ((((κ.fst : (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) univ) :
            ℝ≥0∞)
          (0 : ℝ≥0∞) ∧
        Eq (α := ℝ≥0∞)
          ((((κ.fst : (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) univ) :
            ℝ≥0∞)
          (∞ : ℝ≥0∞) ∧
        Ne (α := ℝ≥0∞)
          ((((κ.fst : (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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
refine_1 :
  (∀
      (_ :
        Ne (α := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
            ℝ≥0∞)
          (0 : ℝ≥0∞)),
      Ne (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            {p : γ × β | p.1 ∈ countablePartitionSet n x} :
          ℝ≥0∞)
        (0 : ℝ≥0∞)) ∧
    ∀
      (_ :
        Eq (α := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
            ℝ≥0∞)
          (∞ : ℝ≥0∞)),
      Eq (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            {p : γ × β | p.1 ∈ countablePartitionSet n x} :
          ℝ≥0∞)
        (∞ : ℝ≥0∞)
⊢ (∀
      (_ :
        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∞)) ∧
    ∀
      (_ :
        Eq (α := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
            ℝ≥0∞)
          (∞ : ℝ≥0∞)),
      Eq (α := ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
        (∞ : ℝ≥0∞)

Tactic:
simp_rw [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)]

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
refine_1 :
  ∀
    (_ :
      Ne (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
          ℝ≥0∞)
        (0 : ℝ≥0∞)),
    Ne (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          {p : γ × β | p.1 ∈ countablePartitionSet n x} :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
refine_1₁ :
  ∀
    (_ :
      Eq (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
          ℝ≥0∞)
        (∞ : ℝ≥0∞)),
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          {p : γ × β | p.1 ∈ countablePartitionSet n x} :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
⊢ (∀
      (_ :
        Ne (α := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
            ℝ≥0∞)
          (0 : ℝ≥0∞)),
      Ne (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            {p : γ × β | p.1 ∈ countablePartitionSet n x} :
          ℝ≥0∞)
        (0 : ℝ≥0∞)) ∧
    ∀
      (_ :
        Eq (α := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
            ℝ≥0∞)
          (∞ : ℝ≥0∞)),
      Eq (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            {p : γ × β | p.1 ∈ countablePartitionSet n x} :
          ℝ≥0∞)
        (∞ : ℝ≥0∞)

Tactic:
constructor
-- 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
⊢ ∀
    (_ :
      Ne (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
          ℝ≥0∞)
        (0 : ℝ≥0∞)),
    Ne (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          {p : γ × β | p.1 ∈ countablePartitionSet n x} :
        ℝ≥0∞)
      (0 : ℝ≥0∞)

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

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

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

Tactic:
fun h_top ↦ eq_top_mono (measure_mono (fun x ↦ ?_)) h_top

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

Tactic:
refine fun h_top ↦ eq_top_mono (measure_mono (fun x ↦ ?_)) h_top

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

Tactic:
exact fun h _ ↦ h