awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : IsFiniteKernel κ
obtain :
  ∀ (S : Finset (Set γ)) (hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n)
    (hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))),
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (⋃₀ (↑S : Set (Set γ)))) fun (x : γ) ↦
        κ.densityProcess ν n a x s) =
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (⋃₀ (↑S : Set (Set γ)) ×ˢ s)
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.densityProcess ν n a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)

Tactic:
obtain ⟨S, hS_subset, rfl⟩ := (measurableSet_generateFrom_countablePartition_iff _ _).mp hA

Premises used: MeasurableSpace.measurableSet_generateFrom_countablePartition_iff, Iff.mp, rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
simp_rw :
  (@integral _ _ _ _ mγ
      (Measure.restrict ((ν : (a : α) → Measure γ) a) (⋃ (i : (↑(↑S : Set (Set γ)) : Type u_3)), (↑i : Set γ)))
      fun (x : γ) ↦ κ.densityProcess ν n a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
      (SProd.sprod (α := Set γ) (⋃ (i : (↑(↑S : Set (Set γ)) : Type u_3)), (↑i : Set γ)) s)
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (⋃₀ (↑S : Set (Set γ)))) fun (x : γ) ↦
      κ.densityProcess ν n a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (⋃₀ (↑S : Set (Set γ)) ×ˢ s)

Tactic:
simp_rw [sUnion_eq_iUnion]

Premises used: Set.sUnion_eq_iUnion
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
u v : ↥S
huv : u ≠ v
⊢ (↑u : Set γ) ∈ (↑S : Set (Set γ))

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 α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
u v : ↥S
huv : u ≠ v
⊢ (↑v : Set γ) ∈ (↑S : Set (Set γ))

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 α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
u v : ↥S
huv : u ≠ v
refine : (↑u : Set γ) ≠ (↑v : Set γ)
⊢ Disjoint (↑u : Set γ) (↑v : Set γ)

Tactic:
refine disjoint_countablePartition (hS_subset (by simp)) (hS_subset (by simp)) ?_

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 α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
u v : ↥S
huv : u ≠ v
rwa : ¬(↑u : Set γ) = (↑v : Set γ)
rwa₁ rwa₂ rwa₃ rwa₄ : ¬u = v
⊢ (↑u : Set γ) ≠ (↑v : Set γ)

Tactic:
rwa [ne_eq, ← Subtype.ext_iff]

Premises used: ne_eq, Subtype.ext_iff
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
⊢ Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))

Tactic:
have h_disj : Pairwise (Disjoint on fun i : S ↦ (i : Set γ)) := by
    intro u v huv
    simp only [Function.onFun]
    refine disjoint_countablePartition (hS_subset (by simp)) (hS_subset (by simp)) ?_
    rwa [ne_eq, ← Subtype.ext_iff]
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
h_disj : Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))
rw :
  Eq (α := ℝ)
    (∑' (n_1 : (↑(↑S : Set (Set γ)) : Type u_3)),
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (↑n_1 : Set γ)) fun (x : γ) ↦
        κ.densityProcess ν n a x s)
    (∑' (a_1 : (↑(↑S : Set (Set γ)) : Type u_3)),
      ENNReal.toReal
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑a_1 : Set γ) ×ˢ s)))
hn :
  Pairwise.{u_3} (α := (↑(↑S : Set (Set γ)) : Type u_3))
    (Function.onFun (β := Set (γ × β)) Disjoint fun (i : (↑(↑S : Set (Set γ)) : Type u_3)) ↦ (↑i : Set γ) ×ˢ s)
h : ∀ (i : (↑(↑S : Set (Set γ)) : Type u_3)), MeasurableSet ((↑i : Set γ) ×ˢ s)
hm : ∀ (i : (↑(↑S : Set (Set γ)) : Type u_3)), MeasurableSet (↑i : Set γ)
hd :
  Pairwise.{u_3} (α := (↑(↑S : Set (Set γ)) : Type u_3))
    (Disjoint on Subtype.val (p := fun (x : Set γ) ↦ x ∈ (↑S : Set (Set γ))))
hfi :
  IntegrableOn (ε := ℝ) (mα := mγ) (fun (x : γ) ↦ κ.densityProcess ν n a x s)
    (⋃ (i : (↑(↑S : Set (Set γ)) : Type u_3)), (↑i : Set γ)) ((ν : (a : α) → Measure γ) a)
⊢ (@integral _ _ _ _ mγ
      (Measure.restrict ((ν : (a : α) → Measure γ) a) (⋃ (i : (↑(↑S : Set (Set γ)) : Type u_3)), (↑i : Set γ)))
      fun (x : γ) ↦ κ.densityProcess ν n a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
      (SProd.sprod (α := Set γ) (⋃ (i : (↑(↑S : Set (Set γ)) : Type u_3)), (↑i : Set γ)) s)

Tactic:
rw [integral_iUnion, iUnion_prod_const, measureReal_def, measure_iUnion,
      ENNReal.tsum_toReal_eq (fun _ ↦ measure_ne_top _ _)]

Premises used: MeasureTheory.measure_ne_top, Set.iUnion_prod_const, MeasureTheory.measure_iUnion, MeasureTheory.measureReal_def, MeasureTheory.integral_iUnion, ENNReal.tsum_toReal_eq
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
h_disj : Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))
e_f :
  ∀ (u : (↑(↑S : Set (Set γ)) : Type u_3)),
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (↑u : Set γ)) fun (x : γ) ↦
        κ.densityProcess ν n a x s) =
      ENNReal.toReal
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑u : Set γ) ×ˢ s))
⊢ Eq (α := ℝ)
    (∑' (n_1 : (↑(↑S : Set (Set γ)) : Type u_3)),
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (↑n_1 : Set γ)) fun (x : γ) ↦
        κ.densityProcess ν n a x s)
    (∑' (a_1 : (↑(↑S : Set (Set γ)) : Type u_3)),
      ENNReal.toReal
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑a_1 : Set γ) ×ˢ s)))

Tactic:
congr with u
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
h_disj : Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))
u : (↑(↑S : Set (Set γ)) : Type u_3)
⊢ (↑u : Set γ) ∈ (↑S : Set (Set γ))

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 α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
h_disj : Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))
u : (↑(↑S : Set (Set γ)) : Type u_3)
e_f :
  Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) ((↑u : Set γ) ×ˢ s) =
    ENNReal.toReal
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑u : Set γ) ×ˢ s))
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (↑u : Set γ)) fun (x : γ) ↦
      κ.densityProcess ν n a x s) =
    ENNReal.toReal
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑u : Set γ) ×ˢ s))

Tactic:
rw [setIntegral_densityProcess_of_mem hκν _ _ hs (hS_subset (by simp))]

Premises used: ProbabilityTheory.Kernel.setIntegral_densityProcess_of_mem
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
h_disj : Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))
u : (↑(↑S : Set (Set γ)) : Type u_3)
⊢ Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) ((↑u : Set γ) ×ˢ s) =
    ENNReal.toReal
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑u : Set γ) ×ˢ s))

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
h_disj : Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))
u v : (↑(↑S : Set (Set γ)) : Type u_3)
huv : u ≠ v
hn : Disjoint (↑u : Set γ) (↑v : Set γ) ∨ s = ⊥
⊢ Function.onFun (β := Set (γ × β)) Disjoint (fun (i : (↑(↑S : Set (Set γ)) : Type u_3)) ↦ (↑i : Set γ) ×ˢ s) u v

Tactic:
simp only [Finset.coe_sort_coe, Set.disjoint_prod, disjoint_self]

Premises used: Finset.coe_sort_coe, Set.disjoint_prod, disjoint_self
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
h_disj : Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))
u v : (↑(↑S : Set (Set γ)) : Type u_3)
huv : u ≠ v
⊢ Disjoint (↑u : Set γ) (↑v : Set γ) ∨ s = ⊥

Tactic:
Or.inl (h_disj huv)

Premises used: Or.inl
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
h_disj : Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))
u v : (↑(↑S : Set (Set γ)) : Type u_3)
huv : u ≠ v
⊢ Disjoint (↑u : Set γ) (↑v : Set γ) ∨ s = ⊥

Tactic:
exact Or.inl (h_disj huv)

Premises used: Or.inl
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
h_disj : Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))
x : (↑(↑S : Set (Set γ)) : Type u_3)
⊢ (↑x : Set γ) ∈ (↑S : Set (Set γ))

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 α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
h_disj : Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))
⊢ ∀ (i : (↑(↑S : Set (Set γ)) : Type u_3)), MeasurableSet ((↑i : Set γ) ×ˢ s)

Tactic:
exact fun _ ↦ (measurableSet_countablePartition n (hS_subset (by simp))).prod hs

Premises used: MeasurableSet.prod, 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 α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
h_disj : Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))
⊢ ∀ (i : (↑(↑S : Set (Set γ)) : Type u_3)), MeasurableSet (↑i : Set γ)

Tactic:
exact fun _ ↦ measurableSet_countablePartition n (hS_subset (by simp))

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 α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
h_disj : Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))
⊢ Pairwise.{u_3} (α := (↑(↑S : Set (Set γ)) : Type u_3))
    (Disjoint on Subtype.val (p := fun (x : Set γ) ↦ x ∈ (↑S : Set (Set γ))))

Tactic:
h_disj
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
h_disj : Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))
⊢ Pairwise.{u_3} (α := (↑(↑S : Set (Set γ)) : Type u_3))
    (Disjoint on Subtype.val (p := fun (x : Set γ) ↦ x ∈ (↑S : Set (Set γ))))

Tactic:
exact h_disj
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
h_disj : Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))
⊢ IntegrableOn (ε := ℝ) (mα := mγ) (fun (x : γ) ↦ κ.densityProcess ν n a x s)
    (⋃ (i : (↑(↑S : Set (Set γ)) : Type u_3)), (↑i : Set γ)) ((ν : (a : α) → Measure γ) a)

Tactic:
(integrable_densityProcess hκν _ _ hs).integrableOn

Premises used: ProbabilityTheory.Kernel.integrable_densityProcess, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : (↑S : Set (Set γ)) ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ (↑S : Set (Set γ)))
h_disj : Pairwise.{u_3} (α := ↥S) (Function.onFun (β := Set γ) Disjoint fun (i : ↥S) ↦ (↑i : Set γ))
⊢ IntegrableOn (ε := ℝ) (mα := mγ) (fun (x : γ) ↦ κ.densityProcess ν n a x s)
    (⋃ (i : (↑(↑S : Set (Set γ)) : Type u_3)), (↑i : Set γ)) ((ν : (a : α) → Measure γ) a)

Tactic:
exact (integrable_densityProcess hκν _ _ hs).integrableOn

Premises used: ProbabilityTheory.Kernel.integrable_densityProcess, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
rw :
  (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) univ) fun (x : γ) ↦
      κ.densityProcess ν n a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)
rw₁ rw₂ :
  Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)
⊢ (@integral _ _ _ _ mγ ((ν : (a : α) → Measure γ) a) fun (x : γ) ↦ κ.densityProcess ν n a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)

Tactic:
rw [← setIntegral_univ, setIntegral_densityProcess hκν _ _ hs MeasurableSet.univ]

Premises used: ProbabilityTheory.Kernel.setIntegral_densityProcess, MeasureTheory.setIntegral_univ, MeasurableSet.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 α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
n m : ℕ
hnm : n ≤ m
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.densityProcess ν m a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)

Tactic:
setIntegral_densityProcess hκν m a hs ((countableFiltration γ).mono hnm A hA)

Premises used: ProbabilityTheory.countableFiltration, ProbabilityTheory.Kernel.setIntegral_densityProcess, MeasureTheory.Filtration.mono
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
i j : ℕ
hij : i ≤ j
a : α
s : Set β
hs : MeasurableSet s
⊢ (ae (F := Measure γ) ((ν : (a : α) → Measure γ) a : Measure γ)).EventuallyEq (β := ℝ)
    (condExp ((↑(countableFiltration γ) : ℕ → MeasurableSpace γ) i) (m₀ := mγ) ((ν : (a : α) → Measure γ) a)
      fun (x : γ) ↦ κ.densityProcess ν j a x s)
    fun (x : γ) ↦ κ.densityProcess ν i a x s

Tactic:
(ae_eq_condExp_of_forall_setIntegral_eq ?_ ?_ ?_ ?_ ?_).symm

Premises used: MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq, Filter.EventuallyEq.symm