awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t_1 : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t : Set (α × β)
htm : MeasurableSet t
iht :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
⊢ Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (univ \ Prod.mk a ⁻¹' t))
    fun (a : α) ↦
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
have h : ∀ (a : α),
  (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (univ \ Prod.mk a ⁻¹' t) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
Tactic: ext1 a
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t_1 : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t : Set (α × β)
htm : MeasurableSet t
iht :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
a : α
⊢ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (univ \ Prod.mk a ⁻¹' t) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
have h : NullMeasurableSet (Prod.mk a ⁻¹' t) ((κ : (a : α) → Measure β) a)
Tactic: rw [← Set.diff_inter_self_eq_diff, Set.inter_univ, measure_diff (Set.subset_univ _)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t_1 : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t : Set (α × β)
htm : MeasurableSet t
iht :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
a : α
h : NullMeasurableSet (Prod.mk a ⁻¹' t) ((κ : (a : α) → Measure β) a)
⊢ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (univ \ Prod.mk a ⁻¹' t) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
have h₁ : Ne (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← Set.diff_inter_self_eq_diff, Set.inter_univ, measure_diff (Set.subset_univ _)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t_1 : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t : Set (α × β)
htm : MeasurableSet t
iht :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (univ \ Prod.mk a ⁻¹' t)
have this : Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
  (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (univ \ Prod.mk a ⁻¹' t))
  fun (a : α) ↦
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
Tactic: have : (fun a => κ a (Set.univ \ Prod.mk a ⁻¹' t)) =
        fun a => κ a Set.univ - κ a (Prod.mk a ⁻¹' t) := by
      ext1 a
      rw [← Set.diff_inter_self_eq_diff, Set.inter_univ, measure_diff (Set.subset_univ _)]
      · exact (measurable_prodMk_left htm).nullMeasurableSet
      · exact measure_ne_top _ _
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t_1 : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t : Set (α × β)
htm : MeasurableSet t
iht :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
this :
  Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (univ \ Prod.mk a ⁻¹' t))
    fun (a : α) ↦
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (univ \ Prod.mk a ⁻¹' t)
have compl : Measurable (β := ℝ≥0∞) fun (a : α) ↦
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf :
  ∀ (i : ℕ),
    Measurable (β := ℝ≥0∞) fun (a : α) ↦
      (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' f i)
a : α
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' f i) : ℝ≥0∞)
have hn : Pairwise (α := ℕ) (onFun.{1, u_2 + 1, 1} (β := Set β) Disjoint fun (i : ℕ) ↦ Prod.mk a ⁻¹' f i)
Tactic: rw [preimage_iUnion, measure_iUnion]
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf :
  ∀ (i : ℕ),
    Measurable (β := ℝ≥0∞) fun (a : α) ↦
      (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' f i)
a : α
hn : Pairwise (α := ℕ) (onFun.{1, u_2 + 1, 1} (β := Set β) Disjoint fun (i : ℕ) ↦ Prod.mk a ⁻¹' f i)
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' f i) : ℝ≥0∞)
have h : ∀ (i : ℕ), MeasurableSet (Prod.mk a ⁻¹' f i)
Tactic: rw [preimage_iUnion, measure_iUnion]
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf :
  ∀ (i : ℕ),
    Measurable (β := ℝ≥0∞) fun (a : α) ↦
      (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' f i)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i)
have this : ∀ (a : α),
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' f i) : ℝ≥0∞)
Tactic: have (a : α) : κ a (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' i, κ a (Prod.mk a ⁻¹' f i) := by
      rw [preimage_iUnion, measure_iUnion]
      · exact h_disj.mono fun _ _ ↦ .preimage _
      · exact fun i ↦ measurable_prodMk_left (hf_meas i)
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
have empty : Measurable (β := ℝ≥0∞) fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' ∅)
Tactic: induction t, ht
    using MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod with
  | empty => simp only [preimage_empty, measure_empty, measurable_const]
  | basic t ht =>
    simp only [Set.mem_image2, Set.mem_setOf_eq] at ht
    obtain ⟨t₁, ht₁, t₂, ht₂, rfl⟩ := ht
    classical
    simp_rw [mk_preimage_prod_right_eq_if]
    have h_eq_ite : (fun a => κ a (ite (a ∈ t₁) t₂ ∅)) = fun a => ite (a ∈ t₁) (κ a t₂) 0 := by
      ext1 a
      split_ifs
      exacts [rfl, measure_empty]
    rw [h_eq_ite]
    exact Measurable.ite ht₁ (Kernel.measurable_coe κ ht₂) measurable_const
  | compl t htm iht =>
    have h_eq_sdiff : ∀ a, Prod.mk a ⁻¹' tᶜ = Set.univ \ Prod.mk a ⁻¹' t := by
      intro a
      ext1 b
      simp only [mem_compl_iff, mem_preimage, mem_diff, mem_univ, true_and]
    simp_rw [h_eq_sdiff]
    have : (fun a => κ a (Set.univ \ Prod.mk a ⁻¹' t)) =
        fun a => κ a Set.univ - κ a (Prod.mk a ⁻¹' t) := by
      ext1 a
      rw [← Set.diff_inter_self_eq_diff, Set.inter_univ, measure_diff (Set.subset_univ _)]
      · exact (measurable_prodMk_left htm).nullMeasurableSet
      · exact measure_ne_top _ _
    rw [this]
    exact Measurable.sub (Kernel.measurable_coe κ MeasurableSet.univ) iht
  | iUnion f h_disj hf_meas hf =>
    have (a : α) : κ a (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' i, κ a (Prod.mk a ⁻¹' f i) := by
      rw [preimage_iUnion, measure_iUnion]
      · exact h_disj.mono fun _ _ ↦ .preimage _
      · exact fun i ↦ measurable_prodMk_left (hf_meas i)
    simpa only [this] using Measurable.tsum hf
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
empty :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' ∅)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
have basic : ∀ (t : Set (α × β))
  (ht :
    Membership.mem (γ := Set (Set (α × β)))
      (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
      t),
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
Tactic: induction t, ht
    using MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod with
  | empty => simp only [preimage_empty, measure_empty, measurable_const]
  | basic t ht =>
    simp only [Set.mem_image2, Set.mem_setOf_eq] at ht
    obtain ⟨t₁, ht₁, t₂, ht₂, rfl⟩ := ht
    classical
    simp_rw [mk_preimage_prod_right_eq_if]
    have h_eq_ite : (fun a => κ a (ite (a ∈ t₁) t₂ ∅)) = fun a => ite (a ∈ t₁) (κ a t₂) 0 := by
      ext1 a
      split_ifs
      exacts [rfl, measure_empty]
    rw [h_eq_ite]
    exact Measurable.ite ht₁ (Kernel.measurable_coe κ ht₂) measurable_const
  | compl t htm iht =>
    have h_eq_sdiff : ∀ a, Prod.mk a ⁻¹' tᶜ = Set.univ \ Prod.mk a ⁻¹' t := by
      intro a
      ext1 b
      simp only [mem_compl_iff, mem_preimage, mem_diff, mem_univ, true_and]
    simp_rw [h_eq_sdiff]
    have : (fun a => κ a (Set.univ \ Prod.mk a ⁻¹' t)) =
        fun a => κ a Set.univ - κ a (Prod.mk a ⁻¹' t) := by
      ext1 a
      rw [← Set.diff_inter_self_eq_diff, Set.inter_univ, measure_diff (Set.subset_univ _)]
      · exact (measurable_prodMk_left htm).nullMeasurableSet
      · exact measure_ne_top _ _
    rw [this]
    exact Measurable.sub (Kernel.measurable_coe κ MeasurableSet.univ) iht
  | iUnion f h_disj hf_meas hf =>
    have (a : α) : κ a (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' i, κ a (Prod.mk a ⁻¹' f i) := by
      rw [preimage_iUnion, measure_iUnion]
      · exact h_disj.mono fun _ _ ↦ .preimage _
      · exact fun i ↦ measurable_prodMk_left (hf_meas i)
    simpa only [this] using Measurable.tsum hf
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
ht : MeasurableSet t
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
empty :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' ∅)
basic :
  ∀ (t : Set (α × β))
    (ht :
      Membership.mem (γ := Set (Set (α × β)))
        (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
        t),
    Measurable (β := ℝ≥0∞) fun (a : α) ↦
      (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
have compl : ∀ (t : Set (α × β)) (htm : MeasurableSet t)
  (iht :
    Measurable (β := ℝ≥0∞) fun (a : α) ↦
      (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)),
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' tᶜ)
Tactic: induction t, ht
    using MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod with
  | empty => simp only [preimage_empty, measure_empty, measurable_const]
  | basic t ht =>
    simp only [Set.mem_image2, Set.mem_setOf_eq] at ht
    obtain ⟨t₁, ht₁, t₂, ht₂, rfl⟩ := ht
    classical
    simp_rw [mk_preimage_prod_right_eq_if]
    have h_eq_ite : (fun a => κ a (ite (a ∈ t₁) t₂ ∅)) = fun a => ite (a ∈ t₁) (κ a t₂) 0 := by
      ext1 a
      split_ifs
      exacts [rfl, measure_empty]
    rw [h_eq_ite]
    exact Measurable.ite ht₁ (Kernel.measurable_coe κ ht₂) measurable_const
  | compl t htm iht =>
    have h_eq_sdiff : ∀ a, Prod.mk a ⁻¹' tᶜ = Set.univ \ Prod.mk a ⁻¹' t := by
      intro a
      ext1 b
      simp only [mem_compl_iff, mem_preimage, mem_diff, mem_univ, true_and]
    simp_rw [h_eq_sdiff]
    have : (fun a => κ a (Set.univ \ Prod.mk a ⁻¹' t)) =
        fun a => κ a Set.univ - κ a (Prod.mk a ⁻¹' t) := by
      ext1 a
      rw [← Set.diff_inter_self_eq_diff, Set.inter_univ, measure_diff (Set.subset_univ _)]
      · exact (measurable_prodMk_left htm).nullMeasurableSet
      · exact measure_ne_top _ _
    rw [this]
    exact Measurable.sub (Kernel.measurable_coe κ MeasurableSet.univ) iht
  | iUnion f h_disj hf_meas hf =>
    have (a : α) : κ a (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' i, κ a (Prod.mk a ⁻¹' f i) := by
      rw [preimage_iUnion, measure_iUnion]
      · exact h_disj.mono fun _ _ ↦ .preimage _
      · exact fun i ↦ measurable_prodMk_left (hf_meas i)
    simpa only [this] using Measurable.tsum hf
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
have rw : Measurable (β := ℝ≥0∞) fun (a : α) ↦
  (((Kernel.sum κ.seq : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
Tactic: rw [← Kernel.kernel_sum_seq κ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((Kernel.sum κ.seq : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
have this : ∀ (a : α),
  Eq (α := ℝ≥0∞)
    ((((Kernel.sum κ.seq : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
    (∑' (n : ℕ), (((κ.seq n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
Tactic: have (a : _) : Kernel.sum (Kernel.seq κ) a (Prod.mk a ⁻¹' t) =
      ∑' n, Kernel.seq κ n a (Prod.mk a ⁻¹' t) :=
    Kernel.sum_apply' _ _ (measurable_prodMk_left ht)
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞)
      ((((Kernel.sum κ.seq : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
      (∑' (n : ℕ), (((κ.seq n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((Kernel.sum κ.seq : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
have simp_rw : Measurable (β := ℝ≥0∞) fun (a : α) ↦
  ∑' (n : ℕ), (((κ.seq n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
Tactic: simp_rw [this]
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞)
      ((((Kernel.sum κ.seq : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
      (∑' (n : ℕ), (((κ.seq n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    ∑' (n : ℕ), (((κ.seq n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
have refine : ∀ (n : ℕ),
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ.seq n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
Tactic: refine Measurable.tsum fun n => ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
inst : IsSFiniteKernel η
s : Set (β × γ)
hs : MeasurableSet s
a : α
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
have this : ∀ (b : β),
  Prod.mk b ⁻¹' s = {c : γ | Membership.mem (γ := Set ((α × β) × γ)) {p : (α × β) × γ | (p.1.2, p.2) ∈ s} ((a, b), c)}
Tactic: have (b : _) : Prod.mk b ⁻¹' s = {c | ((a, b), c) ∈ {p : (α × β) × γ | (p.1.2, p.2) ∈ s}} := rfl
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
inst : IsSFiniteKernel η
s : Set (β × γ)
hs : MeasurableSet s
a : α
this :
  ∀ (b : β),
    Prod.mk b ⁻¹' s = {c : γ | Membership.mem (γ := Set ((α × β) × γ)) {p : (α × β) × γ | (p.1.2, p.2) ∈ s} ((a, b), c)}
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
have simp_rw : Measurable (β := ℝ≥0∞) fun (b : β) ↦
  (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
    {c : γ | Membership.mem (γ := Set ((α × β) × γ)) {p : (α × β) × γ | (p.1.2, p.2) ∈ s} ((a, b), c)}
Tactic: simp_rw [this]
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
inst : IsSFiniteKernel η
s : Set (β × γ)
hs : MeasurableSet s
a : α
this :
  ∀ (b : β),
    Prod.mk b ⁻¹' s = {c : γ | Membership.mem (γ := Set ((α × β) × γ)) {p : (α × β) × γ | (p.1.2, p.2) ∈ s} ((a, b), c)}
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      {c : γ | Membership.mem (γ := Set ((α × β) × γ)) {p : (α × β) × γ | (p.1.2, p.2) ∈ s} ((a, b), c)}
have refine : MeasurableSet (α := (α × β) × γ) {p : (α × β) × γ | (p.1.2, p.2) ∈ s}
Tactic: refine (measurable_kernel_prodMk_left ?_).comp measurable_prodMk_left
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
c : ℝ≥0∞
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    ∫⁻ (b : β), t.indicator (Function.const (α × β) c) (a, b) ∂(κ : (a : α) → Measure β) a
have unfold : Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), t.indicator (fun (x : α × β) ↦ c) (a, b) ∂(κ : (a : α) → Measure β) a
Tactic: unfold Function.const
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
c : ℝ≥0∞
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), t.indicator (fun (x : α × β) ↦ c) (a, b) ∂(κ : (a : α) → Measure β) a
have simp_rw : Measurable (β := ℝ≥0∞) fun (a : α) ↦
  HMul.hMul (β := ℝ≥0∞) c ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
Tactic: simp_rw [lintegral_indicator_const_comp measurable_prodMk_left ht _]
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), f a b ∂(κ : (a : α) → Measure β) a
have h : ∀ (a : α × β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) a = uncurry f a
Tactic: have h : ∀ a, ⨆ n, F n a = uncurry f a := SimpleFunc.iSup_eapprox_apply hf
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α × β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) a = uncurry f a
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), f a b ∂(κ : (a : α) → Measure β) a
have h₁ : ∀ (a : α) (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) = f a b
Tactic: simp only [Prod.forall, uncurry_apply_pair] at h
Cleared hypotheses: h