awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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∞) (((ρ.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 have : ∀ (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: classical
  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]
  simp_rw [this]
  rw [MeasureTheory.lintegral_indicator (measurableSet_singleton x)]
  simp only [Measure.restrict_singleton, lintegral_smul_measure, lintegral_dirac, smul_eq_mul]
  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 : IsSFiniteKernel ρCond
have :
  ∀ (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 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∞)),
  (((ρ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: classical
  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]
  simp_rw [this]
  rw [MeasureTheory.lintegral_indicator (measurableSet_singleton x)]
  simp only [Measure.restrict_singleton, lintegral_smul_measure, lintegral_dirac, smul_eq_mul]
  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 Ω
⊢ 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∞)
have 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∞)
Tactic: congr 2 with s hs
-- 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 Ω
⊢ (((ρ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 : 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]
-- 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 α
a : α
ha : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ IsProbabilityMeasure.{u_3} (α := Ω) (m0 := mΩ) ((ρCond : (a : α) → Measure Ω) a)
have measure_univ : Eq (α := ℝ≥0∞) ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: constructor
-- 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 α
a : α
ha : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
have measure_univ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {a})⁻¹ : ℝ≥0∞)
    ((ρ : (a : Set (α × Ω)) → ℝ≥0∞) (SProd.sprod (α := Set α) (β := Set Ω) {a} univ) : ℝ≥0∞) =
  1
Tactic: rw [IsCondKernel.apply_of_ne_zero _ _ ha, prod_univ, ← Measure.fst_apply
    (measurableSet_singleton _), ENNReal.inv_mul_cancel ha (measure_ne_top _ _)]
-- 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 α
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
⊢ Eq (α := ℝ≥0∞) ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
have measure_univ₁ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {a})⁻¹ : ℝ≥0∞)
    ((ρ : (a : Set (α × Ω)) → ℝ≥0∞) (Prod.fst ⁻¹' {a}) : ℝ≥0∞) =
  1
Tactic: rw [IsCondKernel.apply_of_ne_zero _ _ ha, prod_univ, ← Measure.fst_apply
    (measurableSet_singleton _), ENNReal.inv_mul_cancel ha (measure_ne_top _ _)]
-- 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 α
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
⊢ Eq (α := ℝ≥0∞) ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
have measure_univ₂ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((ρ.fst : (a : Set α) → ℝ≥0∞) {a})⁻¹ : ℝ≥0∞)
    ((ρ.fst : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) =
  1
Tactic: rw [IsCondKernel.apply_of_ne_zero _ _ ha, prod_univ, ← Measure.fst_apply
    (measurableSet_singleton _), ENNReal.inv_mul_cancel ha (measure_ne_top _ _)]
-- 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 α
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
⊢ Eq (α := ℝ≥0∞) ((((ρCond : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
have measure_univ₃ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [IsCondKernel.apply_of_ne_zero _ _ ha, prod_univ, ← Measure.fst_apply
    (measurableSet_singleton _), ENNReal.inv_mul_cancel ha (measure_ne_top _ _)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (hypothesis)
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 : α
⊢ ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    IsProbabilityMeasure.{u_3} (α := Ω) (m0 := mΩ) ((κCond : (a : α × β) → Measure Ω) (a, b))
have h : κ.fst ⊗ₖ κCond = κ
Tactic: have h := disintegrate κ κCond
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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 = κ
⊢ ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    IsProbabilityMeasure.{u_3} (α := Ω) (m0 := mΩ) ((κCond : (a : α × β) → Measure Ω) (a, b))
have pos : ∀ (h_sfin : IsSFiniteKernel κCond),
  ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    IsProbabilityMeasure.{u_3} (α := Ω) (m0 := mΩ) ((κCond : (a : α × β) → Measure Ω) (a, b))
Tactic: by_cases h_sfin : IsSFiniteKernel κCond
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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))
⊢ ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    IsProbabilityMeasure.{u_3} (α := Ω) (m0 := mΩ) ((κCond : (a : α × β) → Measure Ω) (a, b))
have neg : ∀ (h_sfin : ¬IsSFiniteKernel κCond),
  ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    IsProbabilityMeasure.{u_3} (α := Ω) (m0 := mΩ) ((κCond : (a : α × β) → Measure Ω) (a, b))
Tactic: by_cases h_sfin : IsSFiniteKernel κCond
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (hypothesis)
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
⊢ ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    IsProbabilityMeasure.{u_3} (α := Ω) (m0 := mΩ) ((κCond : (a : α × β) → Measure Ω) (a, b))
have h₁ : 0 = κ
Tactic: rw [Kernel.compProd_of_not_isSFiniteKernel_right _ _ h_sfin] at h
Cleared hypotheses: h, h_sfin
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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 β),
    IsProbabilityMeasure.{u_3} (α := Ω) (m0 := mΩ) ((κCond : (a : α × β) → Measure Ω) (a, b))
have h₁ : ∀ (b : β),
  IsProbabilityMeasure.{u_3} (α := Ω) (m0 := mΩ) ((κCond : (a : α × β) → Measure Ω) (a, b)) ↔
    Eq (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
      (1 : ℝ≥0∞)
Tactic: convert! this with b
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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
⊢ ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    IsProbabilityMeasure.{u_3} (α := Ω) (m0 := mΩ) ((κCond : (a : α × β) → Measure Ω) (a, b))
have pos : ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
  Eq (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: suffices ∀ᵐ b ∂(κ.fst a), κCond (a, b) Set.univ = 1 by
    convert! this with b
    exact ⟨fun _ ↦ measure_univ, fun h ↦ ⟨h⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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 β),
      LE.le (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
        (1 : ℝ≥0∞)) ∧
    ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
      LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞)
        ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    Eq (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
      (1 : ℝ≥0∞)
have h₁ : ∀ (a_1 : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β)
          {x : β |
            (fun (b : β) ↦
                LE.le (α := ℝ≥0∞)
                  ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
                  (1 : ℝ≥0∞))
              x}
          x →
        Membership.mem (γ := Set β)
          {x : β |
            Membership.mem (γ := Set β)
                {x : β |
                  (fun (b : β) ↦
                      LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞)
                        ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞))
                    x}
                x →
              Membership.mem (γ := Set β)
                {x : β |
                  (fun (b : β) ↦
                      Eq (α := ℝ≥0∞)
                        ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
                        (1 : ℝ≥0∞))
                    x}
                x}
          x}
    a_1
Tactic: filter_upwards [this.1, this.2] with b h1 h2 using le_antisymm h1 h2
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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 β),
      LE.le (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
        (1 : ℝ≥0∞)) ∧
    ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
      LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞)
        ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
h₁ :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (b : β) ↦
                  LE.le (α := ℝ≥0∞)
                    ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
                    (1 : ℝ≥0∞))
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              Membership.mem (γ := Set β)
                  {x : β |
                    (fun (b : β) ↦
                        LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞)
                          ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞))
                      x}
                  x →
                Membership.mem (γ := Set β)
                  {x : β |
                    (fun (b : β) ↦
                        Eq (α := ℝ≥0∞)
                          ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
                          (1 : ℝ≥0∞))
                      x}
                  x}
            x}
      a_1
⊢ ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    Eq (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
      (1 : ℝ≥0∞)
have h₂ : ∀ (a_1 : β),
  LE.le (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, a_1) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
      (1 : ℝ≥0∞) →
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞)
        ((((κCond : (a : α × β) → Measure Ω) (a, a_1) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) →
      Eq (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, a_1) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
        (1 : ℝ≥0∞)
Tactic: filter_upwards [this.1, this.2] with b h1 h2 using le_antisymm h1 h2
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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
⊢ ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    Eq (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
      (1 : ℝ≥0∞)
have pos : (∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    LE.le (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
      (1 : ℝ≥0∞)) ∧
  ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞)
      ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: suffices (∀ᵐ b ∂(κ.fst a), κCond (a, b) Set.univ ≤ 1)
      ∧ (∀ᵐ b ∂(κ.fst a), 1 ≤ κCond (a, b) Set.univ) by
    filter_upwards [this.1, this.2] with b h1 h2 using le_antisymm h1 h2
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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
s : Set β
hs : MeasurableSet s
| ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have rw : (((((κ.fst ⊗ₖ κCond).fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β),
      s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
        b ∂(κ.fst : (a : α) → Measure β) a =
    (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
have conv_rhs : ∫⁻ (b : β),
    s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
      b ∂(κ.fst : (a : α) → Measure β) a =
  ((((κ.fst ⊗ₖ κCond).fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
Tactic: conv_rhs => rw [← h]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β),
      s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
        b ∂(κ.fst : (a : α) → Measure β) a =
    ((((κ.fst ⊗ₖ κCond).fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
have rw : ∫⁻ (b : β),
    s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
      b ∂(κ.fst : (a : α) → Measure β) a =
  ∫⁻ (b : β),
    s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
      b ∂(κ.fst : (a : α) → Measure β) a
Tactic: rw [fst_compProd_apply _ _ _ hs]