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 α (γ × β)
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∞)
        (⋃ u ∈ countablePartition γ n,
          ⋃ (_ :
            Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)),
            u) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  (∑' (p : (↑(countablePartition γ n) : Type u_3)),
    (((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (⋃ (_ :
        Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (↑p : Set γ) : ℝ≥0∞)
          (0 : ℝ≥0∞)),
        (↑p : Set γ)))
  0
Tactic: rw [measure_biUnion]
-- 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)
rw :
  Eq (α := ℝ≥0∞)
    (∑' (p : (↑(countablePartition γ n) : Type u_3)),
      (((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (⋃ (_ :
          Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (↑p : Set γ) : ℝ≥0∞)
            (0 : ℝ≥0∞)),
          (↑p : Set γ)))
    0
⊢ 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∞)
have hs : (countablePartition γ n).Countable
Tactic: rw [measure_biUnion]
-- 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)
rw :
  Eq (α := ℝ≥0∞)
    (∑' (p : (↑(countablePartition γ n) : Type u_3)),
      (((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (⋃ (_ :
          Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (↑p : Set γ) : ℝ≥0∞)
            (0 : ℝ≥0∞)),
          (↑p : Set γ)))
    0
hs : (countablePartition γ n).Countable
⊢ 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∞)
have hd : (countablePartition γ n).PairwiseDisjoint (α := Set γ) fun (u : Set γ) ↦
  ⋃ (_ : Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)), u
Tactic: rw [measure_biUnion]
-- 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)
rw :
  Eq (α := ℝ≥0∞)
    (∑' (p : (↑(countablePartition γ n) : Type u_3)),
      (((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (⋃ (_ :
          Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (↑p : Set γ) : ℝ≥0∞)
            (0 : ℝ≥0∞)),
          (↑p : Set γ)))
    0
hs : (countablePartition γ n).Countable
hd :
  (countablePartition γ n).PairwiseDisjoint (α := Set γ) fun (u : Set γ) ↦
    ⋃ (_ : 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∞)
        (⋃ u ∈ countablePartition γ n,
          ⋃ (_ :
            Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)),
            u) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have h : ∀ b ∈ countablePartition γ n,
  MeasurableSet.{u_3} (α := γ)
    (⋃ (_ : Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)),
      b)
Tactic: rw [measure_biUnion]
-- 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)
s : Set γ
hs : s ∈ countablePartition γ n
t : Set γ
ht : t ∈ countablePartition γ n
hst : s ≠ t
⊢ Function.onFun (β := Set γ) Disjoint
    (fun (u : Set γ) ↦
      ⋃ (_ : Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)),
        u)
    s t
have hd : ∀ (i : Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
  (i : Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  Disjoint s t
Tactic: simp only [disjoint_iUnion_right, disjoint_iUnion_left]
-- 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)
s : Set γ
hs : s ∈ countablePartition γ n
⊢ MeasurableSet.{u_3} (α := γ)
    (⋃ (_ : Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
      s)
have pos : ∀ (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: by_cases h : fst κ a s = 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 : α
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
pos :
  ∀ (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)
⊢ MeasurableSet.{u_3} (α := γ)
    (⋃ (_ : Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
      s)
have neg : ∀ (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: by_cases h : fst κ a s = 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 α (γ × β)
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)
have 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∞) ≠
  ∞
Tactic: refine (ENNReal.tendsto_toReal ?_).comp ?_
-- 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 α (γ × β)
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∞) ≠
    ∞
⊢ 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)
have 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∞)))
Tactic: refine (ENNReal.tendsto_toReal ?_).comp ?_
-- 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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
⊢ 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∞) ≠
    ∞
have 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∞))
Tactic: rw [ne_eq, ENNReal.div_eq_top]
-- 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 α (γ × β)
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∞) ∧
        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∞))
have 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∞)
Tactic: push Not
-- 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 α (γ × β)
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∞)
        ((((κ.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∞)
have 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∞)
Tactic: simp_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 α (γ × β)
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∞)) ∧
    ∀
      (_ :
        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∞)
have 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∞)
Tactic: constructor