awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
κ : Kernel Unit (α × Ω)
inst_3 : IsFiniteKernel κ
⊢ IsMarkovKernel (mα := Prod.instMeasurableSpace) (mβ := mΩ)
    (borelMarkovFromReal Ω (condKernelUnitReal (κ.map (Prod.map id (embeddingReal Ω)))))

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
κ : Kernel Unit (α × Ω)
inst_3 : IsFiniteKernel κ
rw : κ.fst ⊗ₖ borelMarkovFromReal Ω (condKernelUnitReal (κ.map (Prod.map id (embeddingReal Ω)))) = κ
rw₁ rw₂ : κ = κ
⊢ κ.fst ⊗ₖ κ.condKernelUnitBorel = κ

Tactic:
rw [condKernelUnitBorel, compProd_fst_borelMarkovFromReal _ _ (disintegrate _ _)]

Premises used: ProbabilityTheory.Kernel.compProd_fst_borelMarkovFromReal, ProbabilityTheory.Kernel.disintegrate, ProbabilityTheory.Kernel.condKernelUnitBorel
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
Ω : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
ρ : Measure (α × Ω)
inst_2 : IsFiniteMeasure ρ
a : α
rw :
  Eq.{u_4 + 1} (α := Measure Ω)
    (((condKernelUnitBorel (const Unit ρ)).comap (fun (a : α) ↦ ((), a)) ⋯ : (a : α) → Measure Ω) a : Measure Ω)
    ((condKernelUnitBorel (const Unit ρ) : (a : Unit × α) → Measure Ω) ((), a) : Measure Ω)
⊢ Eq.{u_4 + 1} (α := Measure Ω) ((ρ.condKernel : (a : α) → Measure Ω) a : Measure Ω)
    ((condKernelUnitBorel (const Unit ρ) : (a : Unit × α) → Measure Ω) ((), a) : Measure Ω)

Tactic:
rw [Measure.condKernel]

Premises used: MeasureTheory.Measure.condKernel
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
Ω : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
ρ : Measure (α × Ω)
inst_2 : IsFiniteMeasure ρ
a : α
⊢ Eq.{u_4 + 1} (α := Measure Ω)
    (((condKernelUnitBorel (const Unit ρ)).comap (fun (a : α) ↦ ((), a)) ⋯ : (a : α) → Measure Ω) a : Measure Ω)
    ((condKernelUnitBorel (const Unit ρ) : (a : Unit × α) → Measure Ω) ((), a) : Measure Ω)

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ_1 : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ_1
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
h :
  ∀ (a : Unit) (s : Set α),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((const Unit ρ.fst : (a : Unit) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
        ((((fst (const Unit ρ) : (a : Unit) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Kernel Unit α) (const Unit ρ.fst) (fst (const Unit ρ))

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ_1 : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ_1
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
a : Unit
s : Set α
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((const Unit ρ.fst : (a : Unit) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((((fst (const Unit ρ) : (a : Unit) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [fst_apply, Measure.fst, const_apply]

Premises used: ProbabilityTheory.Kernel.fst_apply, ProbabilityTheory.Kernel.const_apply, MeasureTheory.Measure.fst
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ_1 : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ_1
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
⊢ Eq (α := Kernel Unit α) (const Unit ρ.fst) (fst (const Unit ρ))

Tactic:
have h1 : const Unit (Measure.fst ρ) = fst (const Unit ρ) := by
      ext
      simp only [fst_apply, Measure.fst, const_apply]
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ_1 : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ_1
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
h1 : Eq (α := Kernel Unit α) (const Unit ρ.fst) (fst (const Unit ρ))
h :
  ∀ (a : Unit × α) (s : Set Ω),
    MeasurableSet s →
      Eq (α := ℝ≥0∞)
        (((((prodMkLeft Unit ρ.condKernel : Kernel.{u_1, u_4} (Unit × α) Ω) : (a : Unit × α) → Measure Ω) a :
                Measure Ω) :
              (a : Set Ω) → ℝ≥0∞)
            s :
          ℝ≥0∞)
        ((((condKernelUnitBorel (const Unit ρ) : (a : Unit × α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s :
          ℝ≥0∞)
⊢ prodMkLeft Unit ρ.condKernel = condKernelUnitBorel (const Unit ρ)

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ_1 : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ_1
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
h1 : Eq (α := Kernel Unit α) (const Unit ρ.fst) (fst (const Unit ρ))
a : Unit × α
s : Set Ω
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (((((prodMkLeft Unit ρ.condKernel : Kernel.{u_1, u_4} (Unit × α) Ω) : (a : Unit × α) → Measure Ω) a : Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((condKernelUnitBorel (const Unit ρ) : (a : Unit × α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [prodMkLeft_apply, Measure.condKernel_apply]

Premises used: ProbabilityTheory.Kernel.prodMkLeft_apply, MeasureTheory.Measure.condKernel_apply
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ_1 : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ_1
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
h1 : Eq (α := Kernel Unit α) (const Unit ρ.fst) (fst (const Unit ρ))
⊢ prodMkLeft Unit ρ.condKernel = condKernelUnitBorel (const Unit ρ)

Tactic:
have h2 : prodMkLeft Unit (Measure.condKernel ρ) = condKernelUnitBorel (const Unit ρ) := by
      ext
      simp only [prodMkLeft_apply, Measure.condKernel_apply]
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ_1 : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ_1
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
h1 : Eq (α := Kernel Unit α) (const Unit ρ.fst) (fst (const Unit ρ))
h2 : prodMkLeft Unit ρ.condKernel = condKernelUnitBorel (const Unit ρ)
rw : (const Unit ρ : (a : Unit) → Measure (α × Ω)) () = ρ
⊢ ρ.fst ⊗ₘ ρ.condKernel = ρ

Tactic:
rw [Measure.compProd, h1, h2, disintegrate]

Premises used: ProbabilityTheory.Kernel.disintegrate, MeasureTheory.Measure.compProd
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ_1 : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ_1
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
h1 : Eq (α := Kernel Unit α) (const Unit ρ.fst) (fst (const Unit ρ))
h2 : prodMkLeft Unit ρ.condKernel = condKernelUnitBorel (const Unit ρ)
⊢ (const Unit ρ : (a : Unit) → Measure (α × Ω)) () = ρ

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ_1 : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ_1
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
rw : IsMarkovKernel ((condKernelUnitBorel (const Unit ρ)).comap (fun (a : α) ↦ ((), a)) ⋯)
⊢ IsMarkovKernel ρ.condKernel

Tactic:
rw [Measure.condKernel]

Premises used: MeasureTheory.Measure.condKernel
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ_1 : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ_1
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
⊢ IsMarkovKernel ((condKernelUnitBorel (const Unit ρ)).comap (fun (a : α) ↦ ((), a)) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
Ω : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
ρ : Measure (α × Ω)
inst_2 : IsFiniteMeasure ρ
inst_3 : MeasurableSingletonClass α
x : α
hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
⊢ (((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
      ((ρ : (a : Set (α × Ω)) → ℝ≥0∞) (SProd.sprod (α := Set α) {x} s) : ℝ≥0∞)

Tactic:
Measure.IsCondKernel.apply_of_ne_zero _ _ hx _

Premises used: MeasureTheory.Measure.IsCondKernel.apply_of_ne_zero
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
h_1 : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel κ
hα : Countable α
x y : α
h : x ∈ measurableAtom y
⊢ Eq (α := Kernel β Ω) ((fun (a : α) ↦ (Measure.condKernel ((κ : (a : α) → Measure (β × Ω)) a) : Kernel β Ω)) x)
    ((fun (a : α) ↦ (Measure.condKernel ((κ : (a : α) → Measure (β × Ω)) a) : Kernel β Ω)) y)

Tactic:
simp [apply_congr_of_mem_measurableAtom _ h]

Premises used: ProbabilityTheory.Kernel.apply_congr_of_mem_measurableAtom
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
h : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel κ
rw :
  IsMarkovKernel (α := α × β) (β := Ω) (mα := Prod.instMeasurableSpace) (mβ := mΩ)
    (if hα : Countable α then
      condKernelCountable (fun (a : α) ↦ Measure.condKernel ((κ : (a : α) → Measure (β × Ω)) a)) ⋯
    else κ.condKernelBorel)
⊢ IsMarkovKernel κ.condKernel

Tactic:
rw [condKernel_def]

Premises used: ProbabilityTheory.Kernel.condKernel_def
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
h : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel κ
pos :
  ∀ (h : Countable α),
    IsMarkovKernel (α := α × β) (β := Ω) (mα := Prod.instMeasurableSpace) (mβ := mΩ)
      (condKernelCountable (fun (a : α) ↦ Measure.condKernel ((κ : (a : α) → Measure (β × Ω)) a)) ⋯)
neg : ∀ (h_1 : ¬Countable α), IsMarkovKernel κ.condKernelBorel
⊢ IsMarkovKernel (α := α × β) (β := Ω) (mα := Prod.instMeasurableSpace) (mβ := mΩ)
    (if hα : Countable α then
      condKernelCountable (fun (a : α) ↦ Measure.condKernel ((κ : (a : α) → Measure (β × Ω)) a)) ⋯
    else κ.condKernelBorel)

Tactic:
split_ifs
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
h : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel κ
h_1 : Countable α
⊢ IsMarkovKernel (α := α × β) (β := Ω) (mα := Prod.instMeasurableSpace) (mβ := mΩ)
    (condKernelCountable (fun (a : α) ↦ Measure.condKernel ((κ : (a : α) → Measure (β × Ω)) a)) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
h : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel κ
h_1 : ¬Countable α
⊢ IsMarkovKernel κ.condKernelBorel

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
h : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel κ
rw :
  (κ.fst ⊗ₖ
      if hα : Countable α then
        condKernelCountable (fun (a : α) ↦ Measure.condKernel ((κ : (a : α) → Measure (β × Ω)) a)) ⋯
      else κ.condKernelBorel) =
    κ
⊢ κ.fst ⊗ₖ κ.condKernel = κ

Tactic:
rw [condKernel_def]

Premises used: ProbabilityTheory.Kernel.condKernel_def
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
h : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel κ
pos :
  ∀ (hα : Countable α),
    κ.fst ⊗ₖ condKernelCountable (fun (a : α) ↦ Measure.condKernel ((κ : (a : α) → Measure (β × Ω)) a)) ⋯ = κ
neg : ∀ (hα : ¬Countable α), κ.fst ⊗ₖ κ.condKernelBorel = κ
⊢ (κ.fst ⊗ₖ
      if hα : Countable α then
        condKernelCountable (fun (a : α) ↦ Measure.condKernel ((κ : (a : α) → Measure (β × Ω)) a)) ⋯
      else κ.condKernelBorel) =
    κ

Tactic:
split_ifs with hα
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
h : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel κ
hα : Countable α
⊢ κ.fst ⊗ₖ condKernelCountable (fun (a : α) ↦ Measure.condKernel ((κ : (a : α) → Measure (β × Ω)) a)) ⋯ = κ

Tactic:
disintegrate _ _

Premises used: ProbabilityTheory.Kernel.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
h : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel κ
hα : Countable α
⊢ κ.fst ⊗ₖ condKernelCountable (fun (a : α) ↦ Measure.condKernel ((κ : (a : α) → Measure (β × Ω)) a)) ⋯ = κ

Tactic:
exact disintegrate _ _

Premises used: ProbabilityTheory.Kernel.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
h : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel κ
hα : ¬Countable α
⊢ κ.fst ⊗ₖ κ.condKernelBorel = κ

Tactic:
disintegrate _ _

Premises used: ProbabilityTheory.Kernel.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
h : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel κ
hα : ¬Countable α
⊢ κ.fst ⊗ₖ κ.condKernelBorel = κ

Tactic:
exact disintegrate _ _

Premises used: ProbabilityTheory.Kernel.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsSFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
s : Set Ω
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite
    (Kernel.measurable_coe κ hs) (Kernel.measurable_coe ρ.condKernel hs) (fun t ht _ ↦ ?_)

Premises used: MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite, Filter.EventuallyEq, MeasureTheory.Measure.condKernel, ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsSFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
s : Set Ω
hs : MeasurableSet s
refine :
  ∀ (t : Set α) (ht : MeasurableSet t),
    LT.lt (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
      ∫⁻ (x : α) in t, (((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂ρ.fst =
        ∫⁻ (x : α) in t, (((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂ρ.fst
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite
    (Kernel.measurable_coe κ hs) (Kernel.measurable_coe ρ.condKernel hs) (fun t ht _ ↦ ?_)

Premises used: MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite, MeasureTheory.Measure.condKernel, ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsSFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
s : Set Ω
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : ((ρ.fst ⊗ₘ κ : (a : Set (α × Ω)) → ℝ≥0∞) (t ×ˢ s) : ℝ≥0∞)
| ∫⁻ (x : α) in t, (((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂ρ.fst

Tactic:
rw [Measure.setLIntegral_condKernel_eq_measure_prod ht hs, hκ]

Premises used: MeasureTheory.Measure.setLIntegral_condKernel_eq_measure_prod
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsSFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
s : Set Ω
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
conv_rhs :
  ∫⁻ (x : α) in t, (((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂ρ.fst =
    (ρ.fst ⊗ₘ κ : (a : Set (α × Ω)) → ℝ≥0∞) (t ×ˢ s)
⊢ ∫⁻ (x : α) in t, (((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂ρ.fst =
    ∫⁻ (x : α) in t, (((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂ρ.fst

Tactic:
conv_rhs => rw [Measure.setLIntegral_condKernel_eq_measure_prod ht hs, hκ]

Premises used: MeasureTheory.Measure.setLIntegral_condKernel_eq_measure_prod
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsSFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
s : Set Ω
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in t, (((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂ρ.fst =
    (ρ.fst ⊗ₘ κ : (a : Set (α × Ω)) → ℝ≥0∞) (t ×ˢ s)

Tactic:
(Measure.compProd_apply_prod ht hs).symm

Premises used: MeasureTheory.Measure.compProd_apply_prod, Eq.symm
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsSFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
s : Set Ω
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in t, (((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂ρ.fst =
    (ρ.fst ⊗ₘ κ : (a : Set (α × Ω)) → ℝ≥0∞) (t ×ˢ s)

Tactic:
exact (Measure.compProd_apply_prod ht hs).symm

Premises used: MeasureTheory.Measure.compProd_apply_prod, Eq.symm
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst_1 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
have huniv : ∀ᵐ x ∂ρ.fst, κ x Set.univ = ρ.condKernel x Set.univ :=
    eq_condKernel_of_measure_eq_compProd' κ hκ MeasurableSet.univ