awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
n : ℕ
this : ∀ (x : α), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
x : E
h : x ∈ (s n).range
hs : MeasurableSet (α := α × β) (preimage (β := E) (⇑(s n) : (a : α × β) → E) {x})
⊢ Measurable (β := ℝ≥0∞) fun (x_1 : α) ↦
    (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x_1 ⁻¹' preimage (β := E) (⇑(s n) : (a : α × β) → E) {x})

Tactic:
apply measurable_measure_prodMk_left

Premises used: measurable_measure_prodMk_left
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
n : ℕ
this : ∀ (x : α), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
x : E
h : x ∈ (s n).range
⊢ MeasurableSet (α := α × β) (preimage (β := E) (⇑(s n) : (a : α × β) → E) {x})

Tactic:
(s n).measurableSet_fiber x

Premises used: MeasureTheory.SimpleFunc.measurableSet_fiber
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
n : ℕ
this : ∀ (x : α), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
x : E
h : x ∈ (s n).range
⊢ MeasurableSet (α := α × β) (preimage (β := E) (⇑(s n) : (a : α × β) → E) {x})

Tactic:
exact (s n).measurableSet_fiber x

Premises used: MeasureTheory.SimpleFunc.measurableSet_fiber
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
⊢ ∀ (n : ℕ), StronglyMeasurable (f' n)

Tactic:
have hf' : ∀ n, StronglyMeasurable (f' n) := by
    intro n; refine StronglyMeasurable.indicator ?_ (measurableSet_integrable hf)
    have : ∀ x, ((s' n x).range.filter fun x => x ≠ 0) ⊆ (s n).range := by
      intro x; refine Finset.Subset.trans (Finset.filter_subset _ _) ?_; intro y
      simp_rw [SimpleFunc.mem_range]; rintro ⟨z, rfl⟩; exact ⟨(x, z), rfl⟩
    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 measurable_measure_prodMk_left
    exact (s n).measurableSet_fiber x
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
rw : ∀ (x : α), Tendsto.{0, u_3} (β := E) (fun (i : ℕ) ↦ f' i x) atTop (𝓝 (∫ (y : β), f x y ∂ν))
⊢ Tendsto f' atTop (𝓝 fun (x : α) ↦ ∫ (y : β), f x y ∂ν)

Tactic:
rw [tendsto_pi_nhds]

Premises used: tendsto_pi_nhds
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
pos : ∀ (hfx : Integrable (f x) ν), Tendsto.{0, u_3} (β := E) (fun (i : ℕ) ↦ f' i x) atTop (𝓝 (∫ (y : β), f x y ∂ν))
neg : ∀ (hfx : ¬Integrable (f x) ν), Tendsto.{0, u_3} (β := E) (fun (i : ℕ) ↦ f' i x) atTop (𝓝 (∫ (y : β), f x y ∂ν))
⊢ Tendsto.{0, u_3} (β := E) (fun (i : ℕ) ↦ f' i x) atTop (𝓝 (∫ (y : β), f x y ∂ν))

Tactic:
by_cases hfx : Integrable (f x) ν

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) ν
n : ℕ
apply :
  ∀ᵐ (a : β) ∂ν,
    Norm.norm.{u_3} (E := E) ((s' n x : (a : β) → E) a : E) ≤
      HAdd.hAdd (α := β → ℝ) (β := β → ℝ) (fun (a : β) ↦ ‖f x a‖) (fun (a : β) ↦ ‖f x a‖) a
⊢ Integrable.{u_3, u_2} (ε := E) (⇑(s' n x) : (a : β) → E) ν

Tactic:
apply (hfx.norm.add hfx.norm).mono' (s' n x).aestronglyMeasurable

Premises used: MeasureTheory.Integrable.mono', MeasureTheory.Integrable.add, MeasureTheory.SimpleFunc.aestronglyMeasurable, MeasureTheory.Integrable.norm
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) ν
n : ℕ
h :
  ∀ (y : β),
    Norm.norm.{u_3} (E := E) ((s' n x : (a : β) → E) y : E) ≤
      HAdd.hAdd (α := β → ℝ) (β := β → ℝ) (fun (a : β) ↦ ‖f x a‖) (fun (a : β) ↦ ‖f x a‖) y
⊢ ∀ᵐ (a : β) ∂ν,
    Norm.norm.{u_3} (E := E) ((s' n x : (a : β) → E) a : E) ≤
      HAdd.hAdd (α := β → ℝ) (β := β → ℝ) (fun (a : β) ↦ ‖f x a‖) (fun (a : β) ↦ ‖f x a‖) a

Tactic:
filter_upwards with y
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) ν
n : ℕ
y : β
h :
  Norm.norm.{u_3} (E := E) (((⇑(s n) : (a : α × β) → E) ∘ Prod.mk x) y) ≤
    HAdd.hAdd (α := β → ℝ) (β := β → ℝ) (fun (a : β) ↦ ‖f x a‖) (fun (a : β) ↦ ‖f x a‖) y
⊢ Norm.norm.{u_3} (E := E) ((s' n x : (a : β) → E) y : E) ≤
    HAdd.hAdd (α := β → ℝ) (β := β → ℝ) (fun (a : β) ↦ ‖f x a‖) (fun (a : β) ↦ ‖f x a‖) y

Tactic:
simp_rw [s', SimpleFunc.coe_comp]

Premises used: MeasureTheory.SimpleFunc.coe_comp
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) ν
n : ℕ
y : β
⊢ Norm.norm.{u_3} (E := E) (((⇑(s n) : (a : α × β) → E) ∘ Prod.mk x) y) ≤
    HAdd.hAdd (α := β → ℝ) (β := β → ℝ) (fun (a : β) ↦ ‖f x a‖) (fun (a : β) ↦ ‖f x a‖) y

Tactic:
SimpleFunc.norm_approxOn_zero_le _ _ (x, y) n

Premises used: Prod.mk, MeasureTheory.SimpleFunc.norm_approxOn_zero_le
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) ν
n : ℕ
y : β
⊢ Norm.norm.{u_3} (E := E) (((⇑(s n) : (a : α × β) → E) ∘ Prod.mk x) y) ≤
    HAdd.hAdd (α := β → ℝ) (β := β → ℝ) (fun (a : β) ↦ ‖f x a‖) (fun (a : β) ↦ ‖f x a‖) y

Tactic:
exact SimpleFunc.norm_approxOn_zero_le _ _ (x, y) n

Premises used: Prod.mk, MeasureTheory.SimpleFunc.norm_approxOn_zero_le
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) ν
⊢ ∀ (n : ℕ), Integrable.{u_3, u_2} (ε := E) (⇑(s' n x) : (a : β) → E) ν

Tactic:
have (n : _) : Integrable (s' n 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
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) ν
this : ∀ (n : ℕ), Integrable.{u_3, u_2} (ε := E) (⇑(s' n x) : (a : β) → E) ν
pos :
  Tendsto.{0, u_3} (β := E) (fun (i : ℕ) ↦ ∫ (x_1 : β), (s' i x : (a : β) → E) x_1 ∂ν) atTop (𝓝 (∫ (y : β), f x y ∂ν))
⊢ Tendsto.{0, u_3} (β := E) (fun (i : ℕ) ↦ f' i x) atTop (𝓝 (∫ (y : β), f x y ∂ν))

Tactic:
simp only [f', hfx, SimpleFunc.integral_eq_integral _ (this _), indicator_of_mem,
        mem_setOf_eq]

Premises used: MeasureTheory.SimpleFunc.integral_eq_integral, Set.mem_setOf_eq, Set.indicator_of_mem
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) ν
this : ∀ (n : ℕ), Integrable.{u_3, u_2} (ε := E) (⇑(s' n x) : (a : β) → E) ν
⊢ Tendsto.{0, u_3} (β := E) (fun (i : ℕ) ↦ ∫ (x_1 : β), (s' i x : (a : β) → E) x_1 ∂ν) atTop (𝓝 (∫ (y : β), f x y ∂ν))

Tactic:
tendsto_integral_of_dominated_convergence (fun y => ‖f x y‖ + ‖f x y‖)
          (fun n => (s' n x).aestronglyMeasurable) (hfx.norm.add hfx.norm) ?_ ?_

Premises used: Norm.norm, MeasureTheory.tendsto_integral_of_dominated_convergence, HAdd.hAdd, MeasureTheory.Integrable.add, MeasureTheory.SimpleFunc.aestronglyMeasurable, MeasureTheory.Integrable.norm
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) ν
this : ∀ (n : ℕ), Integrable.{u_3, u_2} (ε := E) (⇑(s' n x) : (a : β) → E) ν
pos :
  ∀ (n : ℕ),
    ∀ᵐ (a : β) ∂ν, Norm.norm.{u_3} (E := E) ((s' n x : (a : β) → E) a : E) ≤ (fun (y : β) ↦ ‖f x y‖ + ‖f x y‖) a
pos₁ : ∀ᵐ (a : β) ∂ν, Tendsto (fun (n : ℕ) ↦ (s' n x : (a : β) → E) a) atTop (𝓝 (f x a))
⊢ Tendsto.{0, u_3} (β := E) (fun (i : ℕ) ↦ ∫ (x_1 : β), (s' i x : (a : β) → E) x_1 ∂ν) atTop (𝓝 (∫ (y : β), f x y ∂ν))

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) ?_ ?_

Premises used: Norm.norm, MeasureTheory.tendsto_integral_of_dominated_convergence, HAdd.hAdd, MeasureTheory.Integrable.add, MeasureTheory.SimpleFunc.aestronglyMeasurable, MeasureTheory.Integrable.norm
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) ν
this : ∀ (n : ℕ), Integrable.{u_3, u_2} (ε := E) (⇑(s' n x) : (a : β) → E) ν
⊢ ∀ (n : ℕ),
    ∀ᵐ (a : β) ∂ν, Norm.norm.{u_3} (E := E) ((s' n x : (a : β) → E) a : E) ≤ (fun (y : β) ↦ ‖f x y‖ + ‖f x y‖) a

Tactic:
fun n => Eventually.of_forall fun y =>
          SimpleFunc.norm_approxOn_zero_le ?_ ?_ (x, y) n

Premises used: Prod.mk, Filter.Eventually.of_forall, MeasureTheory.SimpleFunc.norm_approxOn_zero_le
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) ν
this : ∀ (n : ℕ), Integrable.{u_3, u_2} (ε := E) (⇑(s' n x) : (a : β) → E) ν
pos : ∀ (n : ℕ) (y : β), Measurable (uncurry f)
pos₁ : ∀ (n : ℕ) (y : β), 0 ∈ range (uncurry f) ∪ {0}
⊢ ∀ (n : ℕ),
    ∀ᵐ (a : β) ∂ν, Norm.norm.{u_3} (E := E) ((s' n x : (a : β) → E) a : E) ≤ (fun (y : β) ↦ ‖f x y‖ + ‖f x y‖) a

Tactic:
refine fun n => Eventually.of_forall fun y =>
          SimpleFunc.norm_approxOn_zero_le ?_ ?_ (x, y) n

Premises used: Prod.mk, Filter.Eventually.of_forall, MeasureTheory.SimpleFunc.norm_approxOn_zero_le
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) ν
this : ∀ (n : ℕ), Integrable.{u_3, u_2} (ε := E) (⇑(s' n x) : (a : β) → E) ν
n : ℕ
y : β
⊢ Measurable (uncurry f)

Tactic:
hf.measurable

Premises used: MeasureTheory.StronglyMeasurable.measurable
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) ν
this : ∀ (n : ℕ), Integrable.{u_3, u_2} (ε := E) (⇑(s' n x) : (a : β) → E) ν
n : ℕ
y : β
⊢ Measurable (uncurry f)

Tactic:
exact hf.measurable

Premises used: MeasureTheory.StronglyMeasurable.measurable
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) ν
this : ∀ (n : ℕ), Integrable.{u_3, u_2} (ε := E) (⇑(s' n x) : (a : β) → E) ν
n : ℕ
y : β
⊢ 0 ∈ range (uncurry f) ∪ {0}

Tactic:
simp