awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableIntegral (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y
have h2f' : Tendsto f' atTop (𝓝 fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y)
Tactic: have h2f' : Tendsto f' atTop (𝓝 fun x : α => ∫ y : β, f x y ∂κ x) := by
    rw [tendsto_pi_nhds]; intro x
    by_cases hfx : Integrable (f x) (κ x)
    · have (n : _) : Integrable (s' n x) (κ x) := by
        apply (hfx.norm.add hfx.norm).mono' (s' n x).aestronglyMeasurable
        filter_upwards with y
        simp_rw [s', SimpleFunc.coe_comp]; exact SimpleFunc.norm_approxOn_zero_le _ _ (x, y) n
      simp only [f', hfx, SimpleFunc.integral_eq_integral _ (this _), indicator_of_mem,
        mem_setOf_eq]
      refine
        tendsto_integral_of_dominated_convergence (fun y => ‖f x y‖ + ‖f x y‖)
          (fun n => (s' n x).aestronglyMeasurable) (hfx.norm.add hfx.norm) ?_ ?_
      · -- Porting note: was
        -- exact fun n => Eventually.of_forall fun y =>
        --   SimpleFunc.norm_approxOn_zero_le _ _ (x, y) n
        exact fun n => Eventually.of_forall fun y =>
          SimpleFunc.norm_approxOn_zero_le hf.measurable (by simp) (x, y) n
      · refine Eventually.of_forall fun y => SimpleFunc.tendsto_approxOn hf.measurable (by simp) ?_
        apply subset_closure
        simp [-uncurry_apply_pair]
    · simp [f', hfx, integral_undef]
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y
have pos : ∀ (hE : CompleteSpace E),
  StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y
Tactic: classical
  by_cases hE : CompleteSpace E; swap
  · simp [integral, hE, stronglyMeasurable_const]
  borelize E
  haveI : TopologicalSpace.SeparableSpace (range (uncurry f) ∪ {0} : Set E) :=
    hf.separableSpace_range_union_singleton
  let s : ℕ → SimpleFunc (α × β) E :=
    SimpleFunc.approxOn _ hf.measurable (range (uncurry f) ∪ {0}) 0 (by simp)
  let s' : ℕ → α → SimpleFunc β E := fun n x => (s n).comp (Prod.mk x) measurable_prodMk_left
  let f' : ℕ → α → E := fun n =>
    {x | Integrable (f x) (κ x)}.indicator fun x => (s' n x).integral (κ x)
  have hf' : ∀ n, StronglyMeasurable (f' n) := by
    intro n; refine StronglyMeasurable.indicator ?_ (measurableSet_kernel_integrable hf)
    have : ∀ x, ((s' n x).range.filter fun x => x ≠ 0) ⊆ (s n).range := by
      intro
      exact Finset.Subset.trans (Finset.filter_subset _ _) (SimpleFunc.range_comp_subset_range _ _)
    simp only [SimpleFunc.integral_eq_sum_of_subset (this _)]
    refine Finset.stronglyMeasurable_fun_sum _ fun x _ => ?_
    refine (Measurable.ennreal_toReal ?_).stronglyMeasurable.smul_const _
    simp only [s', SimpleFunc.coe_comp, preimage_comp]
    apply Kernel.measurable_kernel_prodMk_left
    exact (s n).measurableSet_fiber x
  have h2f' : Tendsto f' atTop (𝓝 fun x : α => ∫ y : β, f x y ∂κ x) := by
    rw [tendsto_pi_nhds]; intro x
    by_cases hfx : Integrable (f x) (κ x)
    · have (n : _) : Integrable (s' n x) (κ x) := by
        apply (hfx.norm.add hfx.norm).mono' (s' n x).aestronglyMeasurable
        filter_upwards with y
        simp_rw [s', SimpleFunc.coe_comp]; exact SimpleFunc.norm_approxOn_zero_le _ _ (x, y) n
      simp only [f', hfx, SimpleFunc.integral_eq_integral _ (this _), indicator_of_mem,
        mem_setOf_eq]
      refine
        tendsto_integral_of_dominated_convergence (fun y => ‖f x y‖ + ‖f x y‖)
          (fun n => (s' n x).aestronglyMeasurable) (hfx.norm.add hfx.norm) ?_ ?_
      · -- Porting note: was
        -- exact fun n => Eventually.of_forall fun y =>
        --   SimpleFunc.norm_approxOn_zero_le _ _ (x, y) n
        exact fun n => Eventually.of_forall fun y =>
          SimpleFunc.norm_approxOn_zero_le hf.measurable (by simp) (x, y) n
      · refine Eventually.of_forall fun y => SimpleFunc.tendsto_approxOn hf.measurable (by simp) ?_
        apply subset_closure
        simp [-uncurry_apply_pair]
    · simp [f', hfx, integral_undef]
  exact stronglyMeasurable_of_tendsto _ hf' h2f'
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableIntegral (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α × β → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f (x, y)
have hf₁ : StronglyMeasurable (uncurry (Function.curry f))
Tactic: rw [← uncurry_curry f] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
E : Type u_4
inst : NormedAddCommGroup E
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
inst_2 : NormedSpace ℝ E
f : β × γ → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable.{u_2, u_4} (β := E) fun (x : β) ↦
    @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y)
have x : StronglyMeasurable.{u_2, u_4} (α := β) (β := E)
  ((fun (x : α × β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) x) fun (y : γ) ↦
        (fun (u : (α × β) × γ) ↦ f (u.1.2, u.2)) (x, y)) ∘
    fun (x : β) ↦ (a, x))
Tactic: change
    StronglyMeasurable
      ((fun x => ∫ y, (fun u : (α × β) × γ => f (u.1.2, u.2)) (x, y) ∂η x) ∘ fun x => (a, x))
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
E : Type u_4
inst : NormedAddCommGroup E
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
inst_2 : NormedSpace ℝ E
f : β × γ → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable.{u_2, u_4} (α := β) (β := E)
    ((fun (x : α × β) ↦
        @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) x) fun (y : γ) ↦
          (fun (u : (α × β) × γ) ↦ f (u.1.2, u.2)) (x, y)) ∘
      fun (x : β) ↦ (a, x))
have apply : StronglyMeasurable (β := E) fun (x : α × β) ↦
  @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) x) fun (y : γ) ↦ (fun (u : (α × β) × γ) ↦ f (u.1.2, u.2)) (x, y)
Tactic: apply StronglyMeasurable.comp_measurable _ (measurable_prodMk_left (m := mα))
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableIntegral (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
E : Type u_4
inst : NormedAddCommGroup E
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
inst_2 : NormedSpace ℝ E
f : β × γ → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable (β := E) fun (x : α × β) ↦
    @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) x) fun (y : γ) ↦ (fun (u : (α × β) × γ) ↦ f (u.1.2, u.2)) (x, y)
have this : StronglyMeasurable (β := E) fun (x : α × β) ↦
  @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) x) fun (y : γ) ↦ (f ∘ fun (a : (α × β) × γ) ↦ (a.1.2, a.2)) (x, y)
Tactic: have := MeasureTheory.StronglyMeasurable.integral_kernel_prod_right' (κ := η)
      (hf.comp_measurable (measurable_fst.snd.prodMk measurable_snd))
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
E : Type u_4
inst : NormedAddCommGroup E
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
inst_2 : NormedSpace ℝ E
f : γ × β → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable.{u_2, u_4} (β := E) fun (y : β) ↦
    @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, y)) fun (x : γ) ↦ f (x, y)
have y : StronglyMeasurable.{u_2, u_4} (α := β) (β := E)
  ((fun (y : α × β) ↦
      @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) y) fun (x : γ) ↦
        (fun (u : γ × α × β) ↦ f (u.1, u.2.2)) (x, y)) ∘
    fun (x : β) ↦ (a, x))
Tactic: change
    StronglyMeasurable
      ((fun y => ∫ x, (fun u : γ × α × β => f (u.1, u.2.2)) (x, y) ∂η y) ∘ fun x => (a, x))
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
E : Type u_4
inst : NormedAddCommGroup E
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
inst_2 : NormedSpace ℝ E
f : γ × β → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable.{u_2, u_4} (α := β) (β := E)
    ((fun (y : α × β) ↦
        @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) y) fun (x : γ) ↦
          (fun (u : γ × α × β) ↦ f (u.1, u.2.2)) (x, y)) ∘
      fun (x : β) ↦ (a, x))
have apply : StronglyMeasurable (β := E) fun (y : α × β) ↦
  @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) y) fun (x : γ) ↦ (fun (u : γ × α × β) ↦ f (u.1, u.2.2)) (x, y)
Tactic: apply StronglyMeasurable.comp_measurable _ (measurable_prodMk_left (m := mα))
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableIntegral (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
E : Type u_4
inst : NormedAddCommGroup E
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
inst_2 : NormedSpace ℝ E
f : γ × β → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable (β := E) fun (y : α × β) ↦
    @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) y) fun (x : γ) ↦ (fun (u : γ × α × β) ↦ f (u.1, u.2.2)) (x, y)
have this : StronglyMeasurable (β := E) fun (y : α × β) ↦
  @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) y) fun (x : γ) ↦ (f ∘ fun (a : γ × α × β) ↦ (a.1, a.2.2)) (x, y)
Tactic: have := MeasureTheory.StronglyMeasurable.integral_kernel_prod_left' (κ := η)
      (hf.comp_measurable (measurable_fst.prodMk measurable_snd.snd))
-- 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 (α × β)
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)
have ht₁ : ∃ (a : Set α), MeasurableSet a ∧ ∃ (b : Set β), MeasurableSet b ∧ a ×ˢ b = t
Tactic: simp only [Set.mem_image2, Set.mem_setOf_eq] at ht
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_1 : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t : Set (α × β)
ht : ∃ (a : Set α), MeasurableSet a ∧ ∃ (b : Set β), MeasurableSet b ∧ a ×ˢ b = t
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
have basic : ∀ (t₁ : Set α) (ht₁ : MeasurableSet t₁) (t₂ : Set β) (ht₂ : MeasurableSet t₂),
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t₁ ×ˢ t₂)
Tactic: obtain ⟨t₁, ht₁, t₂, ht₂, rfl⟩ := ht
Cleared hypotheses: t, 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 (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t₁ ×ˢ t₂)
have basic : Measurable (β := ℝ≥0∞) fun (a : α) ↦
  (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅)
Tactic: simp_rw [mk_preimage_prod_right_eq_if]
-- 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)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
⊢ Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅))
    fun (a : α) ↦ if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0
have h : ∀ (a : α),
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅) : ℝ≥0∞)
    (if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0 : ℝ≥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 : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
a : α
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅) : ℝ≥0∞)
    (if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0 : ℝ≥0∞)
have pos : a ∈ t₁ →
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ : ℝ≥0∞)
Tactic: split_ifs
-- 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)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
a : α
pos :
  a ∈ t₁ →
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅) : ℝ≥0∞)
    (if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0 : ℝ≥0∞)
have neg : a ∉ t₁ → Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) ∅) 0
Tactic: split_ifs
-- 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)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅)
have h_eq_ite : Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
  (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅))
  fun (a : α) ↦ if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0
Tactic: 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]
-- 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)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
h_eq_ite :
  Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅))
    fun (a : α) ↦ if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅)
have basic : Measurable (β := ℝ≥0∞) fun (a : α) ↦
  if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0
Tactic: rw [h_eq_ite]
-- 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)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t₁ ×ˢ t₂)
have basic : Measurable (β := ℝ≥0∞) fun (a : α) ↦
  (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅)
Tactic: 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
-- 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)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
basic :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t₁ ×ˢ t₂)
have basic₁ : ∀
  (h_eq_ite :
    Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
      (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅))
      fun (a : α) ↦ if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0),
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅)
Tactic: 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
-- 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)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
basic :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅)
basic₁ :
  ∀
    (h_eq_ite :
      Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
        (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅))
        fun (a : α) ↦ if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0),
    Measurable (β := ℝ≥0∞) fun (a : α) ↦
      (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t₁ ×ˢ t₂)
have basic₂ : ∀
  (h_eq_ite :
    Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
      (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅))
      fun (a : α) ↦ if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0),
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0
Tactic: 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
-- 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)
a : α
⊢ Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
have h : ∀ (b : β), b ∈ Prod.mk a ⁻¹' tᶜ ↔ b ∈ univ \ Prod.mk a ⁻¹' t
Tactic: ext1 b
-- 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)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' tᶜ)
have h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
Tactic: 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]
-- 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
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' tᶜ)
have compl : Measurable (β := ℝ≥0∞) fun (a : α) ↦
  (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (univ \ Prod.mk a ⁻¹' t)
Tactic: simp_rw [h_eq_sdiff]