awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
⊢ MeasurableSet.{u_1} (α := α) {x : α | Integrable (f x) ν}
have simp_rw : MeasurableSet.{u_1} (α := α) {x : α | HasFiniteIntegral (f x) ν}
Tactic: simp_rw [Integrable, hf.of_uncurry_left.aestronglyMeasurable, true_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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)
⊢ StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν
have pos : ∀ (hE : CompleteSpace E), StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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)
pos : ∀ (hE : CompleteSpace E), StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν
⊢ StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν
have neg : ∀ (hE : ¬CompleteSpace E), StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (hypothesis)
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
⊢ StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (hypothesis)
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 : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν
have this : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
Tactic: haveI : SeparableSpace (range (uncurry f) ∪ {0} : Set E) :=
    hf.separableSpace_range_union_singleton
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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)
have refine : StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
Tactic: refine StronglyMeasurable.indicator ?_ (measurableSet_integrable hf)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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 : ℕ
x : α
⊢ {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
have refine : (s' n x).range ⊆ (s n).range
Tactic: refine Finset.Subset.trans (Finset.filter_subset _ _) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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 : ℕ
x : α
y : E
⊢ y ∈ (s' n x).range → y ∈ (s n).range
have simp_rw : Membership.mem (γ := Set E) (range.{u_3, u_2 + 1} (ι := β) (⇑(s' n x) : (a : β) → E)) y →
  Membership.mem (γ := Set E) (range (ι := α × β) (⇑(s n) : (a : α × β) → E)) y
Tactic: simp_rw [SimpleFunc.mem_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (hypothesis)
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.{u_1, u_3} (β := E) fun (x : α) ↦ SimpleFunc.integral ν (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 x; refine Finset.Subset.trans (Finset.filter_subset _ _) ?_; intro y
      simp_rw [SimpleFunc.mem_range]; rintro ⟨z, rfl⟩; exact ⟨(x, z), rfl⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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
⊢ StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
have simp : StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦
  ∑ x_1 ∈ (s n).range, ν.real (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.MeasureTheory.Integral.Prod (goal)
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
⊢ StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦
    ∑ x_1 ∈ (s n).range, ν.real (preimage (β := E) (⇑(s' n x) : (a : β) → E) {x_1}) • x_1
have refine : ∀ x ∈ (s n).range,
  StronglyMeasurable.{u_1, u_3} (β := E) fun (x_2 : α) ↦ ν.real (preimage (β := E) (⇑(s' n x_2) : (a : β) → E) {x}) • x
Tactic: refine Finset.stronglyMeasurable_fun_sum _ fun x _ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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
⊢ StronglyMeasurable.{u_1, u_3} (β := E) fun (x_1 : α) ↦ ν.real (preimage (β := E) (⇑(s' n x_1) : (a : β) → E) {x}) • x
have refine : Measurable (β := ℝ≥0∞) fun (x_1 : α) ↦ (ν : (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.MeasureTheory.Integral.Prod (goal)
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
⊢ Measurable (β := ℝ≥0∞) fun (x_1 : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (preimage (β := E) (⇑(s' n x_1) : (a : β) → E) {x})
have simp : Measurable (β := ℝ≥0∞) fun (x_1 : α) ↦
  (ν : (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.MeasureTheory.Integral.Prod (goal)
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
⊢ Measurable (β := ℝ≥0∞) fun (x_1 : α) ↦
    (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x_1 ⁻¹' preimage (β := E) (⇑(s n) : (a : α × β) → E) {x})
have hs : MeasurableSet (α := α × β) (preimage (β := E) (⇑(s n) : (a : α × β) → E) {x})
Tactic: apply measurable_measure_prodMk_left
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (hypothesis)
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)
⊢ StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν
have hf' : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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)
⊢ Tendsto f' atTop (𝓝 fun (x : α) ↦ ∫ (y : β), f x y ∂ν)
have rw : ∀ (x : α), Tendsto.{0, u_3} (β := E) (fun (i : ℕ) ↦ f' i x) atTop (𝓝 (∫ (y : β), f x y ∂ν))
Tactic: rw [tendsto_pi_nhds]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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 : α
⊢ Tendsto.{0, u_3} (β := E) (fun (i : ℕ) ↦ f' i x) atTop (𝓝 (∫ (y : β), f x y ∂ν))
have pos : ∀ (hfx : Integrable (f x) ν), Tendsto.{0, u_3} (β := E) (fun (i : ℕ) ↦ f' i x) atTop (𝓝 (∫ (y : β), f x y ∂ν))
Tactic: by_cases hfx : Integrable (f x) ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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 ∂ν))
⊢ Tendsto.{0, u_3} (β := E) (fun (i : ℕ) ↦ f' i x) atTop (𝓝 (∫ (y : β), f x y ∂ν))
have neg : ∀ (hfx : ¬Integrable (f x) ν), Tendsto.{0, u_3} (β := E) (fun (i : ℕ) ↦ f' i x) atTop (𝓝 (∫ (y : β), f x y ∂ν))
Tactic: by_cases hfx : Integrable (f x) ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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) ν
have 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
Tactic: apply (hfx.norm.add hfx.norm).mono' (s' n x).aestronglyMeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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 : ℕ
⊢ ∀ᵐ (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
have 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
Tactic: filter_upwards with y
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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 x : (a : β) → E) y : E) ≤
    HAdd.hAdd (α := β → ℝ) (β := β → ℝ) (fun (a : β) ↦ ‖f x a‖) (fun (a : β) ↦ ‖f x a‖) y
have 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
Tactic: simp_rw [s', SimpleFunc.coe_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (hypothesis)
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) ν
⊢ Tendsto.{0, u_3} (β := E) (fun (i : ℕ) ↦ f' i x) atTop (𝓝 (∫ (y : β), f x y ∂ν))
have this₁ : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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 : ℕ) ↦ f' i x) atTop (𝓝 (∫ (y : β), f x y ∂ν))
have pos : Tendsto.{0, u_3} (β := E) (fun (i : ℕ) ↦ ∫ (x_1 : β), (s' i x : (a : β) → E) x_1 ∂ν) atTop (𝓝 (∫ (y : β), f x y ∂ν))
Tactic: simp only [f', hfx, SimpleFunc.integral_eq_integral _ (this _), indicator_of_mem,
        mem_setOf_eq]