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 : α
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∞)

Tactic:
exact measure_ne_top _ _

Premises used: MeasureTheory.measure_ne_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 α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
hx : ¬κ.densityProcess κ.fst n a x univ = 1
⊢ ¬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

Premises used: ProbabilityTheory.Kernel.densityProcess_fst_univ
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
hx :
  ¬Eq (α := ℝ)
      (if
          Eq (α := ℝ≥0∞)
            ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
            (0 : ℝ≥0∞) then
        0
      else 1)
      1
⊢ Eq (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa using hx
-- 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 : α
⊢ 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
-- 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 :
  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∞)

Tactic:
measure_mono_null this ?_

Premises used: MeasureTheory.measure_mono_null
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
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∞)}
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∞)
⊢ Eq (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
        {a_1 : γ | ¬κ.densityProcess κ.fst n a a_1 univ = 1} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
refine measure_mono_null this ?_

Premises used: MeasureTheory.measure_mono_null
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
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
simp :
  ∃ i ∈ countablePartition γ n,
    Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) ∧ t ∈ i
⊢ Membership.mem (γ := Set γ)
    (⋃ u ∈ countablePartition γ n,
      ⋃ (_ : Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)),
        u)
    t

Tactic:
simp only [mem_setOf_eq, mem_iUnion, exists_prop] at ht ⊢

Premises used: Set.mem_iUnion, Set.mem_setOf_eq, exists_prop
-- 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 :
  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 :
  Eq (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ i ∈ countablePartition γ n,
    Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) ∧ t ∈ i

Tactic:
⟨countablePartitionSet n t, countablePartitionSet_mem _ _, ht,
      mem_countablePartitionSet _ _⟩

Premises used: MeasurableSpace.mem_countablePartitionSet, MeasurableSpace.countablePartitionSet, MeasurableSpace.countablePartitionSet_mem, And.intro, Exists.intro
-- 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 :
  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 :
  Eq (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ i ∈ countablePartition γ n,
    Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) ∧ t ∈ i

Tactic:
exact ⟨countablePartitionSet n t, countablePartitionSet_mem _ _, ht,
      mem_countablePartitionSet _ _⟩
-- 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 :
  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∞)}
⊢ 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 _ _⟩
-- 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)
⊢ 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:
measure_mono_null this ?_

Premises used: MeasureTheory.measure_mono_null
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
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)
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∞)
⊢ 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 ?_

Premises used: MeasureTheory.measure_mono_null
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
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
h :
  ∀ b ∈ countablePartition γ n,
    MeasurableSet.{u_3} (α := γ)
      (⋃ (_ :
        Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)), b)
⊢ 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:
rw [measure_biUnion]

Premises used: MeasureTheory.measure_biUnion
-- 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)
⊢ 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:
simp
-- 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)
⊢ (countablePartition γ n).Countable

Tactic:
(finite_countablePartition _ _).countable

Premises used: MeasurableSpace.finite_countablePartition, Set.Finite.countable
-- 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)
⊢ (countablePartition γ n).Countable

Tactic:
exact (finite_countablePartition _ _).countable

Premises used: MeasurableSpace.finite_countablePartition, Set.Finite.countable
-- 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
t : Set γ
ht : t ∈ countablePartition γ n
hst : s ≠ t
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
⊢ Function.onFun (β := Set γ) Disjoint
    (fun (u : Set γ) ↦
      ⋃ (_ : Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)),
        u)
    s t

Tactic:
simp only [disjoint_iUnion_right, disjoint_iUnion_left]

Premises used: Set.disjoint_iUnion_left, Set.disjoint_iUnion_right
-- 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
t : Set γ
ht : t ∈ countablePartition γ n
hst : s ≠ t
⊢ ∀ (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:
fun _ _ ↦ disjoint_countablePartition hs ht hst

Premises used: MeasurableSpace.disjoint_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
t : Set γ
ht : t ∈ countablePartition γ n
hst : s ≠ t
⊢ ∀ (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:
exact fun _ _ ↦ disjoint_countablePartition hs ht hst

Premises used: MeasurableSpace.disjoint_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
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)
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)
⊢ 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

Premises used: DFunLike.coe, ProbabilityTheory.Kernel.fst