awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
s : Set Ω
hs : MeasurableSet s
this : IsSFiniteKernel ρCond
a : α
hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
inl :
  Eq (α := ℝ≥0∞)
    ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (Prod.mk a ⁻¹' Prod.mk a '' s) : ℝ≥0∞)
    ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk a ⁻¹' SProd.sprod (α := Set α) {a} s) :
      ℝ≥0∞)
    (indicator {a} (fun (x : α) ↦ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) a : ℝ≥0∞)

Tactic:
simp only [singleton_prod, mem_singleton_iff, indicator_of_mem]

Premises used: Set.singleton_prod, Set.indicator_of_mem, Set.mem_singleton_iff
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
s : Set Ω
hs : MeasurableSet s
this : IsSFiniteKernel ρCond
a : α
hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
inl : ∀ (y : Ω), y ∈ Prod.mk a ⁻¹' Prod.mk a '' s ↔ y ∈ s
⊢ Eq (α := ℝ≥0∞)
    ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (Prod.mk a ⁻¹' Prod.mk a '' s) : ℝ≥0∞)
    ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
congr with y
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
s : Set Ω
hs : MeasurableSet s
this : IsSFiniteKernel ρCond
a : α
hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
y : Ω
⊢ y ∈ Prod.mk a ⁻¹' Prod.mk a '' s ↔ y ∈ s

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
x : α
hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
hs : MeasurableSet s
this : IsSFiniteKernel ρCond
a : α
hax : a ≠ x
inr :
  Eq (α := ℝ≥0∞)
    ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (Prod.mk a ⁻¹' Prod.mk x '' s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk a ⁻¹' SProd.sprod (α := Set α) {x} s) :
      ℝ≥0∞)
    (indicator {x} (fun (x : α) ↦ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) a : ℝ≥0∞)

Tactic:
simp only [singleton_prod, mem_singleton_iff, hax, not_false_eq_true, indicator_of_notMem]

Premises used: Set.singleton_prod, Set.mem_singleton_iff, Set.indicator_of_notMem, not_false_eq_true
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
x : α
hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
hs : MeasurableSet s
this : IsSFiniteKernel ρCond
a : α
hax : a ≠ x
h : ∀ (y : Ω), y ∈ Prod.mk a ⁻¹' Prod.mk x '' s ↔ Membership.mem (γ := Set Ω) ∅ y
⊢ Prod.mk a ⁻¹' Prod.mk x '' s = ∅

Tactic:
ext y
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
x : α
hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
hs : MeasurableSet s
this : IsSFiniteKernel ρCond
a : α
hax : a ≠ x
y : Ω
⊢ y ∈ Prod.mk a ⁻¹' Prod.mk x '' s ↔ Membership.mem (γ := Set Ω) ∅ y

Tactic:
simp [Ne.symm hax]

Premises used: Ne.symm
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
x : α
hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
hs : MeasurableSet s
this : IsSFiniteKernel ρCond
a : α
hax : a ≠ x
⊢ Prod.mk a ⁻¹' Prod.mk x '' s = ∅

Tactic:
have : Prod.mk a ⁻¹' Prod.mk x '' s = ∅ := by ext y; simp [Ne.symm hax]
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
x : α
hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
hs : MeasurableSet s
this_1 : IsSFiniteKernel ρCond
a : α
hax : a ≠ x
this : Prod.mk a ⁻¹' Prod.mk x '' s = ∅
⊢ Eq (α := ℝ≥0∞)
    ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (Prod.mk a ⁻¹' Prod.mk x '' s) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
simp only [this, measure_empty]

Premises used: MeasureTheory.measure_empty
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
x : α
hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
hs : MeasurableSet s
this : IsSFiniteKernel ρCond
⊢ ∀ (a : α),
    Eq (α := ℝ≥0∞)
      ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (Prod.mk a ⁻¹' SProd.sprod (α := Set α) {x} s) :
        ℝ≥0∞)
      (indicator {x} (fun (x : α) ↦ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) a : ℝ≥0∞)

Tactic:
have (a : _) : ρCond a (Prod.mk a ⁻¹' {x} ×ˢ s) = ({x} : Set α).indicator (ρCond · s) a := by
    obtain rfl | hax := eq_or_ne a x
    · simp only [singleton_prod, mem_singleton_iff, indicator_of_mem]
      congr with y
      simp
    · simp only [singleton_prod, mem_singleton_iff, hax, not_false_eq_true, indicator_of_notMem]
      have : Prod.mk a ⁻¹' Prod.mk x '' s = ∅ := by ext y; simp [Ne.symm hax]
      simp only [this, measure_empty]
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
x : α
hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
hs : MeasurableSet s
this_1 : IsSFiniteKernel ρCond
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞)
      ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (Prod.mk a ⁻¹' SProd.sprod (α := Set α) {x} s) :
        ℝ≥0∞)
      (indicator {x} (fun (x : α) ↦ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) a : ℝ≥0∞)
simp_rw :
  (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
      (∫⁻ (a : α),
        indicator {x} (fun (x : α) ↦ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) a ∂ρ.fst)
⊢ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
      (∫⁻ (a : α),
        (((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (Prod.mk a ⁻¹' SProd.sprod (α := Set α) {x} s) ∂ρ.fst)

Tactic:
simp_rw [this]
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
x : α
hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
hs : MeasurableSet s
this_1 : IsSFiniteKernel ρCond
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞)
      ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (Prod.mk a ⁻¹' SProd.sprod (α := Set α) {x} s) :
        ℝ≥0∞)
      (indicator {x} (fun (x : α) ↦ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) a : ℝ≥0∞)
rw :
  (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
      (∫⁻ (a : α) in {x}, (((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂ρ.fst)
⊢ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
      (∫⁻ (a : α),
        indicator {x} (fun (x : α) ↦ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) a ∂ρ.fst)

Tactic:
rw [MeasureTheory.lintegral_indicator (measurableSet_singleton x)]

Premises used: MeasurableSingletonClass.measurableSet_singleton, MeasureTheory.lintegral_indicator
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
x : α
hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
hs : MeasurableSet s
this_1 : IsSFiniteKernel ρCond
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞)
      ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (Prod.mk a ⁻¹' SProd.sprod (α := Set α) {x} s) :
        ℝ≥0∞)
      (indicator {x} (fun (x : α) ↦ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) a : ℝ≥0∞)
simp :
  (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞)
        ((((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞))
⊢ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
      (∫⁻ (a : α) in {x}, (((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂ρ.fst)

Tactic:
simp only [Measure.restrict_singleton, lintegral_smul_measure, lintegral_dirac, smul_eq_mul]

Premises used: MeasureTheory.Measure.restrict_singleton, MeasureTheory.lintegral_smul_measure, MeasureTheory.lintegral_dirac, smul_eq_mul
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
x : α
hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
hs : MeasurableSet s
this_1 : IsSFiniteKernel ρCond
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞)
      ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (Prod.mk a ⁻¹' SProd.sprod (α := Set α) {x} s) :
        ℝ≥0∞)
      (indicator {x} (fun (x : α) ↦ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) a : ℝ≥0∞)
rw :
  (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    HMul.hMul (β := ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
        ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞))
      ((((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
      ((((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
rw₂ rw₃ :
  Eq (α := ℝ≥0∞) ((((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    ((((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞)
        ((((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞))

Tactic:
rw [← mul_assoc, ENNReal.inv_mul_cancel hx (measure_ne_top _ _), one_mul]

Premises used: mul_assoc, MeasureTheory.measure_ne_top, ENNReal.inv_mul_cancel, one_mul
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
x : α
hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
e_a :
  ∀ (s : Set Ω) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      (((comap (fun (y : Ω) ↦ (x, y)) (HSMul.hSMul (α := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞) ρ) :
              Measure Ω) :
            (a : Set Ω) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    (((comap (fun (y : Ω) ↦ (x, y)) (HSMul.hSMul (α := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞) ρ) :
            Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
congr 2 with s hs
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
x : α
hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s_1 s : Set Ω
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    (((comap (fun (y : Ω) ↦ (x, y)) (HSMul.hSMul (α := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞) ρ) :
            Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
simp [IsCondKernel.apply_of_ne_zero_of_measurableSet _ _ hx hs,
      (measurableEmbedding_prodMk_left x).comap_apply, Set.singleton_prod]

Premises used: Set.singleton_prod, MeasurableEmbedding.comap_apply, measurableEmbedding_prodMk_left, _private.0.MeasureTheory.Measure.IsCondKernel.apply_of_ne_zero_of_measurableSet
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
x : α
hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
⊢ Eq (α := ℝ≥0∞) ((((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    (((comap (fun (y : Ω) ↦ (x, y)) (HSMul.hSMul (α := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞) ρ) :
            Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
have : ρCond x s = ((ρ.fst {x})⁻¹ • ρ).comap (fun (y : Ω) ↦ (x, y)) s := by
    congr 2 with s hs
    simp [IsCondKernel.apply_of_ne_zero_of_measurableSet _ _ hx hs,
      (measurableEmbedding_prodMk_left x).comap_apply, Set.singleton_prod]
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
x : α
hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
this :
  Eq (α := ℝ≥0∞) ((((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    (((comap (fun (y : Ω) ↦ (x, y)) (HSMul.hSMul (α := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞) ρ) :
            Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        s :
      ℝ≥0∞)
⊢ (((ρCond : (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:
simp [this, (measurableEmbedding_prodMk_left x).comap_apply, Set.singleton_prod]

Premises used: Set.singleton_prod, MeasurableEmbedding.comap_apply, measurableEmbedding_prodMk_left
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
a : α
ha : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
measure_univ :
  Eq (α := ℝ≥0∞) ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ IsProbabilityMeasure.{u_3} (α := Ω) (m0 := mΩ) ((ρCond : (a : α) → Measure Ω) a)

Tactic:
constructor
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
a : α
ha : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
measure_univ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {a})⁻¹ : ℝ≥0∞)
      ((ρ : (a : Set (α × Ω)) → ℝ≥0∞) (SProd.sprod (α := Set α) (β := Set Ω) {a} univ) : ℝ≥0∞) =
    1
measure_univ₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {a})⁻¹ : ℝ≥0∞)
      ((ρ : (a : Set (α × Ω)) → ℝ≥0∞) (Prod.fst ⁻¹' {a}) : ℝ≥0∞) =
    1
measure_univ₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {a})⁻¹ : ℝ≥0∞)
      ((ρ.fst : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) =
    1
measure_univ₃ measure_univ₄ : Eq (α := ℝ≥0∞) 1 1
⊢ Eq (α := ℝ≥0∞) ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
rw [IsCondKernel.apply_of_ne_zero _ _ ha, prod_univ, ← Measure.fst_apply
    (measurableSet_singleton _), ENNReal.inv_mul_cancel ha (measure_ne_top _ _)]

Premises used: MeasurableSingletonClass.measurableSet_singleton, Set.prod_univ, MeasureTheory.measure_ne_top, MeasureTheory.Measure.fst_apply, ENNReal.inv_mul_cancel, MeasureTheory.Measure.IsCondKernel.apply_of_ne_zero
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
inst_1 : IsFiniteMeasure ρ
inst_2 : MeasurableSingletonClass α
hρ : ∀ (a : α), Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ IsMarkovKernel ρCond

Tactic:
⟨fun _ ↦ isProbabilityMeasure _ _ (hρ _)⟩

Premises used: MeasureTheory.Measure.IsCondKernel.isProbabilityMeasure, ProbabilityTheory.IsMarkovKernel.mk
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond_1 κCond : Kernel (α × β) Ω
⊢ fst.{u_1, u_2, u_3} (γ := Ω) (mγ := mΩ) 0 ⊗ₖ κCond = 0

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : κ.IsCondKernel κCond
⊢ κ.fst ⊗ₖ κCond = κ

Tactic:
IsCondKernel.disintegrate

Premises used: ProbabilityTheory.Kernel.IsCondKernel.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
⊢ κ.fst ⊗ₖ κCond = κ

Tactic:
have h := disintegrate κ κCond
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
pos :
  ∀ (h_sfin : IsSFiniteKernel κCond),
    ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
      IsProbabilityMeasure.{u_3} (α := Ω) (m0 := mΩ) ((κCond : (a : α × β) → Measure Ω) (a, b))
neg :
  ∀ (h_sfin : ¬IsSFiniteKernel κCond),
    ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
      IsProbabilityMeasure.{u_3} (α := Ω) (m0 := mΩ) ((κCond : (a : α × β) → Measure Ω) (a, b))
⊢ ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    IsProbabilityMeasure.{u_3} (α := Ω) (m0 := mΩ) ((κCond : (a : α × β) → Measure Ω) (a, b))

Tactic:
by_cases h_sfin : IsSFiniteKernel κCond

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : ¬IsSFiniteKernel κCond
⊢ 0 = κ

Tactic:
rw [Kernel.compProd_of_not_isSFiniteKernel_right _ _ h_sfin] at h

Premises used: ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_right
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : ¬IsSFiniteKernel κCond
h₁ : 0 = κ
⊢ ¬IsSFiniteKernel κCond

Tactic:
rw [Kernel.compProd_of_not_isSFiniteKernel_right _ _ h_sfin] at h

Premises used: ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_right
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : 0 = κ
h_sfin : ¬IsSFiniteKernel κCond
⊢ ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    IsProbabilityMeasure.{u_3} (α := Ω) (m0 := mΩ) ((κCond : (a : α × β) → Measure Ω) (a, b))

Tactic:
simp [h.symm]

Premises used: Eq.symm
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
this :
  ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    Eq (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
      (1 : ℝ≥0∞)
⊢ ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    Eq (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
      (1 : ℝ≥0∞)

Tactic:
this