awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
n : ℕ
x : E
h : x ∈ (s n).range
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x_1 : α) ↦
    Measure.real.{u_2} (α := β) (m := mβ) ((κ : (a : α) → Measure β) x_1)
        (preimage (β := E) (⇑(s n) : (a : β) → E) {x}) •
      x
have pos : Measurable (β := ℝ≥0∞) fun (x_1 : α) ↦
  (((κ : (a : α) → Measure β) x_1 : Measure β) : (a : Set β) → ℝ≥0∞) (preimage (β := E) (⇑(s n) : (a : β) → E) {x})
Tactic: refine (Measurable.ennreal_toReal ?_).stronglyMeasurable.smul_const _
-- 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 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
⊢ Tendsto f' atTop (𝓝 fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y)
have pos : ∀ (x : α),
  Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y))
Tactic: rw [tendsto_pi_nhds]
-- 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 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
x : α
⊢ Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y))
have pos : ∀ (hfx : @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)),
  Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y))
Tactic: by_cases hfx : Integrable f (κ x)
-- 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 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
x : α
pos :
  ∀ (hfx : @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)),
    Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
      (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y))
⊢ Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y))
have neg : ∀ (hfx : ¬@Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)),
  Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y))
Tactic: by_cases hfx : Integrable f (κ x)
-- 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 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
x : α
hfx : @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)
⊢ Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y))
have pos : Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s i)) atTop
  (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y))
Tactic: simp only [mem_setOf_eq, hfx, indicator_of_mem, f']
-- 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 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : (n : ℕ) → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n)
x : α
hfx : @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)
⊢ Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s i)) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y))
have pos : range f ∪ {0} ⊆ range f ∪ {0}
Tactic: apply tendsto_integral_approxOn_of_measurable_of_range_subset _ hfx
-- 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 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
have pos : ∀ (hE : CompleteSpace E),
  StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
Tactic: classical
  by_cases hE : CompleteSpace E; swap
  · simp [integral, hE, stronglyMeasurable_const]
  borelize E
  have : TopologicalSpace.SeparableSpace (range f ∪ {0} : Set E) :=
    hf.separableSpace_range_union_singleton
  let s : ℕ → SimpleFunc β E := SimpleFunc.approxOn _ hf.measurable (range f ∪ {0}) 0 (by simp)
  let f' n : α → E := {x | Integrable f (κ x)}.indicator fun x ↦ (s n).integral (κ x)
  refine stronglyMeasurable_of_tendsto (f := f') atTop (fun n ↦ ?_) ?_
  · refine StronglyMeasurable.indicator ?_ (measurableSet_integrable hf)
    simp_rw [SimpleFunc.integral_eq]
    refine Finset.stronglyMeasurable_fun_sum _ fun _ _ ↦ ?_
    refine (Measurable.ennreal_toReal ?_).stronglyMeasurable.smul_const _
    exact κ.measurable_coe ((s n).measurableSet_fiber _)
  · rw [tendsto_pi_nhds]; intro x
    by_cases hfx : Integrable f (κ x)
    · simp only [mem_setOf_eq, hfx, indicator_of_mem, f']
      apply tendsto_integral_approxOn_of_measurable_of_range_subset _ hfx
      exact subset_rfl
    · 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 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
pos :
  ∀ (hE : CompleteSpace E),
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
have neg : ∀ (hE : ¬CompleteSpace E),
  StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
Tactic: classical
  by_cases hE : CompleteSpace E; swap
  · simp [integral, hE, stronglyMeasurable_const]
  borelize E
  have : TopologicalSpace.SeparableSpace (range f ∪ {0} : Set E) :=
    hf.separableSpace_range_union_singleton
  let s : ℕ → SimpleFunc β E := SimpleFunc.approxOn _ hf.measurable (range f ∪ {0}) 0 (by simp)
  let f' n : α → E := {x | Integrable f (κ x)}.indicator fun x ↦ (s n).integral (κ x)
  refine stronglyMeasurable_of_tendsto (f := f') atTop (fun n ↦ ?_) ?_
  · refine StronglyMeasurable.indicator ?_ (measurableSet_integrable hf)
    simp_rw [SimpleFunc.integral_eq]
    refine Finset.stronglyMeasurable_fun_sum _ fun _ _ ↦ ?_
    refine (Measurable.ennreal_toReal ?_).stronglyMeasurable.smul_const _
    exact κ.measurable_coe ((s n).measurableSet_fiber _)
  · rw [tendsto_pi_nhds]; intro x
    by_cases hfx : Integrable f (κ x)
    · simp only [mem_setOf_eq, hfx, indicator_of_mem, f']
      apply tendsto_integral_approxOn_of_measurable_of_range_subset _ hfx
      exact subset_rfl
    · 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 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
pos :
  ∀ (hE : CompleteSpace E),
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
neg :
  ∀ (hE : ¬CompleteSpace E),
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
pos₁ :
  ∀ (hE : CompleteSpace E),
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
neg₁ neg₂ :
  ∀ (hE : ¬CompleteSpace E),
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
pos₂ pos₃ :
  ∀ (hE : CompleteSpace E),
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
have pos₄ : ∀ (hE : CompleteSpace E),
  let this := borel E;
  BorelSpace E →
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
Tactic: classical
  by_cases hE : CompleteSpace E; swap
  · simp [integral, hE, stronglyMeasurable_const]
  borelize E
  have : TopologicalSpace.SeparableSpace (range f ∪ {0} : Set E) :=
    hf.separableSpace_range_union_singleton
  let s : ℕ → SimpleFunc β E := SimpleFunc.approxOn _ hf.measurable (range f ∪ {0}) 0 (by simp)
  let f' n : α → E := {x | Integrable f (κ x)}.indicator fun x ↦ (s n).integral (κ x)
  refine stronglyMeasurable_of_tendsto (f := f') atTop (fun n ↦ ?_) ?_
  · refine StronglyMeasurable.indicator ?_ (measurableSet_integrable hf)
    simp_rw [SimpleFunc.integral_eq]
    refine Finset.stronglyMeasurable_fun_sum _ fun _ _ ↦ ?_
    refine (Measurable.ennreal_toReal ?_).stronglyMeasurable.smul_const _
    exact κ.measurable_coe ((s n).measurableSet_fiber _)
  · rw [tendsto_pi_nhds]; intro x
    by_cases hfx : Integrable f (κ x)
    · simp only [mem_setOf_eq, hfx, indicator_of_mem, f']
      apply tendsto_integral_approxOn_of_measurable_of_range_subset _ hfx
      exact subset_rfl
    · 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 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
pos :
  ∀ (hE : CompleteSpace E),
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
neg :
  ∀ (hE : ¬CompleteSpace E),
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
pos₁ :
  ∀ (hE : CompleteSpace E),
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
neg₁ neg₂ :
  ∀ (hE : ¬CompleteSpace E),
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
pos₂ pos₃ :
  ∀ (hE : CompleteSpace E),
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
pos₄ :
  ∀ (hE : CompleteSpace E),
    let this := borel E;
    BorelSpace E →
      StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
        @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
have pos₅ : ∀ (hE : CompleteSpace E),
  let this := borel E;
  BorelSpace E →
    ∀ (this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)),
      StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
        @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
Tactic: classical
  by_cases hE : CompleteSpace E; swap
  · simp [integral, hE, stronglyMeasurable_const]
  borelize E
  have : TopologicalSpace.SeparableSpace (range f ∪ {0} : Set E) :=
    hf.separableSpace_range_union_singleton
  let s : ℕ → SimpleFunc β E := SimpleFunc.approxOn _ hf.measurable (range f ∪ {0}) 0 (by simp)
  let f' n : α → E := {x | Integrable f (κ x)}.indicator fun x ↦ (s n).integral (κ x)
  refine stronglyMeasurable_of_tendsto (f := f') atTop (fun n ↦ ?_) ?_
  · refine StronglyMeasurable.indicator ?_ (measurableSet_integrable hf)
    simp_rw [SimpleFunc.integral_eq]
    refine Finset.stronglyMeasurable_fun_sum _ fun _ _ ↦ ?_
    refine (Measurable.ennreal_toReal ?_).stronglyMeasurable.smul_const _
    exact κ.measurable_coe ((s n).measurableSet_fiber _)
  · rw [tendsto_pi_nhds]; intro x
    by_cases hfx : Integrable f (κ x)
    · simp only [mem_setOf_eq, hfx, indicator_of_mem, f']
      apply tendsto_integral_approxOn_of_measurable_of_range_subset _ hfx
      exact subset_rfl
    · 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: by_cases hE : CompleteSpace E
-- 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)
pos :
  ∀ (hE : CompleteSpace E),
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y
have neg : ∀ (hE : ¬CompleteSpace E),
  StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y
Tactic: by_cases hE : CompleteSpace E
-- 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
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- 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 : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y
have this : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
Tactic: haveI : TopologicalSpace.SeparableSpace (range (uncurry f) ∪ {0} : Set E) :=
    hf.separableSpace_range_union_singleton
-- 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)
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)
n : ℕ
⊢ StronglyMeasurable (f' n)
have refine : StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦ SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
Tactic: refine StronglyMeasurable.indicator ?_ (measurableSet_kernel_integrable hf)
-- 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)
n : ℕ
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦ SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
have this₁ : ∀ (x : α), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
Tactic: 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 _ _)
-- 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)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : 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)
n : ℕ
this : ∀ (x : α), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦ SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
have simp : StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
  ∑ x_1 ∈ (s n).range,
    Measure.real.{u_2} (α := β) (m := mβ) ((κ : (a : α) → Measure β) x)
        (preimage (β := E) (⇑(s' n x) : (a : β) → E) {x_1}) •
      x_1
Tactic: simp only [SimpleFunc.integral_eq_sum_of_subset (this _)]
-- 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)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : 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)
n : ℕ
this : ∀ (x : α), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    ∑ x_1 ∈ (s n).range,
      Measure.real.{u_2} (α := β) (m := mβ) ((κ : (a : α) → Measure β) x)
          (preimage (β := E) (⇑(s' n x) : (a : β) → E) {x_1}) •
        x_1
have refine : ∀ x ∈ (s n).range,
  StronglyMeasurable.{u_1, u_4} (β := E) fun (x_2 : α) ↦
    Measure.real.{u_2} (α := β) (m := mβ) ((κ : (a : α) → Measure β) x_2)
        (preimage (β := E) (⇑(s' n x_2) : (a : β) → E) {x}) •
      x
Tactic: refine Finset.stronglyMeasurable_fun_sum _ fun x _ => ?_