awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (β := ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ mγ ((ν : (a : α) → Measure γ) a) fun (a_1 : γ) ↦ κ.density ν a a_1 (seq i)) atTop
    (𝓝 (@integral _ _ _ _ mγ ((ν : (a : α) → Measure γ) a) fun (a : γ) ↦ 0))
have refine_2 : Tendsto (β := ℝ)
  (fun (i : ℕ) ↦ @integral _ _ _ _ mγ ((ν : (a : α) → Measure γ) a) fun (a_1 : γ) ↦ κ.density ν a a_1 (seq i)) atTop
  (𝓝 0)
Tactic: rw [integral_zero]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
⊢ (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 =
    if
        Eq (α := ℝ≥0∞)
          ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
          (0 : ℝ≥0∞) then
      0
    else 1
have pos : ∀
  (h :
    Eq (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (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∞)).toReal =
    0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
pos :
  ∀
    (h :
      Eq (α := ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
        (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∞)).toReal =
      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∞)).toReal =
    if
        Eq (α := ℝ≥0∞)
          ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
          (0 : ℝ≥0∞) then
      0
    else 1
have neg : ∀
  (h :
    ¬Eq (α := ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
        (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∞)).toReal =
    1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h :
  Eq (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞) (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∞)).toReal =
    0
have pos : (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)).toReal =
  0
Tactic: simp only [h]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h :
  Eq (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
          ℝ≥0∞)
        (0 : ℝ≥0∞)).toReal =
    0
have pos : ∀
  (h' :
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)),
  (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
          ℝ≥0∞)
        (0 : ℝ≥0∞)).toReal =
    0
Tactic: by_cases h' : κ a (countablePartitionSet n x ×ˢ univ) = 0
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h :
  Eq (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞) (0 : ℝ≥0∞)
pos :
  ∀
    (h' :
      Eq (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
          ℝ≥0∞)
        (0 : ℝ≥0∞)),
    (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
              (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
            ℝ≥0∞)
          (0 : ℝ≥0∞)).toReal =
      0
⊢ (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
          ℝ≥0∞)
        (0 : ℝ≥0∞)).toReal =
    0
have neg : ∀
  (h' :
    ¬Eq (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
          ℝ≥0∞)
        (0 : ℝ≥0∞)),
  (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (SProd.sprod (β := Set β) (countablePartitionSet n x) univ) :
          ℝ≥0∞)
        (0 : ℝ≥0∞)).toReal =
    0
Tactic: by_cases h' : κ a (countablePartitionSet n x ×ˢ univ) = 0
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h :
  ¬Eq (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (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∞)).toReal =
    1
have neg : (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∞)).toReal =
  1
Tactic: rw [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h :
  ¬Eq (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ SProd.sprod (β := Set β) (countablePartitionSet n x) univ = {p : γ × β | p.1 ∈ countablePartitionSet n x}
have h₁ : ∀ (x_1 : γ × β),
  x_1 ∈ SProd.sprod (β := Set β) (countablePartitionSet n x) univ ↔
    Membership.mem (γ := Set (γ × β)) {p : γ × β | p.1 ∈ countablePartitionSet n x} x_1
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h :
  ¬Eq (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ (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∞)).toReal =
    1
have this : SProd.sprod (β := Set β) (countablePartitionSet n x) univ = {p : γ × β | p.1 ∈ countablePartitionSet n x}
Tactic: have : countablePartitionSet n x ×ˢ univ = {p : γ × β | p.1 ∈ countablePartitionSet n x} := by
      ext x
      simp
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h :
  ¬Eq (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
this : SProd.sprod (β := Set β) (countablePartitionSet n x) univ = {p : γ × β | p.1 ∈ countablePartitionSet n x}
⊢ (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∞)).toReal =
    1
have neg : ENNReal.toReal 1 = 1
Tactic: rw [this, ENNReal.div_self]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h :
  ¬Eq (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
this : SProd.sprod (β := Set β) (countablePartitionSet n x) univ = {p : γ × β | p.1 ∈ countablePartitionSet n x}
neg : ENNReal.toReal 1 = 1
⊢ (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∞)).toReal =
    1
have neg₁ : Ne (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
      {p : γ × β | p.1 ∈ countablePartitionSet n x} :
    ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: rw [this, ENNReal.div_self]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h :
  ¬Eq (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
this : SProd.sprod (β := Set β) (countablePartitionSet n x) univ = {p : γ × β | p.1 ∈ countablePartitionSet n x}
neg : ENNReal.toReal 1 = 1
neg₁ :
  Ne (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        {p : γ × β | p.1 ∈ countablePartitionSet n x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ (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∞)).toReal =
    1
have neg₂ : Ne (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
      {p : γ × β | p.1 ∈ countablePartitionSet n x} :
    ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: rw [this, ENNReal.div_self]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h :
  ¬Eq (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
this : SProd.sprod (β := Set β) (countablePartitionSet n x) univ = {p : γ × β | p.1 ∈ countablePartitionSet n x}
⊢ Ne (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        {p : γ × β | p.1 ∈ countablePartitionSet n x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have neg : ∀
  (h :
    ¬Eq (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            {p : γ × β | p.1 ∈ countablePartitionSet n x} :
          ℝ≥0∞)
        (0 : ℝ≥0∞))
  (this : SProd.sprod (β := Set β) (countablePartitionSet n x) univ = {p : γ × β | p.1 ∈ countablePartitionSet n x}),
  Ne (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        {p : γ × β | p.1 ∈ countablePartitionSet n x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: rwa [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)] at h
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
hx : ¬κ.densityProcess κ.fst n a x univ = 1
⊢ Eq (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞) (0 : ℝ≥0∞)
have hx₁ : ¬Eq (α := ℝ)
    (if
        Eq (α := ℝ≥0∞)
          ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
          (0 : ℝ≥0∞) then
      0
    else 1)
    1
Tactic: rw [densityProcess_fst_univ] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
⊢ Eq (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        {a_1 : γ | ¬κ.densityProcess κ.fst n a a_1 univ = 1} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have this : 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∞)}
Tactic: have : {x | ¬ densityProcess κ (fst κ) n a x univ = 1}
      ⊆ {x | fst κ a (countablePartitionSet n x) = 0} := by
    intro x hx
    simp only [mem_setOf_eq] at hx ⊢
    rw [densityProcess_fst_univ] at hx
    simpa using hx
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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 :
  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∞)}
⊢ Eq (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        {a_1 : γ | ¬κ.densityProcess κ.fst n a a_1 univ = 1} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have refine : Eq (α := ℝ≥0∞)
  ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
      {x : γ |
        Eq (α := ℝ≥0∞)
          ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
          (0 : ℝ≥0∞)} :
    ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: refine measure_mono_null this ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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 :
  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∞)}
t : γ
ht :
  Membership.mem (γ := Set γ)
    {x : γ |
      Eq (α := ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
        (0 : ℝ≥0∞)}
    t
⊢ Membership.mem (γ := Set γ)
    (⋃ u ∈ countablePartition γ n,
      ⋃ (_ : Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)),
        u)
    t
have simp : ∃ i ∈ countablePartition γ n,
  Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) ∧ t ∈ i
Tactic: simp only [mem_setOf_eq, mem_iUnion, exists_prop] at ht ⊢
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (hypothesis)
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 :
  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∞)}
⊢ Eq (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        {x : γ |
          Eq (α := ℝ≥0∞)
            ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
            (0 : ℝ≥0∞)} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have 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)
Tactic: have : {x | fst κ a (countablePartitionSet n x) = 0}
      ⊆ ⋃ (u) (_ : u ∈ countablePartition γ n) (_ : fst κ a u = 0), u := by
    intro t ht
    simp only [mem_setOf_eq, mem_iUnion, exists_prop] at ht ⊢
    exact ⟨countablePartitionSet n t, countablePartitionSet_mem _ _, ht,
      mem_countablePartitionSet _ _⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
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)
⊢ Eq (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        {x : γ |
          Eq (α := ℝ≥0∞)
            ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
            (0 : ℝ≥0∞)} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have refine : Eq (α := ℝ≥0∞)
  ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (⋃ u ∈ countablePartition γ n,
        ⋃ (_ :
          Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)),
          u) :
    ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: refine measure_mono_null this ?_