awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq :
  ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' t) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) t
⊢ ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' tᶜ) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) tᶜ
have calc : ∫⁻ (b : β),
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' t)ᶜ ∂(ν : (a : α) → Measure β) a =
  ∫⁻ (b : β),
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ :
        ℝ≥0∞)
      ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' t) :
        ℝ≥0∞) ∂(ν : (a : α) → Measure β) a
Tactic: calc ∫⁻ b, hf.toKernel f (a, b) (Prod.mk b ⁻¹' tᶜ) ∂(ν a)
      = ∫⁻ b, hf.toKernel f (a, b) (Prod.mk b ⁻¹' t)ᶜ ∂(ν a) := rfl
    _ = ∫⁻ b, hf.toKernel f (a, b) univ
          - hf.toKernel f (a, b) (Prod.mk b ⁻¹' t) ∂(ν a) := by
        congr with x : 1
        exact measure_compl (measurable_prodMk_left ht)
          (measure_ne_top (hf.toKernel f (a, x)) _)
    _ = ∫⁻ x, hf.toKernel f (a, x) univ ∂(ν a) -
          ∫⁻ x, hf.toKernel f (a, x) (Prod.mk x ⁻¹' t) ∂(ν a) := by
        have h_le : (fun x ↦ hf.toKernel f (a, x) (Prod.mk x ⁻¹' t))
              ≤ᵐ[ν a] fun x ↦ hf.toKernel f (a, x) univ :=
          Eventually.of_forall fun _ ↦ measure_mono (subset_univ _)
        rw [lintegral_sub _ _ h_le]
        · exact Kernel.measurable_kernel_prodMk_left' ht a
        refine ((lintegral_mono_ae h_le).trans_lt ?_).ne
        rw [lintegral_toKernel_univ hf]
        exact measure_lt_top _ univ
    _ = κ a univ - κ a t := by rw [ht_eq, lintegral_toKernel_univ hf]
    _ = κ a tᶜ := (measure_compl ht (measure_ne_top _ _)).symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (f' i)
⊢ ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' ⋃ (i : ℕ), f' i) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (⋃ (i : ℕ), f' i)
have h_eq : ∀ (a : β), Eq (α := Set ℝ) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f' i) (⋃ (i : ℕ), Prod.mk a ⁻¹' f' i)
Tactic: have h_eq : ∀ a, Prod.mk a ⁻¹' ⋃ i, f' i = ⋃ i, Prod.mk a ⁻¹' f' i := by
      simp only [preimage_iUnion, implies_true]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (f' i)
h_eq : ∀ (a : β), Eq (α := Set ℝ) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f' i) (⋃ (i : ℕ), Prod.mk a ⁻¹' f' i)
⊢ ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' ⋃ (i : ℕ), f' i) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (⋃ (i : ℕ), f' i)
have iUnion : ∫⁻ (b : β),
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
      (⋃ (i : ℕ), Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
  (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (⋃ (i : ℕ), f' i)
Tactic: simp_rw [h_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (f' i)
h_eq : ∀ (a : β), Eq (α := Set ℝ) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f' i) (⋃ (i : ℕ), Prod.mk a ⁻¹' f' i)
a_1 : β
⊢ Pairwise (α := ℕ) (Function.onFun (β := Set ℝ) Disjoint fun (i : ℕ) ↦ Prod.mk a_1 ⁻¹' f' i)
have _ : ∀ ⦃i j : ℕ⦄, i ≠ j → Function.onFun (β := Set ℝ) Disjoint (fun (i : ℕ) ↦ Prod.mk a_1 ⁻¹' f' i) i j
Tactic: _
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (f' i)
h_eq : ∀ (a : β), Eq (α := Set ℝ) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f' i) (⋃ (i : ℕ), Prod.mk a ⁻¹' f' i)
⊢ ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (⋃ (i : ℕ), Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (⋃ (i : ℕ), f' i)
have h_disj : ∀ (a : β), Pairwise (α := ℕ) (Function.onFun (β := Set ℝ) Disjoint fun (i : ℕ) ↦ Prod.mk a ⁻¹' f' i)
Tactic: have h_disj : ∀ a, Pairwise (Disjoint on fun i ↦ Prod.mk a ⁻¹' f' i) := by
      intro _ _ _ hij
      exact Disjoint.preimage _ (hf_disj hij)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (f' i)
h_eq : ∀ (a : β), Eq (α := Set ℝ) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f' i) (⋃ (i : ℕ), Prod.mk a ⁻¹' f' i)
h_disj : ∀ (a : β), Pairwise (α := ℕ) (Function.onFun (β := Set ℝ) Disjoint fun (i : ℕ) ↦ Prod.mk a ⁻¹' f' i)
⊢ ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (⋃ (i : ℕ), Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      ∑' (i : ℕ),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a
have e_f : ∀ (x : β),
  Eq (α := ℝ≥0∞)
    ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (⋃ (i : ℕ), Prod.mk x ⁻¹' f' i) :
      ℝ≥0∞)
    (∑' (i : ℕ),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk x ⁻¹' f' i) :
      ℝ≥0∞)
Tactic: congr with x : 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (f' i)
h_eq : ∀ (a : β), Eq (α := Set ℝ) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f' i) (⋃ (i : ℕ), Prod.mk a ⁻¹' f' i)
h_disj : ∀ (a : β), Pairwise (α := ℕ) (Function.onFun (β := Set ℝ) Disjoint fun (i : ℕ) ↦ Prod.mk a ⁻¹' f' i)
x : β
⊢ Eq (α := ℝ≥0∞)
    ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (⋃ (i : ℕ), Prod.mk x ⁻¹' f' i) :
      ℝ≥0∞)
    (∑' (i : ℕ),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk x ⁻¹' f' i) :
      ℝ≥0∞)
have e_f : Eq (α := ℝ≥0∞)
  (∑' (i : ℕ),
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
      (Prod.mk x ⁻¹' f' i))
  (∑' (i : ℕ),
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
      (Prod.mk x ⁻¹' f' i))
Tactic: rw [measure_iUnion (h_disj x) fun i ↦ measurable_prodMk_left (hf_meas i)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (f' i)
h_eq : ∀ (a : β), Eq (α := Set ℝ) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f' i) (⋃ (i : ℕ), Prod.mk a ⁻¹' f' i)
h_disj : ∀ (a : β), Pairwise (α := ℕ) (Function.onFun (β := Set ℝ) Disjoint fun (i : ℕ) ↦ Prod.mk a ⁻¹' f' i)
⊢ ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (⋃ (i : ℕ), Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (⋃ (i : ℕ), f' i)
have calc : ∫⁻ (b : β),
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
      (⋃ (i : ℕ), Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
  ∫⁻ (b : β),
    ∑' (i : ℕ),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a
Tactic: calc ∫⁻ b, hf.toKernel f (a, b) (⋃ i, Prod.mk b ⁻¹' f' i) ∂(ν a)
      = ∫⁻ b, ∑' i, hf.toKernel f (a, b) (Prod.mk b ⁻¹' f' i) ∂(ν a) := by
          congr with x : 1
          rw [measure_iUnion (h_disj x) fun i ↦ measurable_prodMk_left (hf_meas i)]
    _ = ∑' i, ∫⁻ b, hf.toKernel f (a, b) (Prod.mk b ⁻¹' f' i) ∂(ν a) :=
          lintegral_tsum fun i ↦ (Kernel.measurable_kernel_prodMk_left' (hf_meas i) a).aemeasurable
    _ = ∑' i, κ a (f' i) := by simp_rw [hf_eq]
    _ = κ a (iUnion f') := (measure_iUnion hf_disj hf_meas).symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (f' i)
h_eq : ∀ (a : β), Eq (α := Set ℝ) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f' i) (⋃ (i : ℕ), Prod.mk a ⁻¹' f' i)
h_disj : ∀ (a : β), Pairwise (α := ℕ) (Function.onFun (β := Set ℝ) Disjoint fun (i : ℕ) ↦ Prod.mk a ⁻¹' f' i)
calc :
  ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (⋃ (i : ℕ), Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      ∑' (i : ℕ),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a
⊢ ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (⋃ (i : ℕ), Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (⋃ (i : ℕ), f' i)
have calc₁ : Eq (α := ℝ≥0∞)
  (∑' (i : ℕ),
    ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a)
  (∑' (i : ℕ), (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (f' i))
Tactic: calc ∫⁻ b, hf.toKernel f (a, b) (⋃ i, Prod.mk b ⁻¹' f' i) ∂(ν a)
      = ∫⁻ b, ∑' i, hf.toKernel f (a, b) (Prod.mk b ⁻¹' f' i) ∂(ν a) := by
          congr with x : 1
          rw [measure_iUnion (h_disj x) fun i ↦ measurable_prodMk_left (hf_meas i)]
    _ = ∑' i, ∫⁻ b, hf.toKernel f (a, b) (Prod.mk b ⁻¹' f' i) ∂(ν a) :=
          lintegral_tsum fun i ↦ (Kernel.measurable_kernel_prodMk_left' (hf_meas i) a).aemeasurable
    _ = ∑' i, κ a (f' i) := by simp_rw [hf_eq]
    _ = κ a (iUnion f') := (measure_iUnion hf_disj hf_meas).symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
inst_1 : IsSFiniteKernel ν
hf : IsCondKernelCDF f κ ν
⊢ ν ⊗ₖ IsCondKernelCDF.toKernel f hf = κ
have h : ∀ (a : α) (s : Set (β × ℝ)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    ((((ν ⊗ₖ IsCondKernelCDF.toKernel f hf : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
inst_1 : IsSFiniteKernel ν
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((ν ⊗ₖ IsCondKernelCDF.toKernel f hf : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∫⁻ (b : β),
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' s) ∂(ν : (a : α) → Measure β) a =
  (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) s
Tactic: rw [Kernel.compProd_apply hs, lintegral_toKernel_mem hf a hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
inst_1 : IsSFiniteKernel ν
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
hs : MeasurableSet s
h :
  ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞)
    ((((ν ⊗ₖ IsCondKernelCDF.toKernel f hf : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Kernel.compProd_apply hs, lintegral_toKernel_mem hf a hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℝ
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((ρ.IicSnd r : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((ρ.restrict (SProd.sprod (α := Set α) univ (Iic r))).fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)
Tactic: rw [IicSnd, fst_apply hs, restrict_apply' (MeasurableSet.univ.prod measurableSet_Iic),
    univ_prod, Set.prod_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℝ
s : Set α
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) (((ρ.restrict (SProd.sprod (α := Set α) univ (Iic r))).fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ρ.IicSnd r : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((ρ.restrict (SProd.sprod (α := Set α) univ (Iic r)) : (a : Set (α × ℝ)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
  ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)
Tactic: rw [IicSnd, fst_apply hs, restrict_apply' (MeasurableSet.univ.prod measurableSet_Iic),
    univ_prod, Set.prod_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℝ
s : Set α
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) (((ρ.restrict (SProd.sprod (α := Set α) univ (Iic r))).fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    ((ρ.restrict (SProd.sprod (α := Set α) univ (Iic r)) : (a : Set (α × ℝ)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ρ.IicSnd r : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (Prod.fst ⁻¹' s ∩ SProd.sprod (α := Set α) univ (Iic r)) : ℝ≥0∞)
  ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)
Tactic: rw [IicSnd, fst_apply hs, restrict_apply' (MeasurableSet.univ.prod measurableSet_Iic),
    univ_prod, Set.prod_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℝ
s : Set α
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) (((ρ.restrict (SProd.sprod (α := Set α) univ (Iic r))).fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    ((ρ.restrict (SProd.sprod (α := Set α) univ (Iic r)) : (a : Set (α × ℝ)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (Prod.fst ⁻¹' s ∩ SProd.sprod (α := Set α) univ (Iic r)) : ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ρ.IicSnd r : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' Iic r) : ℝ≥0∞)
  ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)
Tactic: rw [IicSnd, fst_apply hs, restrict_apply' (MeasurableSet.univ.prod measurableSet_Iic),
    univ_prod, Set.prod_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℝ
s : Set α
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) (((ρ.restrict (SProd.sprod (α := Set α) univ (Iic r))).fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    ((ρ.restrict (SProd.sprod (α := Set α) univ (Iic r)) : (a : Set (α × ℝ)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (Prod.fst ⁻¹' s ∩ SProd.sprod (α := Set α) univ (Iic r)) : ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)
rw₃ :
  Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' Iic r) : ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ρ.IicSnd r : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)
have rw₄ : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' Iic r) : ℝ≥0∞)
  ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' Iic r) : ℝ≥0∞)
Tactic: rw [IicSnd, fst_apply hs, restrict_apply' (MeasurableSet.univ.prod measurableSet_Iic),
    univ_prod, Set.prod_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
t : ℚ
s : Set α
hs : MeasurableSet s
inst : IsFiniteMeasure ρ
⊢ Eq (α := ℝ≥0∞) (⨅ (r : { r' : ℚ // t < r' }), (ρ.IicSnd (↑(↑r : ℚ) : ℝ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ρ.IicSnd (↑t : ℝ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have simp_rw : Eq (α := ℝ≥0∞)
  (⨅ (r : { r' : ℚ // t < r' }), (ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(↑r : ℚ) : ℝ))) :
    ℝ≥0∞)
  ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑t : ℝ))) : ℝ≥0∞)
Tactic: simp_rw [ρ.IicSnd_apply _ hs, Measure.iInf_rat_gt_prod_Iic hs]