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 α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : β → E
hμ : μ ≠ 0
hf_meas : AEStronglyMeasurable (β := E) (fun (x : α × β) ↦ f x.2) (μ.prod ν)
hf_fin : HasFiniteIntegral (ε := E) (fun (x : α × β) ↦ f x.2) (μ.prod ν)
right : HasFiniteIntegral f ν
⊢ Integrable f ν

Tactic:
use hf_meas.of_comp_snd hμ

Premises used: MeasureTheory.AEStronglyMeasurable.of_comp_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 ν
f : β → E
hμ : μ ≠ 0
hf_meas : AEStronglyMeasurable (β := E) (fun (x : α × β) ↦ f x.2) (μ.prod ν)
hf_fin : HasFiniteIntegral (ε := E) (fun (x : α × β) ↦ f x.2) (μ.prod ν)
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α × β) ↦ ‖f x.2‖ₑ) (μ.prod ν)

Tactic:
have := hf_meas.enorm
-- 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 ν
f : β → E
hμ : μ ≠ 0
hf_meas : AEStronglyMeasurable (β := E) (fun (x : α × β) ↦ f x.2) (μ.prod ν)
hf_fin : HasFiniteIntegral (ε := E) (fun (x : α × β) ↦ f x.2) (μ.prod ν)
this : AEMeasurable (β := ℝ≥0∞) (fun (x : α × β) ↦ ‖f x.2‖ₑ) (μ.prod ν)
⊢ HasFiniteIntegral f ν

Tactic:
aesop (add simp [HasFiniteIntegral, lintegral_prod, ENNReal.mul_lt_top_iff])

Premises used: ENNReal.mul_lt_top_iff, MeasureTheory.lintegral_prod, MeasureTheory.HasFiniteIntegral
-- 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 : SFinite μ
f : α → E
hf : Integrable (ε := E) (fun (x : α × β) ↦ f x.1) (μ.prod ν)
hν : ν ≠ 0
⊢ Integrable f μ

Tactic:
hf.swap.of_comp_snd hν

Premises used: MeasureTheory.Integrable.of_comp_snd, MeasureTheory.Integrable.swap
-- 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 : IsFiniteMeasure μ
f : β → E
hμ : μ ≠ 0
⊢ Integrable (ε := E) (fun (x : α × β) ↦ f x.2) (μ.prod ν) ↔ Integrable f ν

Tactic:
⟨(.of_comp_snd · hμ), (.comp_snd · μ)⟩

Premises used: MeasureTheory.Integrable.comp_snd, MeasureTheory.Integrable.of_comp_snd, Iff.intro
-- 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 : IsFiniteMeasure ν
f : α → E
hν : ν ≠ 0
⊢ Integrable (ε := E) (fun (x : α × β) ↦ f x.1) (μ.prod ν) ↔ Integrable f μ

Tactic:
⟨(.of_comp_fst · hν), (.comp_fst · ν)⟩

Premises used: MeasureTheory.Integrable.of_comp_fst, MeasureTheory.Integrable.comp_fst, Iff.intro
-- 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 : Integrable f (μ.prod ν)
⊢ Integrable.{u_3, u_1} (ε := E) (fun (x : α) ↦ ∫ (y : β), f (x, y) ∂ν) μ

Tactic:
Integrable.mono hf.integral_norm_prod_left hf.aestronglyMeasurable.integral_prod_right' <|
    Eventually.of_forall fun x =>
      (norm_integral_le_integral_norm _).trans_eq <|
        (norm_of_nonneg <|
            integral_nonneg_of_ae <|
              Eventually.of_forall fun y => (norm_nonneg (f (x, y)) :)).symm

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, LE.le.trans_eq, MeasureTheory.Integrable.mono, MeasureTheory.norm_integral_le_integral_norm, MeasureTheory.Integrable.integral_norm_prod_left, Prod.mk, Filter.Eventually.of_forall, MeasureTheory.AEStronglyMeasurable.integral_prod_right', MeasureTheory.integral_nonneg_of_ae, Eq.symm, norm_nonneg, Real.norm_of_nonneg
-- 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
inst_5 : SFinite μ
f : α × β → E
hf : Integrable f (μ.prod ν)
⊢ Integrable.{u_3, u_2} (ε := E) (fun (y : β) ↦ ∫ (x : α), f (x, y) ∂μ) ν

Tactic:
hf.swap.integral_prod_left

Premises used: MeasureTheory.Integrable.integral_prod_left, MeasureTheory.Integrable.swap, Prod.swap
-- 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
inst_5 : SFinite μ
f : α × β → E
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : β × α), f z.swap ∂ν.prod μ) (∫ (z : α × β), f z ∂μ.prod ν)

Tactic:
measurePreserving_swap.integral_comp MeasurableEquiv.prodComm.measurableEmbedding _

Premises used: MeasurableEquiv.measurableEmbedding, MeasureTheory.MeasurePreserving.integral_comp, MeasurableEquiv.prodComm, MeasureTheory.Measure.measurePreserving_swap
-- 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
inst_5 : SFinite μ
s : Set α
t : Set β
f : α × β → E
rw :
  Eq.{u_3 + 1} (α := E) (∫ (z : β × α), f z.swap ∂(ν.restrict t).prod (μ.restrict s))
    (∫ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν)
rw₁ :
  Eq.{u_3 + 1} (α := E) (∫ (z : β × α), f z.swap ∂(ν.restrict t).prod (μ.restrict s))
    (∫ (z : α × β), f z ∂(μ.restrict s).prod (ν.restrict t))
rw₂ rw₃ :
  Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂(μ.restrict s).prod (ν.restrict t))
    (∫ (z : α × β), f z ∂(μ.restrict s).prod (ν.restrict t))
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : β × α) in t ×ˢ s, f z.swap ∂ν.prod μ) (∫ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν)

Tactic:
rw [← Measure.prod_restrict, ← Measure.prod_restrict, integral_prod_swap]

Premises used: MeasureTheory.Measure.prod_restrict, MeasureTheory.integral_prod_swap
-- 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
inst_5 : SFinite μ
E' : Type u_4
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
⊢ Eq.{u_4 + 1} (α := E') (∫ (x : α), F (∫ (y : β), f (x, y) + g (x, y) ∂ν) ∂μ)
    (∫ (x : α), F (HAdd.hAdd (α := E) (∫ (y : β), f (x, y) ∂ν) (∫ (y : β), g (x, y) ∂ν)) ∂μ)

Tactic:
integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- 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
inst_5 : SFinite μ
E' : Type u_4
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
refine :
  EventuallyEq.{u_1, u_4} (β := E') (ae μ) (fun (x : α) ↦ F (∫ (y : β), f (x, y) + g (x, y) ∂ν)) fun (x : α) ↦
    F (HAdd.hAdd (α := E) (∫ (y : β), f (x, y) ∂ν) (∫ (y : β), g (x, y) ∂ν))
⊢ Eq.{u_4 + 1} (α := E') (∫ (x : α), F (∫ (y : β), f (x, y) + g (x, y) ∂ν) ∂μ)
    (∫ (x : α), F (HAdd.hAdd (α := E) (∫ (y : β), f (x, y) ∂ν) (∫ (y : β), g (x, y) ∂ν)) ∂μ)

Tactic:
refine integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- 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
inst_5 : SFinite μ
E' : Type u_4
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
h :
  ∀ (a : α) (h2f : Integrable.{u_3, u_2} (ε := E) (fun (y : β) ↦ f (a, y)) ν)
    (h2g : Integrable.{u_3, u_2} (ε := E) (fun (y : β) ↦ g (a, y)) ν),
    F (∫ (y : β), f (a, y) + g (a, y) ∂ν) = F (HAdd.hAdd (α := E) (∫ (y : β), f (a, y) ∂ν) (∫ (y : β), g (a, y) ∂ν))
⊢ EventuallyEq.{u_1, u_4} (β := E') (ae μ) (fun (x : α) ↦ F (∫ (y : β), f (x, y) + g (x, y) ∂ν)) fun (x : α) ↦
    F (HAdd.hAdd (α := E) (∫ (y : β), f (x, y) ∂ν) (∫ (y : β), g (x, y) ∂ν))

Tactic:
filter_upwards [hf.prod_right_ae, hg.prod_right_ae] with _ h2f h2g

Premises used: MeasureTheory.Integrable.prod_right_ae
-- 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
inst_5 : SFinite μ
E' : Type u_4
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
a : α
h2f : Integrable.{u_3, u_2} (ε := E) (fun (y : β) ↦ f (a, y)) ν
h2g : Integrable.{u_3, u_2} (ε := E) (fun (y : β) ↦ g (a, y)) ν
⊢ F (∫ (y : β), f (a, y) + g (a, y) ∂ν) = F (HAdd.hAdd (α := E) (∫ (y : β), f (a, y) ∂ν) (∫ (y : β), g (a, y) ∂ν))

Tactic:
simp [integral_add h2f h2g]

Premises used: MeasureTheory.integral_add
-- 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
inst_5 : SFinite μ
E' : Type u_4
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
⊢ Eq.{u_4 + 1} (α := E') (∫ (x : α), F (∫ (y : β), f (x, y) - g (x, y) ∂ν) ∂μ)
    (∫ (x : α), F (HSub.hSub (α := E) (∫ (y : β), f (x, y) ∂ν) (∫ (y : β), g (x, y) ∂ν)) ∂μ)

Tactic:
integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- 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
inst_5 : SFinite μ
E' : Type u_4
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
refine :
  EventuallyEq.{u_1, u_4} (β := E') (ae μ) (fun (x : α) ↦ F (∫ (y : β), f (x, y) - g (x, y) ∂ν)) fun (x : α) ↦
    F (HSub.hSub (α := E) (∫ (y : β), f (x, y) ∂ν) (∫ (y : β), g (x, y) ∂ν))
⊢ Eq.{u_4 + 1} (α := E') (∫ (x : α), F (∫ (y : β), f (x, y) - g (x, y) ∂ν) ∂μ)
    (∫ (x : α), F (HSub.hSub (α := E) (∫ (y : β), f (x, y) ∂ν) (∫ (y : β), g (x, y) ∂ν)) ∂μ)

Tactic:
refine integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- 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
inst_5 : SFinite μ
E' : Type u_4
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
h :
  ∀ (a : α) (h2f : Integrable.{u_3, u_2} (ε := E) (fun (y : β) ↦ f (a, y)) ν)
    (h2g : Integrable.{u_3, u_2} (ε := E) (fun (y : β) ↦ g (a, y)) ν),
    F (∫ (y : β), f (a, y) - g (a, y) ∂ν) = F (HSub.hSub (α := E) (∫ (y : β), f (a, y) ∂ν) (∫ (y : β), g (a, y) ∂ν))
⊢ EventuallyEq.{u_1, u_4} (β := E') (ae μ) (fun (x : α) ↦ F (∫ (y : β), f (x, y) - g (x, y) ∂ν)) fun (x : α) ↦
    F (HSub.hSub (α := E) (∫ (y : β), f (x, y) ∂ν) (∫ (y : β), g (x, y) ∂ν))

Tactic:
filter_upwards [hf.prod_right_ae, hg.prod_right_ae] with _ h2f h2g

Premises used: MeasureTheory.Integrable.prod_right_ae
-- 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
inst_5 : SFinite μ
E' : Type u_4
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
a : α
h2f : Integrable.{u_3, u_2} (ε := E) (fun (y : β) ↦ f (a, y)) ν
h2g : Integrable.{u_3, u_2} (ε := E) (fun (y : β) ↦ g (a, y)) ν
⊢ F (∫ (y : β), f (a, y) - g (a, y) ∂ν) = F (HSub.hSub (α := E) (∫ (y : β), f (a, y) ∂ν) (∫ (y : β), g (a, y) ∂ν))

Tactic:
simp [integral_sub h2f h2g]

Premises used: MeasureTheory.integral_sub
-- 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
inst_5 : SFinite μ
f g : α × β → E
F : E → ℝ≥0∞
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
⊢ ∫⁻ (x : α), F (∫ (y : β), f (x, y) - g (x, y) ∂ν) ∂μ =
    ∫⁻ (x : α), F (HSub.hSub (α := E) (∫ (y : β), f (x, y) ∂ν) (∫ (y : β), g (x, y) ∂ν)) ∂μ

Tactic:
lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- 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
inst_5 : SFinite μ
f g : α × β → E
F : E → ℝ≥0∞
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
refine :
  (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ F (∫ (y : β), f (x, y) - g (x, y) ∂ν)) fun (x : α) ↦
    F (HSub.hSub (α := E) (∫ (y : β), f (x, y) ∂ν) (∫ (y : β), g (x, y) ∂ν))
⊢ ∫⁻ (x : α), F (∫ (y : β), f (x, y) - g (x, y) ∂ν) ∂μ =
    ∫⁻ (x : α), F (HSub.hSub (α := E) (∫ (y : β), f (x, y) ∂ν) (∫ (y : β), g (x, y) ∂ν)) ∂μ

Tactic:
refine lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- 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
inst_5 : SFinite μ
f g : α × β → E
F : E → ℝ≥0∞
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
h :
  ∀ (a : α) (h2f : Integrable.{u_3, u_2} (ε := E) (fun (y : β) ↦ f (a, y)) ν)
    (h2g : Integrable.{u_3, u_2} (ε := E) (fun (y : β) ↦ g (a, y)) ν),
    F (∫ (y : β), f (a, y) - g (a, y) ∂ν) = F (HSub.hSub (α := E) (∫ (y : β), f (a, y) ∂ν) (∫ (y : β), g (a, y) ∂ν))
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ F (∫ (y : β), f (x, y) - g (x, y) ∂ν)) fun (x : α) ↦
    F (HSub.hSub (α := E) (∫ (y : β), f (x, y) ∂ν) (∫ (y : β), g (x, y) ∂ν))

Tactic:
filter_upwards [hf.prod_right_ae, hg.prod_right_ae] with _ h2f h2g

Premises used: MeasureTheory.Integrable.prod_right_ae
-- 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
inst_5 : SFinite μ
f g : α × β → E
F : E → ℝ≥0∞
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
a : α
h2f : Integrable.{u_3, u_2} (ε := E) (fun (y : β) ↦ f (a, y)) ν
h2g : Integrable.{u_3, u_2} (ε := E) (fun (y : β) ↦ g (a, y)) ν
⊢ F (∫ (y : β), f (a, y) - g (a, y) ∂ν) = F (HSub.hSub (α := E) (∫ (y : β), f (a, y) ∂ν) (∫ (y : β), g (a, y) ∂ν))

Tactic:
simp [integral_sub h2f h2g]

Premises used: MeasureTheory.integral_sub
-- 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
inst_5 : SFinite μ
f g : α × β → E
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
⊢ ∫ (x : α), ∫ (y : β), f (x, y) + g (x, y) ∂ν ∂μ =
    HAdd.hAdd (α := E) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ) (∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ)

Tactic:
(integral_fn_integral_add id hf hg).trans <|
    integral_add hf.integral_prod_left hg.integral_prod_left

Premises used: MeasureTheory.Integrable.integral_prod_left, id, MeasureTheory.integral_fn_integral_add, MeasureTheory.integral_add, Eq.trans
-- 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
inst_5 : SFinite μ
f g : α × β → E
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
⊢ ∫ (x : α), ∫ (y : β), (f + g) (x, y) ∂ν ∂μ =
    HAdd.hAdd (α := E) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ) (∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ)

Tactic:
integral_integral_add hf hg

Premises used: MeasureTheory.integral_integral_add
-- 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
inst_5 : SFinite μ
f g : α × β → E
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
⊢ ∫ (x : α), ∫ (y : β), f (x, y) - g (x, y) ∂ν ∂μ =
    HSub.hSub (α := E) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ) (∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ)

Tactic:
(integral_fn_integral_sub id hf hg).trans <|
    integral_sub hf.integral_prod_left hg.integral_prod_left

Premises used: MeasureTheory.Integrable.integral_prod_left, MeasureTheory.integral_fn_integral_sub, id, MeasureTheory.integral_sub, Eq.trans
-- 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
inst_5 : SFinite μ
f g : α × β → E
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
⊢ ∫ (x : α), ∫ (y : β), (f - g) (x, y) ∂ν ∂μ =
    HSub.hSub (α := E) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ) (∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ)

Tactic:
integral_integral_sub hf hg

Premises used: MeasureTheory.integral_integral_sub
-- 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
inst_5 : SFinite μ
rw :
  ∀ (x : ↥(Lp E 1 (μ.prod ν))),
    ContinuousAt (Y := E)
      (fun (f : ↥(Lp E 1 (μ.prod ν))) ↦ ∫ (x : α), ∫ (y : β), (↑(↑f : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y) ∂ν ∂μ) x
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 (μ.prod ν))) ↦
    ∫ (x : α), ∫ (y : β), (↑(↑f : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y) ∂ν ∂μ

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- 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
inst_5 : SFinite μ
g : ↥(Lp E 1 (μ.prod ν))
⊢ ContinuousAt (Y := E)
    (fun (f : ↥(Lp E 1 (μ.prod ν))) ↦ ∫ (x : α), ∫ (y : β), (↑(↑f : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y) ∂ν ∂μ) g

Tactic:
tendsto_integral_of_L1 _ (L1.integrable_coeFn g).integral_prod_left.aestronglyMeasurable
      (Eventually.of_forall fun h => (L1.integrable_coeFn h).integral_prod_left) ?_

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.tendsto_integral_of_L1, ContinuousAt, MeasureTheory.Integrable.integral_prod_left, MeasureTheory.L1.integrable_coeFn, Filter.Eventually.of_forall
-- 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
inst_5 : SFinite μ
g : ↥(Lp E 1 (μ.prod ν))
tendsto_integral_of_L1 :
  Tendsto (β := ℝ≥0∞)
    (fun (i : ↥(Lp E 1 (μ.prod ν))) ↦
      ∫⁻ (x : α),
        ‖HSub.hSub (α := E) (∫ (y : β), (↑(↑i : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y) ∂ν)
            (∫ (y : β), (↑(↑g : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y) ∂ν)‖ₑ ∂μ)
    (𝓝 g) (𝓝 0)
⊢ ContinuousAt (Y := E)
    (fun (f : ↥(Lp E 1 (μ.prod ν))) ↦ ∫ (x : α), ∫ (y : β), (↑(↑f : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y) ∂ν ∂μ) g

Tactic:
refine
    tendsto_integral_of_L1 _ (L1.integrable_coeFn g).integral_prod_left.aestronglyMeasurable
      (Eventually.of_forall fun h => (L1.integrable_coeFn h).integral_prod_left) ?_

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.tendsto_integral_of_L1, MeasureTheory.Integrable.integral_prod_left, MeasureTheory.L1.integrable_coeFn, Filter.Eventually.of_forall
-- 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
inst_5 : SFinite μ
g : ↥(Lp E 1 (μ.prod ν))
simp_rw :
  Tendsto (β := ℝ≥0∞)
    (fun (i : ↥(Lp E 1 (μ.prod ν))) ↦
      ∫⁻ (x : α),
        enorm.{u_3} (E := E)
          (∫ (y : β),
            (↑(↑i : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y) -
              (↑(↑g : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y) ∂ν) ∂μ)
    (𝓝 g) (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (i : ↥(Lp E 1 (μ.prod ν))) ↦
      ∫⁻ (x : α),
        ‖HSub.hSub (α := E) (∫ (y : β), (↑(↑i : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y) ∂ν)
            (∫ (y : β), (↑(↑g : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y) ∂ν)‖ₑ ∂μ)
    (𝓝 g) (𝓝 0)

Tactic:
simp_rw [← lintegral_fn_integral_sub _ (L1.integrable_coeFn _) (L1.integrable_coeFn g)]

Premises used: MeasureTheory.L1.integrable_coeFn, MeasureTheory.lintegral_fn_integral_sub
-- 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
inst_5 : SFinite μ
g : ↥(Lp E 1 (μ.prod ν))
apply : ↥(Lp E 1 (μ.prod ν)) → ℝ≥0∞
apply₁ :
  Tendsto (β := ℝ≥0∞)
    (fun (i : ↥(Lp E 1 (μ.prod ν))) ↦
      ∫⁻ (x : α),
        ∫⁻ (y : β),
          ‖(↑(↑i : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y) -
              (↑(↑g : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y)‖ₑ ∂ν ∂μ)
    (𝓝 g) (𝓝 0)
apply₂ :
  LE.le (α := ↥(Lp E 1 (μ.prod ν)) → ℝ≥0∞)
    (fun (i : ↥(Lp E 1 (μ.prod ν))) ↦
      ∫⁻ (x : α),
        enorm.{u_3} (E := E)
          (∫ (y : β),
            (↑(↑i : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y) -
              (↑(↑g : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y) ∂ν) ∂μ)
    fun (i : ↥(Lp E 1 (μ.prod ν))) ↦
    ∫⁻ (x : α),
      ∫⁻ (y : β),
        ‖(↑(↑i : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y) - (↑(↑g : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y)‖ₑ ∂ν ∂μ
⊢ Tendsto (β := ℝ≥0∞)
    (fun (i : ↥(Lp E 1 (μ.prod ν))) ↦
      ∫⁻ (x : α),
        enorm.{u_3} (E := E)
          (∫ (y : β),
            (↑(↑i : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y) -
              (↑(↑g : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y) ∂ν) ∂μ)
    (𝓝 g) (𝓝 0)

Tactic:
apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds _ (fun i => zero_le) _

Premises used: zero_le, tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds
-- 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
inst_5 : SFinite μ
g : ↥(Lp E 1 (μ.prod ν))
⊢ ↥(Lp E 1 (μ.prod ν)) → ℝ≥0∞

Tactic:
exact fun i => ∫⁻ x, ∫⁻ y, ‖i (x, y) - g (x, y)‖ₑ ∂ν ∂μ

Premises used: MeasureTheory.AEEqFun.cast, HSub.hSub, Prod.mk, ENorm.enorm, Subtype.val, MeasureTheory.lintegral