awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
inst_3 : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this :
  ∀ (b : β),
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (t.indicator 1 b : ENNReal) =
      t.indicator (fun (b : β) ↦ (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s) b
h₁ :
  Eq (α := ENNReal) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) (1 : ENNReal)
integral_le_kernel :
  ∫⁻ (b : β) in t, (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a ≤
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t
_ :
  HSub.hSub (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
      (∫⁻ (a : β) in t,
        (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a) =
    ∫⁻ (b : β) in t, 1 ∂(κ : (a : α) → Measure β) a -
      ∫⁻ (b : β) in t,
        (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a
_₁ :
  ∫⁻ (b : β) in t, 1 ∂(κ : (a : α) → Measure β) a -
      ∫⁻ (b : β) in t,
        (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β) in t,
      HSub.hSub (α := ENNReal) (β := ENNReal) (1 : ENNReal)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) ∂(κ : (a : α) → Measure β) a
⊢ HSub.hSub (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) t : ENNReal)
      (∫⁻ (a : β) in t,
        (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ENNReal) s ∂(κ : (a : α) → Measure β) a) ≤
    0
have _₂ : ∫⁻ (b : β),
    HSub.hSub (α := ENNReal) (β := ENNReal) (1 : ENNReal)
      ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ENNReal) s : ENNReal) ∂(κ : (a : α) → Measure β) a =
  ∫⁻ (x : β), (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ENNReal) sᶜ ∂(κ : (a : α) → Measure β) a
Tactic: calc
    _ = ∫⁻ b in t, 1 ∂κ a - ∫⁻ b in t, (η b) s ∂κ a := by
      rw [setLIntegral_one]
    _ = ∫⁻ b in t, 1 - (η b) s ∂κ a := by
      rw [lintegral_sub]
      · exact η.measurable_coe hs
      · exact ne_top_of_le_ne_top (by simp) integral_le_kernel
      · refine ae_of_all _ fun b ↦ ?_
        rw [← measure_univ (μ := η b)]
        exact measure_mono (by simp)
    _ ≤ ∫⁻ b, 1 - (η b) s ∂κ a := setLIntegral_le_lintegral _ _
    _ = ∫⁻ x, (η x) sᶜ ∂κ a := by
        congr with x
        rw [measure_compl hs (by simp)]
        simp
    _ = (η ∘ₖ κ) a sᶜ := by
        rw [η.comp_apply' _ _ hs.compl]
    _ = 0 := by
      rw [measure_compl hs (by simp), measure_univ h₁, h₁, tsub_self]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
hρ : ρ ≠ 0
⊢ IsSFiniteKernel ρCond
have contrapose : ∀ (hρ : ¬IsSFiniteKernel ρCond), ρ = 0
Tactic: contrapose hρ
Cleared hypotheses: hρ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
hρ : ¬IsSFiniteKernel ρCond
⊢ ρ = 0
have rwa : ρ.fst ⊗ₘ ρCond = 0
Tactic: rwa [← ρ.disintegrate ρCond, Measure.compProd_of_not_isSFiniteKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst : ρ.IsCondKernel ρCond
hρ : ¬IsSFiniteKernel ρCond
rwa : ρ.fst ⊗ₘ ρCond = 0
⊢ ρ = 0
have rwa₁ : Eq (α := Measure (α × Ω)) 0 0
Tactic: rwa [← ρ.disintegrate ρCond, Measure.compProd_of_not_isSFiniteKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (hypothesis)
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
⊢ (((ρ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∞)
have this : IsSFiniteKernel ρCond
Tactic: have := isSFiniteKernel ρ ρCond (by rintro rfl; simp at hx)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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
⊢ (((ρ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∞)
have nth_rewrite : (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
    ((ρ.fst ⊗ₘ ρCond : (a : Set (α × Ω)) → ℝ≥0∞) (SProd.sprod (α := Set α) {x} s) : ℝ≥0∞)
Tactic: nth_rewrite 2 [← ρ.disintegrate ρCond]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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
⊢ (((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
      ((ρ.fst ⊗ₘ ρCond : (a : Set (α × Ω)) → ℝ≥0∞) (SProd.sprod (α := Set α) {x} s) : ℝ≥0∞)
have rw : (((ρ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: rw [Measure.compProd_apply (measurableSet_prod.mpr (Or.inl ⟨measurableSet_singleton x, hs⟩))]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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∞)
have inl : ∀ (hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥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: obtain rfl | hax := eq_or_ne a x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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 : α
inl :
  ∀ (hx : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥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∞)
⊢ 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∞)
have inr : ∀ (hax : a ≠ x),
  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: obtain rfl | hax := eq_or_ne a x
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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∞)
⊢ 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∞)
have 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∞)
Tactic: simp only [singleton_prod, mem_singleton_iff, indicator_of_mem]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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∞)
⊢ 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∞)
have inl : ∀ (y : Ω), y ∈ Prod.mk a ⁻¹' Prod.mk a '' s ↔ y ∈ s
Tactic: congr with y
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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
⊢ 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∞)
have inr : Eq (α := ℝ≥0∞)
  ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (Prod.mk a ⁻¹' Prod.mk x '' s) : ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: simp only [singleton_prod, mem_singleton_iff, hax, not_false_eq_true, indicator_of_notMem]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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 = ∅
have h : ∀ (y : Ω), y ∈ Prod.mk a ⁻¹' Prod.mk x '' s ↔ Membership.mem (γ := Set Ω) ∅ y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (hypothesis)
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
⊢ Eq (α := ℝ≥0∞)
    ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (Prod.mk a ⁻¹' Prod.mk x '' s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have this₁ : Prod.mk a ⁻¹' Prod.mk x '' s = ∅
Tactic: have : Prod.mk a ⁻¹' Prod.mk x '' s = ∅ := by ext y; simp [Ne.symm hax]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (hypothesis)
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
⊢ (((ρ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)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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∞)
⊢ (((ρ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)
have 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)
Tactic: simp_rw [this]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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∞)
⊢ (((ρ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)
have 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)
Tactic: rw [MeasureTheory.lintegral_indicator (measurableSet_singleton x)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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∞)
⊢ (((ρ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)
have 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∞))
Tactic: simp only [Measure.restrict_singleton, lintegral_smul_measure, lintegral_dirac, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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∞)
⊢ (((ρ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∞))
have 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∞)
Tactic: rw [← mul_assoc, ENNReal.inv_mul_cancel hx (measure_ne_top _ _), one_mul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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∞)
⊢ (((ρ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∞))
have 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∞)
Tactic: rw [← mul_assoc, ENNReal.inv_mul_cancel hx (measure_ne_top _ _), one_mul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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∞)
⊢ (((ρ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∞))
have rw₂ : Eq (α := ℝ≥0∞) ((((ρCond : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥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]