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)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) ν
this : ∀ (n : ℕ), Integrable.{u_3, u_2} (ε := E) (⇑(s' n x) : (a : β) → E) ν
⊢ ∀ᵐ (a : β) ∂ν, Tendsto (fun (n : ℕ) ↦ (s' n x : (a : β) → E) a) atTop (𝓝 (f x a))

Tactic:
Eventually.of_forall fun y => SimpleFunc.tendsto_approxOn ?_ ?_ ?_

Premises used: Filter.Eventually.of_forall, MeasureTheory.SimpleFunc.tendsto_approxOn
-- 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 : ∀ (y : β), Measurable.{u_2, u_3} (β := E) fun (x_1 : β) ↦ uncurry f (x, x_1)
pos₁ : ∀ (y : β), 0 ∈ range (uncurry f) ∪ {0}
pos₂ :
  ∀ (y : β), uncurry f (x, y) ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (range (uncurry f) ∪ {0})
⊢ ∀ᵐ (a : β) ∂ν, Tendsto (fun (n : ℕ) ↦ (s' n x : (a : β) → E) a) atTop (𝓝 (f x a))

Tactic:
refine Eventually.of_forall fun y => SimpleFunc.tendsto_approxOn ?_ ?_ ?_

Premises used: Filter.Eventually.of_forall, MeasureTheory.SimpleFunc.tendsto_approxOn
-- 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) ν
y : β
⊢ Measurable.{u_2, u_3} (β := E) fun (x_1 : β) ↦ uncurry f (x, x_1)

Tactic:
hf.measurable.of_uncurry_left

Premises used: MeasureTheory.StronglyMeasurable.measurable, Measurable.of_uncurry_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)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) ν
this : ∀ (n : ℕ), Integrable.{u_3, u_2} (ε := E) (⇑(s' n x) : (a : β) → E) ν
y : β
⊢ Measurable.{u_2, u_3} (β := E) fun (x_1 : β) ↦ uncurry f (x, x_1)

Tactic:
exact hf.measurable.of_uncurry_left

Premises used: MeasureTheory.StronglyMeasurable.measurable, Measurable.of_uncurry_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)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) ν
this : ∀ (n : ℕ), Integrable.{u_3, u_2} (ε := E) (⇑(s' n x) : (a : β) → E) ν
y : β
⊢ 0 ∈ range (uncurry f) ∪ {0}

Tactic:
simp
-- 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) ν
y : β
pos : uncurry f (x, y) ∈ range (uncurry f) ∪ {0}
⊢ uncurry f (x, y) ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (range (uncurry f) ∪ {0})

Tactic:
apply subset_closure

Premises used: subset_closure
-- 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) ν
y : β
⊢ uncurry f (x, y) ∈ range (uncurry f) ∪ {0}

Tactic:
simp [-uncurry_apply_pair]

Premises used: Function.uncurry_apply_pair
-- 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) ν
⊢ Tendsto.{0, u_3} (β := E) (fun (i : ℕ) ↦ f' i x) atTop (𝓝 (∫ (y : β), f x y ∂ν))

Tactic:
simp [f', hfx, integral_undef]

Premises used: MeasureTheory.integral_undef
-- 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)
⊢ Tendsto f' atTop (𝓝 fun (x : α) ↦ ∫ (y : β), f x y ∂ν)

Tactic:
have h2f' : Tendsto f' atTop (𝓝 fun x : α => ∫ y : β, f x y ∂ν) := by
    rw [tendsto_pi_nhds]; intro x
    by_cases hfx : Integrable (f x) ν
    · 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
      simp only [f', hfx, SimpleFunc.integral_eq_integral _ (this _), indicator_of_mem,
        mem_setOf_eq]
      refine
        tendsto_integral_of_dominated_convergence (fun y => ‖f x y‖ + ‖f x y‖)
          (fun n => (s' n x).aestronglyMeasurable) (hfx.norm.add hfx.norm) ?_ ?_
      · refine fun n => Eventually.of_forall fun y =>
          SimpleFunc.norm_approxOn_zero_le ?_ ?_ (x, y) n
        · exact hf.measurable
        · simp
      · refine Eventually.of_forall fun y => SimpleFunc.tendsto_approxOn ?_ ?_ ?_
        · exact hf.measurable.of_uncurry_left
        · simp
        apply subset_closure
        simp [-uncurry_apply_pair]
    · simp [f', hfx, integral_undef]
-- 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)
h2f' : Tendsto f' atTop (𝓝 fun (x : α) ↦ ∫ (y : β), f x y ∂ν)
⊢ StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν

Tactic:
stronglyMeasurable_of_tendsto _ hf' h2f'

Premises used: stronglyMeasurable_of_tendsto
-- 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)
h2f' : Tendsto f' atTop (𝓝 fun (x : α) ↦ ∫ (y : β), f x y ∂ν)
⊢ StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν

Tactic:
exact stronglyMeasurable_of_tendsto _ hf' h2f'

Premises used: stronglyMeasurable_of_tendsto
-- 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 f
⊢ StronglyMeasurable (uncurry (Function.curry f))

Tactic:
rw [← uncurry_curry f] at hf

Premises used: Function.uncurry_curry
-- 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 (Function.curry f))
⊢ StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f (x, y) ∂ν

Tactic:
hf.integral_prod_right

Premises used: MeasureTheory.StronglyMeasurable.integral_prod_right
-- 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 (Function.curry f))
⊢ StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f (x, y) ∂ν

Tactic:
exact hf.integral_prod_right

Premises used: MeasureTheory.StronglyMeasurable.integral_prod_right
-- 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)
⊢ StronglyMeasurable.{u_2, u_3} (β := E) fun (y : β) ↦ ∫ (x : α), f x y ∂μ

Tactic:
(hf.comp_measurable measurable_swap).integral_prod_right'

Premises used: MeasureTheory.StronglyMeasurable.comp_measurable, MeasureTheory.StronglyMeasurable.integral_prod_right', measurable_swap
-- 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 f
⊢ StronglyMeasurable.{u_2, u_3} (β := E) fun (y : β) ↦ ∫ (x : α), f (x, y) ∂μ

Tactic:
(hf.comp_measurable measurable_swap).integral_prod_right'

Premises used: MeasureTheory.StronglyMeasurable.comp_measurable, MeasureTheory.StronglyMeasurable.integral_prod_right', measurable_swap, Prod.swap
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : Ne (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ν.real (Prod.mk x ⁻¹' s)) μ

Tactic:
⟨(measurable_measure_prodMk_left hs).ennreal_toReal.aemeasurable.aestronglyMeasurable, ?_⟩

Premises used: AEMeasurable.aestronglyMeasurable, Measurable.aemeasurable, MeasureTheory.Integrable, measurable_measure_prodMk_left, And.intro, Measurable.ennreal_toReal
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : Ne (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ν.real (Prod.mk x ⁻¹' s)) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ν.real (Prod.mk x ⁻¹' s)) μ

Tactic:
refine ⟨(measurable_measure_prodMk_left hs).ennreal_toReal.aemeasurable.aestronglyMeasurable, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : Ne (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
simp_rw : ∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s))) ∂μ < ∞
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ν.real (Prod.mk x ⁻¹' s)) μ

Tactic:
simp_rw [hasFiniteIntegral_iff_enorm, measureReal_def, enorm_eq_ofReal toReal_nonneg]

Premises used: ENNReal.toReal_nonneg, MeasureTheory.measureReal_def, Real.enorm_eq_ofReal, MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : Ne (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
h2s.lt_top

Premises used: Ne.lt_top
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : Ne (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s))) ∂μ =
    (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s
⊢ ∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s))) ∂μ < ∞

Tactic:
convert! h2s.lt_top using 1

Premises used: Ne.lt_top
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : Ne (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s))) ∂μ =
    ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s))) ∂μ =
    (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s

Tactic:
rw [prod_apply hs]

Premises used: MeasureTheory.Measure.prod_apply
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : Ne (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ ENNReal.ofReal (ENNReal.toReal ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)))) fun (a : α) ↦
    (ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)
⊢ ∫⁻ (a : α), ENNReal.ofReal (ENNReal.toReal ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s))) ∂μ =
    ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ

Tactic:
apply lintegral_congr_ae

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : Ne (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ (x : α) (hx : LT.lt (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    ENNReal.ofReal (ENNReal.toReal ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s))) =
      (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ ENNReal.ofReal (ENNReal.toReal ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)))) fun (a : α) ↦
    (ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)

Tactic:
filter_upwards [ae_measure_lt_top hs h2s] with x hx

Premises used: MeasureTheory.Measure.ae_measure_lt_top
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : Ne (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : LT.lt (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [lt_top_iff_ne_top] at hx

Premises used: lt_top_iff_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : Ne (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : Ne (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.ofReal (ENNReal.toReal ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s))) =
    (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)

Tactic:
simp [ofReal_toReal, hx]

Premises used: ENNReal.ofReal_toReal
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
X : Type u_4
inst_2 : TopologicalSpace X
inst_3 : SFinite μ
inst_4 : SFinite ν
f : β × α → X
hf : AEStronglyMeasurable f (ν.prod μ)
⊢ AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f (map Prod.swap (μ.prod ν))

Tactic:
rw [← prod_swap] at hf

Premises used: MeasureTheory.Measure.prod_swap
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
X : Type u_4
inst_2 : TopologicalSpace X
inst_3 : SFinite μ
inst_4 : SFinite ν
f : β × α → X
hf : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f (map Prod.swap (μ.prod ν))
⊢ AEStronglyMeasurable (β := X) (fun (z : α × β) ↦ f z.swap) (μ.prod ν)

Tactic:
hf.comp_measurable measurable_swap

Premises used: MeasureTheory.AEStronglyMeasurable.comp_measurable, measurable_swap
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
X : Type u_4
inst_2 : TopologicalSpace X
inst_3 : SFinite μ
inst_4 : SFinite ν
f : β × α → X
hf : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f (map Prod.swap (μ.prod ν))
⊢ AEStronglyMeasurable (β := X) (fun (z : α × β) ↦ f z.swap) (μ.prod ν)

Tactic:
exact hf.comp_measurable measurable_swap

Premises used: MeasureTheory.AEStronglyMeasurable.comp_measurable, measurable_swap
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
γ : Type u_5
inst_2 : TopologicalSpace γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (β := γ) (fun (z : α × β) ↦ f z.1) (μ.prod ν)

Tactic:
hf.comp_quasiMeasurePreserving quasiMeasurePreserving_fst

Premises used: MeasureTheory.AEStronglyMeasurable.comp_quasiMeasurePreserving, MeasureTheory.Measure.quasiMeasurePreserving_fst
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
γ : Type u_5
inst_2 : TopologicalSpace γ
f : β → γ
hf : AEStronglyMeasurable f ν
⊢ AEStronglyMeasurable (β := γ) (fun (z : α × β) ↦ f z.2) (μ.prod ν)

Tactic:
hf.comp_quasiMeasurePreserving quasiMeasurePreserving_snd

Premises used: MeasureTheory.AEStronglyMeasurable.comp_quasiMeasurePreserving, MeasureTheory.Measure.quasiMeasurePreserving_snd
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
inst_4 : NormedSpace ℝ E
f : α × β → E
hf : AEStronglyMeasurable f (μ.prod ν)
a : α
hx : ∀ᵐ (y : β) ∂ν, f (a, y) = AEStronglyMeasurable.mk f hf (a, y)
⊢ Eq.{u_3 + 1} (α := E) (∫ (y : β), f (a, y) ∂ν) (∫ (y : β), AEStronglyMeasurable.mk f hf (a, y) ∂ν)

Tactic:
integral_congr_ae hx

Premises used: MeasureTheory.integral_congr_ae