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
h1f : AEStronglyMeasurable f (μ.prod ν)
x : α
hx : ∀ᵐ (y : β) ∂ν, AEStronglyMeasurable.mk f h1f (x, y) = f (x, y)
⊢ HasFiniteIntegral.{u_2, u_3} (ε := E) (fun (y : β) ↦ AEStronglyMeasurable.mk f h1f (x, y)) ν ↔
    HasFiniteIntegral.{u_2, u_3} (ε := E) (fun (y : β) ↦ f (x, y)) ν

Tactic:
exact hasFiniteIntegral_congr hx

Premises used: MeasureTheory.hasFiniteIntegral_congr
-- 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
h1f : AEStronglyMeasurable f (μ.prod ν)
h₂ :
  (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν) fun (x : α) ↦
    ∫ (y : β), ‖f (x, y)‖ ∂ν
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν) μ ↔
    HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ∫ (y : β), ‖f (x, y)‖ ∂ν) μ

Tactic:
apply hasFiniteIntegral_congr

Premises used: MeasureTheory.hasFiniteIntegral_congr
-- 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
h1f : AEStronglyMeasurable f (μ.prod ν)
a : α
hx : ∀ᵐ (y : β) ∂ν, AEStronglyMeasurable.mk f h1f (a, y) = f (a, y)
⊢ Eq (α := ℝ) (∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (a, y)‖ ∂ν) (∫ (y : β), ‖f (a, y)‖ ∂ν)

Tactic:
integral_congr_ae (EventuallyEq.fun_comp hx _)

Premises used: MeasureTheory.integral_congr_ae, Filter.EventuallyEq.fun_comp
-- 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
h1f : AEStronglyMeasurable f (μ.prod ν)
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α | (fun (x : α) ↦ ∀ᵐ (y : β) ∂ν, AEStronglyMeasurable.mk f h1f (x, y) = f (x, y)) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦
                  Eq (α := ℝ) ((fun (x : α) ↦ (∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν : ℝ)) x)
                    ((fun (x : α) ↦ (∫ (y : β), ‖f (x, y)‖ ∂ν : ℝ)) x))
                x}
            x}
      a
h₁ h₂ :
  ∀ (a : α) (hx : ∀ᵐ (y : β) ∂ν, AEStronglyMeasurable.mk f h1f (a, y) = f (a, y)),
    Eq (α := ℝ) (∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (a, y)‖ ∂ν) (∫ (y : β), ‖f (a, y)‖ ∂ν)
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν) fun (x : α) ↦
    ∫ (y : β), ‖f (x, y)‖ ∂ν

Tactic:
filter_upwards [ae_ae_of_ae_prod h1f.ae_eq_mk.symm] with _ hx using
      integral_congr_ae (EventuallyEq.fun_comp hx _)

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.Measure.ae_ae_of_ae_prod, Filter.EventuallyEq.symm
-- 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
h1f : AEStronglyMeasurable f (μ.prod ν)
⊢ Integrable f (μ.prod ν) ↔
    (∀ᵐ (x : α) ∂μ, Integrable.{u_3, u_2} (ε := E) (fun (y : β) ↦ f (x, y)) ν) ∧
      Integrable (ε := ℝ) (fun (x : α) ↦ ∫ (y : β), ‖f (x, y)‖ ∂ν) μ

Tactic:
simp [Integrable, h1f, hasFiniteIntegral_prod_iff', h1f.norm.integral_prod_right',
    h1f.prodMk_left]

Premises used: MeasureTheory.hasFiniteIntegral_prod_iff', MeasureTheory.Integrable, MeasureTheory.AEStronglyMeasurable.norm, MeasureTheory.AEStronglyMeasurable.integral_prod_right', MeasureTheory.AEStronglyMeasurable.prodMk_left
-- 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
h1f : AEStronglyMeasurable f (μ.prod ν)
⊢ Integrable (ε := E) (fun (z : β × α) ↦ f z.swap) (ν.prod μ) ↔
    (∀ᵐ (x : β) ∂ν, Integrable.{u_3, u_1} (ε := E) (fun (y : α) ↦ f (x, y).swap) μ) ∧
      Integrable (ε := ℝ) (fun (x : β) ↦ ∫ (y : α), ‖f (x, y).swap‖ ∂μ) ν

Tactic:
integrable_prod_iff h1f.prod_swap

Premises used: MeasureTheory.integrable_prod_iff, MeasureTheory.AEStronglyMeasurable.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 : SFinite μ
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
h : Integrable f (μ.prod ν) ↔ Integrable (ε := E) (fun (z : β × α) ↦ f z.swap) (ν.prod μ)
⊢ Integrable f (μ.prod ν) ↔
    (∀ᵐ (y : β) ∂ν, Integrable.{u_3, u_1} (ε := E) (fun (x : α) ↦ f (x, y)) μ) ∧
      Integrable (ε := ℝ) (fun (y : β) ↦ ∫ (x : α), ‖f (x, y)‖ ∂μ) ν

Tactic:
convert! integrable_prod_iff h1f.prod_swap using 1

Premises used: MeasureTheory.integrable_prod_iff, MeasureTheory.AEStronglyMeasurable.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 : SFinite μ
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
h : Integrable f (μ.prod ν) ↔ Integrable (ε := E) (fun (x : β × α) ↦ (f ∘ Prod.swap) x) (ν.prod μ)
h₁ h₂ : Integrable f (μ.prod ν) ↔ Integrable f (μ.prod ν)
⊢ Integrable f (μ.prod ν) ↔ Integrable (ε := E) (fun (z : β × α) ↦ f z.swap) (ν.prod μ)

Tactic:
rw [funext fun _ => Function.comp_apply.symm, integrable_swap_iff]

Premises used: funext, MeasureTheory.integrable_swap_iff, Function.comp_apply, Eq.symm
-- 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 f (μ.prod ν)
⊢ ∀ᵐ (y : β) ∂ν, Integrable.{u_3, u_1} (ε := E) (fun (x : α) ↦ f (x, y)) μ

Tactic:
((integrable_prod_iff' hf.aestronglyMeasurable).mp hf).1

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, And.left, MeasureTheory.integrable_prod_iff', Iff.mp
-- 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 f (μ.prod ν)
⊢ ∀ᵐ (x : α) ∂μ, Integrable.{u_3, u_2} (ε := E) (fun (y : β) ↦ f (x, y)) ν

Tactic:
hf.swap.prod_left_ae

Premises used: MeasureTheory.Integrable.swap, MeasureTheory.Integrable.prod_left_ae, 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 ν
f : α × β → E
hf : Integrable f (μ.prod ν)
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ∫ (y : β), ‖f (x, y)‖ ∂ν) μ

Tactic:
((integrable_prod_iff hf.aestronglyMeasurable).mp hf).2

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.integrable_prod_iff, And.right, Iff.mp
-- 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 f (μ.prod ν)
⊢ Integrable (ε := ℝ) (fun (y : β) ↦ ∫ (x : α), ‖f (x, y)‖ ∂μ) ν

Tactic:
hf.swap.integral_norm_prod_left

Premises used: MeasureTheory.Integrable.integral_norm_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
F : Type u_4
G : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : NormedAddCommGroup G
op : E → F → G
hop : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry op)
hop_norm : ∃ (C : ℝ), ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
right : HasFiniteIntegral (ε := G) (fun (z : α × β) ↦ op (f z.1) (g z.2)) (μ.prod ν)
⊢ Integrable (ε := G) (fun (z : α × β) ↦ op (f z.1) (g z.2)) (μ.prod ν)

Tactic:
use hop.comp_aestronglyMeasurable₂ hf.1.comp_fst hg.1.comp_snd

Premises used: And.left, MeasureTheory.AEStronglyMeasurable.comp_fst, MeasureTheory.AEStronglyMeasurable.comp_snd, Continuous.comp_aestronglyMeasurable₂
-- 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
F : Type u_4
G : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : NormedAddCommGroup G
op : E → F → G
hop : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry op)
hop_norm : ∃ (C : ℝ), ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
right :
  ∀ (C : ℝ) (hC : ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖),
    HasFiniteIntegral (ε := G) (fun (z : α × β) ↦ op (f z.1) (g z.2)) (μ.prod ν)
⊢ HasFiniteIntegral (ε := G) (fun (z : α × β) ↦ op (f z.1) (g z.2)) (μ.prod ν)

Tactic:
rcases hop_norm with ⟨C, hC⟩
-- 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
F : Type u_4
G : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : NormedAddCommGroup G
op : E → F → G
hop : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry op)
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
C : ℝ
hC : ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖
hfg : ∀ (z : α × β), ‖op (f z.1) (g z.2)‖ₑ ≤ ENNReal.ofReal C * ‖f z.1‖ₑ * ‖g z.2‖ₑ
⊢ ∫⁻ (z : α × β), ‖op (f z.1) (g z.2)‖ₑ ∂μ.prod ν ≤ ∫⁻ (z : α × β), ENNReal.ofReal C * ‖f z.1‖ₑ * ‖g z.2‖ₑ ∂μ.prod ν

Tactic:
gcongr with z
-- 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
F : Type u_4
G : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : NormedAddCommGroup G
op : E → F → G
hop : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry op)
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
C : ℝ
hC : ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖
z : α × β
hfg : ‖op (f z.1) (g z.2)‖ ≤ (↑C.toNNReal : ℝ) * ‖f z.1‖ * ‖g z.2‖
⊢ ‖op (f z.1) (g z.2)‖ₑ ≤ ENNReal.ofReal C * ‖f z.1‖ₑ * ‖g z.2‖ₑ

Tactic:
simp only [enorm_eq_nnnorm, ENNReal.ofReal, ← ENNReal.coe_mul, ENNReal.coe_le_coe,
        ← NNReal.coe_le_coe, NNReal.coe_mul, coe_nnnorm]

Premises used: ENNReal.ofReal, ENNReal.coe_le_coe, enorm_eq_nnnorm, ENNReal.coe_mul, coe_nnnorm, NNReal.coe_mul, NNReal.coe_le_coe
-- 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
F : Type u_4
G : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : NormedAddCommGroup G
op : E → F → G
hop : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry op)
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
C : ℝ
hC : ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖
z : α × β
⊢ ‖op (f z.1) (g z.2)‖ ≤ (↑C.toNNReal : ℝ) * ‖f z.1‖ * ‖g z.2‖

Tactic:
(hC _ _).trans ?_

Premises used: LE.le.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
F : Type u_4
G : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : NormedAddCommGroup G
op : E → F → G
hop : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry op)
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
C : ℝ
hC : ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖
z : α × β
hfg : C * ‖f z.1‖ * ‖g z.2‖ ≤ (↑C.toNNReal : ℝ) * ‖f z.1‖ * ‖g z.2‖
⊢ ‖op (f z.1) (g z.2)‖ ≤ (↑C.toNNReal : ℝ) * ‖f z.1‖ * ‖g z.2‖

Tactic:
refine (hC _ _).trans ?_

Premises used: LE.le.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
F : Type u_4
G : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : NormedAddCommGroup G
op : E → F → G
hop : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry op)
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
C : ℝ
hC : ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖
z : α × β
hfg : C ≤ (↑C.toNNReal : ℝ)
⊢ C * ‖f z.1‖ * ‖g z.2‖ ≤ (↑C.toNNReal : ℝ) * ‖f z.1‖ * ‖g z.2‖

Tactic:
gcongr
-- 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
F : Type u_4
G : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : NormedAddCommGroup G
op : E → F → G
hop : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry op)
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
C : ℝ
hC : ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖
z : α × β
⊢ C ≤ (↑C.toNNReal : ℝ)

Tactic:
apply le_coe_toNNReal

Premises used: Real.le_coe_toNNReal
-- 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
F : Type u_4
G : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : NormedAddCommGroup G
op : E → F → G
hop : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry op)
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
C : ℝ
hC : ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖
⊢ ∫⁻ (z : α × β), ENNReal.ofReal C * ‖f z.1‖ₑ * ‖g z.2‖ₑ ∂μ.prod ν ≤
    ∫⁻ (x : α), ∫⁻ (y : β), ENNReal.ofReal C * ‖f x‖ₑ * ‖g y‖ₑ ∂ν ∂μ

Tactic:
lintegral_prod_le _

Premises used: MeasureTheory.lintegral_prod_le
-- 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
F : Type u_4
G : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : NormedAddCommGroup G
op : E → F → G
hop : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry op)
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
C : ℝ
hC : ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖
⊢ ∫⁻ (x : α), ∫⁻ (y : β), ENNReal.ofReal C * ‖f x‖ₑ * ‖g y‖ₑ ∂ν ∂μ ≤
    (ENNReal.ofReal C * ∫⁻ (x : α), ‖f x‖ₑ ∂μ) * ∫⁻ (y : β), ‖g y‖ₑ ∂ν

Tactic:
simp [lintegral_const_mul', lintegral_mul_const', hg.2.ne, mul_assoc]

Premises used: MeasureTheory.lintegral_const_mul', mul_assoc, And.right, MeasureTheory.lintegral_mul_const', LT.lt.ne
-- 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
F : Type u_4
G : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : NormedAddCommGroup G
op : E → F → G
hop : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry op)
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
C : ℝ
hC : ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖
⊢ (ENNReal.ofReal C * ∫⁻ (x : α), ‖f x‖ₑ ∂μ) * ∫⁻ (y : β), ‖g y‖ₑ ∂ν < ∞

Tactic:
apply_rules [ENNReal.mul_lt_top, hf.2, hg.2, ENNReal.ofReal_lt_top]

Premises used: ENNReal.ofReal_lt_top, ENNReal.mul_lt_top, And.right
-- 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
F : Type u_4
G : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : NormedAddCommGroup G
op : E → F → G
hop : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry op)
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
C : ℝ
hC : ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖
ν₁ : ∫⁻ (z : α × β), ‖op (f z.1) (g z.2)‖ₑ ∂μ.prod ν ≤ ∫⁻ (z : α × β), ENNReal.ofReal C * ‖f z.1‖ₑ * ‖g z.2‖ₑ ∂μ.prod ν
ν₂ :
  ∫⁻ (x : α), ∫⁻ (y : β), ENNReal.ofReal C * ‖f x‖ₑ * ‖g y‖ₑ ∂ν ∂μ ≤
    (ENNReal.ofReal C * ∫⁻ (x : α), ‖f x‖ₑ ∂μ) * ∫⁻ (y : β), ‖g y‖ₑ ∂ν
ν₃ : (ENNReal.ofReal C * ∫⁻ (x : α), ‖f x‖ₑ ∂μ) * ∫⁻ (y : β), ‖g y‖ₑ ∂ν < ∞
⊢ HasFiniteIntegral (ε := G) (fun (z : α × β) ↦ op (f z.1) (g z.2)) (μ.prod ν)

Tactic:
calc
    ∫⁻ z, ‖op (f z.1) (g z.2)‖ₑ ∂μ.prod ν ≤ ∫⁻ z, .ofReal C * ‖f z.1‖ₑ * ‖g z.2‖ₑ ∂μ.prod ν := by
      gcongr with z
      simp only [enorm_eq_nnnorm, ENNReal.ofReal, ← ENNReal.coe_mul, ENNReal.coe_le_coe,
        ← NNReal.coe_le_coe, NNReal.coe_mul, coe_nnnorm]
      refine (hC _ _).trans ?_
      gcongr
      apply le_coe_toNNReal
    _ ≤ ∫⁻ x, ∫⁻ y, .ofReal C * ‖f x‖ₑ * ‖g y‖ₑ ∂ν ∂μ := lintegral_prod_le _
    _ ≤ .ofReal C * (∫⁻ x, ‖f x‖ₑ ∂μ) * ∫⁻ y, ‖g y‖ₑ ∂ν := by
      simp [lintegral_const_mul', lintegral_mul_const', hg.2.ne, mul_assoc]
    _ < ∞ := by apply_rules [ENNReal.mul_lt_top, hf.2, hg.2, ENNReal.ofReal_lt_top]

Premises used: ENorm.enorm, MeasureTheory.Measure.prod, MeasureTheory.lintegral_prod_le, MeasureTheory.lintegral
-- 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
f : α → E
hf : Integrable f μ
ν : Measure β
inst_3 : IsFiniteMeasure ν
rw : ∀ (hf : MemLp f 1 μ) (ν : Measure β) [IsFiniteMeasure ν], MemLp (ε := E) (fun (x : α × β) ↦ f x.1) 1 (μ.prod ν)
⊢ Integrable (ε := E) (fun (x : α × β) ↦ f x.1) (μ.prod ν)

Tactic:
rw [← memLp_one_iff_integrable] at hf ⊢

Premises used: MeasureTheory.memLp_one_iff_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
f : α → E
hf : MemLp f 1 μ
ν : Measure β
inst_3 : IsFiniteMeasure ν
⊢ MemLp (ε := E) (fun (x : α × β) ↦ f x.1) 1 (μ.prod ν)

Tactic:
hf.comp_fst ν

Premises used: MeasureTheory.MemLp.comp_fst
-- 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
f : α → E
hf : MemLp f 1 μ
ν : Measure β
inst_3 : IsFiniteMeasure ν
⊢ MemLp (ε := E) (fun (x : α × β) ↦ f x.1) 1 (μ.prod ν)

Tactic:
exact hf.comp_fst ν

Premises used: MeasureTheory.MemLp.comp_fst
-- 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 : SFinite ν
f : β → E
hf : Integrable f ν
μ : Measure α
inst_4 : IsFiniteMeasure μ
rw : ∀ (hf : MemLp f 1 ν) (μ : Measure α) [IsFiniteMeasure μ], MemLp (ε := E) (fun (x : α × β) ↦ f x.2) 1 (μ.prod ν)
⊢ Integrable (ε := E) (fun (x : α × β) ↦ f x.2) (μ.prod ν)

Tactic:
rw [← memLp_one_iff_integrable] at hf ⊢

Premises used: MeasureTheory.memLp_one_iff_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 : SFinite ν
f : β → E
hf : MemLp f 1 ν
μ : Measure α
inst_4 : IsFiniteMeasure μ
⊢ MemLp (ε := E) (fun (x : α × β) ↦ f x.2) 1 (μ.prod ν)

Tactic:
hf.comp_snd μ

Premises used: MeasureTheory.MemLp.comp_snd
-- 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 : SFinite ν
f : β → E
hf : MemLp f 1 ν
μ : Measure α
inst_4 : IsFiniteMeasure μ
⊢ MemLp (ε := E) (fun (x : α × β) ↦ f x.2) 1 (μ.prod ν)

Tactic:
exact hf.comp_snd μ

Premises used: MeasureTheory.MemLp.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
R : Type u_4
inst_3 : NormedRing R
inst_4 : Module R E
inst_5 : IsBoundedSMul R E
f : α → R
g : β → E
hf : Integrable f μ
hg : Integrable g ν
⊢ ∀ (x : R) (y : E), ‖x • y‖ ≤ 1 * ‖x‖ * ‖y‖

Tactic:
simpa using norm_smul_le

Premises used: norm_smul_le
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
L : Type u_4
inst_2 : NormedRing L
f : α → L
g : β → L
hf : Integrable f μ
hg : Integrable g ν
⊢ Integrable (ε := L) (fun (z : α × β) ↦ f z.1 * g z.2) (μ.prod ν)

Tactic:
hf.smul_prod hg

Premises used: MeasureTheory.Integrable.smul_prod
-- 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
s : Set α
t : Set β
hf : IntegrableOn f (s ×ˢ t) (μ.prod ν)
rw :
  ∀ (hf : Integrable f ((μ.restrict s).prod (ν.restrict t))),
    Integrable (f ∘ Prod.swap) ((ν.restrict t).prod (μ.restrict s))
⊢ IntegrableOn (f ∘ Prod.swap) (t ×ˢ s) (ν.prod μ)

Tactic:
rw [IntegrableOn, ← Measure.prod_restrict] at hf ⊢

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.Measure.prod_restrict
-- 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
s : Set α
t : Set β
hf : Integrable f ((μ.restrict s).prod (ν.restrict t))
⊢ Integrable (f ∘ Prod.swap) ((ν.restrict t).prod (μ.restrict s))

Tactic:
hf.swap

Premises used: 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 : SFinite μ
f : α × β → E
s : Set α
t : Set β
hf : Integrable f ((μ.restrict s).prod (ν.restrict t))
⊢ Integrable (f ∘ Prod.swap) ((ν.restrict t).prod (μ.restrict s))

Tactic:
exact hf.swap

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

Tactic:
rcases hf with ⟨hf_meas, hf_fin⟩
-- 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
hf : Integrable (ε := E) (fun (x : α × β) ↦ f x.2) (μ.prod ν)
hμ : μ ≠ 0
hf_meas : AEStronglyMeasurable (β := E) (fun (x : α × β) ↦ f x.2) (μ.prod ν)
⊢ HasFiniteIntegral (ε := E) (fun (x : α × β) ↦ f x.2) (μ.prod ν)

Tactic:
rcases hf with ⟨hf_meas, hf_fin⟩