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 : 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
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 x_1) : (a : β) → E) {x}) •
      x
have refine : Measurable (β := ℝ≥0∞) fun (x_1 : α) ↦
  (((κ : (a : α) → Measure β) x_1 : Measure β) : (a : Set β) → ℝ≥0∞) (preimage (β := E) (⇑(s' n x_1) : (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 : 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
x : E
h : x ∈ (s n).range
⊢ Measurable (β := ℝ≥0∞) fun (x_1 : α) ↦
    (((κ : (a : α) → Measure β) x_1 : Measure β) : (a : Set β) → ℝ≥0∞)
      (preimage (β := E) (⇑(s' n x_1) : (a : β) → E) {x})
have simp : Measurable (β := ℝ≥0∞) fun (x_1 : α) ↦
  (((κ : (a : α) → Measure β) x_1 : Measure β) : (a : Set β) → ℝ≥0∞)
    (Prod.mk x_1 ⁻¹' preimage (β := E) (⇑(s n) : (a : α × β) → E) {x})
Tactic: simp only [s', SimpleFunc.coe_comp, preimage_comp]
-- 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
x : E
h : x ∈ (s n).range
⊢ Measurable (β := ℝ≥0∞) fun (x_1 : α) ↦
    (((κ : (a : α) → Measure β) x_1 : Measure β) : (a : Set β) → ℝ≥0∞)
      (Prod.mk x_1 ⁻¹' preimage (β := E) (⇑(s n) : (a : α × β) → E) {x})
have ht : MeasurableSet (α := α × β) (preimage (β := E) (⇑(s n) : (a : α × β) → E) {x})
Tactic: apply Kernel.measurable_kernel_prodMk_left
-- 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)
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y
have hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
Tactic: 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
-- 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)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
⊢ Tendsto f' atTop (𝓝 fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y)
have rw : ∀ (x : α),
  Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x 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 : 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)
x : α
⊢ Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y))
have pos : ∀ (hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)),
  Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y))
Tactic: by_cases hfx : Integrable (f x) (κ 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 : 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)
x : α
pos :
  ∀ (hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)),
    Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
      (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y))
⊢ Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y))
have neg : ∀ (hfx : ¬@Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)),
  Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y))
Tactic: by_cases hfx : Integrable (f x) (κ 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 : 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)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
n : ℕ
⊢ @Integrable.{u_4, u_2} E _ _ β mβ (⇑(s' n x) : (a : β) → E) ((κ : (a : α) → Measure β) x)
have apply : ∀ᵐ (a : β) ∂((κ : (a : α) → Measure β) x : Measure β),
  norm.{u_4} (E := E) ((s' n x : (a : β) → E) a : E) ≤
    HAdd.hAdd (α := β → ℝ) (β := β → ℝ) (fun (a : β) ↦ ‖f x a‖) (fun (a : β) ↦ ‖f x a‖) a
Tactic: apply (hfx.norm.add hfx.norm).mono' (s' n x).aestronglyMeasurable
-- 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)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
n : ℕ
⊢ ∀ᵐ (a : β) ∂((κ : (a : α) → Measure β) x : Measure β),
    norm.{u_4} (E := E) ((s' n x : (a : β) → E) a : E) ≤
      HAdd.hAdd (α := β → ℝ) (β := β → ℝ) (fun (a : β) ↦ ‖f x a‖) (fun (a : β) ↦ ‖f x a‖) a
have h : ∀ (y : β),
  norm.{u_4} (E := E) ((s' n x : (a : β) → E) y : E) ≤
    HAdd.hAdd (α := β → ℝ) (β := β → ℝ) (fun (a : β) ↦ ‖f x a‖) (fun (a : β) ↦ ‖f x a‖) y
Tactic: filter_upwards with y
-- 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)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
n : ℕ
y : β
⊢ norm.{u_4} (E := E) ((s' n x : (a : β) → E) y : E) ≤
    HAdd.hAdd (α := β → ℝ) (β := β → ℝ) (fun (a : β) ↦ ‖f x a‖) (fun (a : β) ↦ ‖f x a‖) y
have h : norm.{u_4} (E := E) (((⇑(s n) : (a : α × β) → E) ∘ Prod.mk x) y) ≤
  HAdd.hAdd (α := β → ℝ) (β := β → ℝ) (fun (a : β) ↦ ‖f x a‖) (fun (a : β) ↦ ‖f x a‖) y
Tactic: simp_rw [s', SimpleFunc.coe_comp]
-- 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)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
⊢ Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y))
have this₁ : ∀ (n : ℕ), @Integrable.{u_4, u_2} E _ _ β mβ (⇑(s' n x) : (a : β) → E) ((κ : (a : α) → Measure β) x)
Tactic: 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
-- 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)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
this : ∀ (n : ℕ), @Integrable.{u_4, u_2} E _ _ β mβ (⇑(s' n x) : (a : β) → E) ((κ : (a : α) → Measure β) x)
⊢ Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y))
have pos : Tendsto.{0, u_4} (β := E)
  (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (x_1 : β) ↦ (s' i x : (a : β) → E) x_1) atTop
  (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y))
Tactic: simp only [f', hfx, SimpleFunc.integral_eq_integral _ (this _), indicator_of_mem,
        mem_setOf_eq]
-- 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)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
this : ∀ (n : ℕ), @Integrable.{u_4, u_2} E _ _ β mβ (⇑(s' n x) : (a : β) → E) ((κ : (a : α) → Measure β) x)
⊢ Tendsto.{0, u_4} (β := E)
    (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (x_1 : β) ↦ (s' i x : (a : β) → E) x_1) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y))
have pos : ∀ (n : ℕ),
  ∀ᵐ (a : β) ∂((κ : (a : α) → Measure β) x : Measure β),
    norm.{u_4} (E := E) ((s' n x : (a : β) → E) a : E) ≤ (fun (y : β) ↦ ‖f x y‖ + ‖f x y‖) a
Tactic: 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) ?_ ?_
-- 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)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
this : ∀ (n : ℕ), @Integrable.{u_4, u_2} E _ _ β mβ (⇑(s' n x) : (a : β) → E) ((κ : (a : α) → Measure β) x)
pos :
  ∀ (n : ℕ),
    ∀ᵐ (a : β) ∂((κ : (a : α) → Measure β) x : Measure β),
      norm.{u_4} (E := E) ((s' n x : (a : β) → E) a : E) ≤ (fun (y : β) ↦ ‖f x y‖ + ‖f x y‖) a
⊢ Tendsto.{0, u_4} (β := E)
    (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (x_1 : β) ↦ (s' i x : (a : β) → E) x_1) atTop
    (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y))
have pos₁ : ∀ᵐ (a : β) ∂((κ : (a : α) → Measure β) x : Measure β),
  Tendsto (fun (n : ℕ) ↦ (s' n x : (a : β) → E) a) atTop (𝓝 (f x a))
Tactic: 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) ?_ ?_
-- 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)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
this : ∀ (n : ℕ), @Integrable.{u_4, u_2} E _ _ β mβ (⇑(s' n x) : (a : β) → E) ((κ : (a : α) → Measure β) x)
⊢ ∀ᵐ (a : β) ∂((κ : (a : α) → Measure β) x : Measure β),
    Tendsto (fun (n : ℕ) ↦ (s' n x : (a : β) → E) a) atTop (𝓝 (f x a))
have pos : ∀ (y : β), uncurry f (x, y) ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (range (uncurry f) ∪ {0})
Tactic: refine Eventually.of_forall fun y => SimpleFunc.tendsto_approxOn hf.measurable (by simp) ?_
-- 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)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)
this : ∀ (n : ℕ), @Integrable.{u_4, u_2} E _ _ β mβ (⇑(s' n x) : (a : β) → E) ((κ : (a : α) → Measure β) x)
y : β
⊢ uncurry f (x, y) ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (range (uncurry f) ∪ {0})
have pos : uncurry f (x, y) ∈ range (uncurry f) ∪ {0}
Tactic: apply subset_closure