awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : SFinite μ
a b : ℝ
f : ℝ → α → E
h_int : @Integrable _ _ _ _ Prod.instMeasurableSpace (uncurry f) (Measure.prod (Measure.restrict volume (uIoc a b)) μ)
inl :
  ∀ (hab : a ≤ b),
    Eq.{u_3 + 1} (α := E) (∫ (x : ℝ) in a..b, ∫ (y : α), f x y ∂μ) (∫ (y : α), ∫ (x : ℝ) in a..b, f x y ∂μ)
inr :
  ∀ (hab : b ≤ a),
    Eq.{u_3 + 1} (α := E) (∫ (x : ℝ) in a..b, ∫ (y : α), f x y ∂μ) (∫ (y : α), ∫ (x : ℝ) in a..b, f x y ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : ℝ) in a..b, ∫ (y : α), f x y ∂μ) (∫ (y : α), ∫ (x : ℝ) in a..b, f x y ∂μ)

Tactic:
rcases le_total a b with (hab | hab)

Premises used: le_total
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : SFinite μ
a b : ℝ
f : ℝ → α → E
h_int : @Integrable _ _ _ _ Prod.instMeasurableSpace (uncurry f) (Measure.prod (Measure.restrict volume (uIoc a b)) μ)
hab : a ≤ b
inl :
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ ∫ (y : α), f x y ∂μ)
    (∫ (y : α), @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ f x y ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : ℝ) in a..b, ∫ (y : α), f x y ∂μ) (∫ (y : α), ∫ (x : ℝ) in a..b, f x y ∂μ)

Tactic:
simp_rw [intervalIntegral.integral_of_le hab]

Premises used: intervalIntegral.integral_of_le
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : SFinite μ
a b : ℝ
f : ℝ → α → E
h_int : @Integrable _ _ _ _ Prod.instMeasurableSpace (uncurry f) (Measure.prod (Measure.restrict volume (uIoc a b)) μ)
hab : a ≤ b
⊢ @Integrable _ _ _ _ Prod.instMeasurableSpace (uncurry f) (Measure.prod (Measure.restrict volume (Ioc a b)) μ)

Tactic:
simp only [hab, Set.uIoc_of_le] at h_int

Premises used: Set.uIoc_of_le
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : SFinite μ
a b : ℝ
f : ℝ → α → E
hab : a ≤ b
h_int : @Integrable _ _ _ _ Prod.instMeasurableSpace (uncurry f) (Measure.prod (Measure.restrict volume (Ioc a b)) μ)
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ ∫ (y : α), f x y ∂μ)
    (∫ (y : α), @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ f x y ∂μ)

Tactic:
integral_integral_swap h_int

Premises used: MeasureTheory.integral_integral_swap
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : SFinite μ
a b : ℝ
f : ℝ → α → E
hab : a ≤ b
h_int : @Integrable _ _ _ _ Prod.instMeasurableSpace (uncurry f) (Measure.prod (Measure.restrict volume (Ioc a b)) μ)
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ ∫ (y : α), f x y ∂μ)
    (∫ (y : α), @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ f x y ∂μ)

Tactic:
exact integral_integral_swap h_int

Premises used: MeasureTheory.integral_integral_swap
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : SFinite μ
a b : ℝ
f : ℝ → α → E
h_int : @Integrable _ _ _ _ Prod.instMeasurableSpace (uncurry f) (Measure.prod (Measure.restrict volume (uIoc a b)) μ)
hab : b ≤ a
inr :
  Eq.{u_3 + 1} (α := E)
    (-@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ ∫ (y : α), f x y ∂μ)
    (∫ (y : α), -@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x y ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : ℝ) in a..b, ∫ (y : α), f x y ∂μ) (∫ (y : α), ∫ (x : ℝ) in a..b, f x y ∂μ)

Tactic:
simp_rw [intervalIntegral.integral_of_ge hab]

Premises used: intervalIntegral.integral_of_ge
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : SFinite μ
a b : ℝ
f : ℝ → α → E
h_int : @Integrable _ _ _ _ Prod.instMeasurableSpace (uncurry f) (Measure.prod (Measure.restrict volume (uIoc a b)) μ)
hab : b ≤ a
⊢ @Integrable _ _ _ _ Prod.instMeasurableSpace (uncurry f) (Measure.prod (Measure.restrict volume (Ioc b a)) μ)

Tactic:
simp only [hab, Set.uIoc_of_ge] at h_int

Premises used: Set.uIoc_of_ge
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : SFinite μ
a b : ℝ
f : ℝ → α → E
hab : b ≤ a
h_int : @Integrable _ _ _ _ Prod.instMeasurableSpace (uncurry f) (Measure.prod (Measure.restrict volume (Ioc b a)) μ)
inr :
  Eq.{u_3 + 1} (α := E)
    (-∫ (y : α),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x y ∂μ)
    (∫ (y : α), -@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x y ∂μ)
inr₁ inr₂ :
  Eq.{u_3 + 1} (α := E)
    (-∫ (y : α),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x y ∂μ)
    (-∫ (a_1 : α), @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x a_1 ∂μ)
⊢ Eq.{u_3 + 1} (α := E)
    (-@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ ∫ (y : α), f x y ∂μ)
    (∫ (y : α), -@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x y ∂μ)

Tactic:
rw [integral_integral_swap h_int, integral_neg]

Premises used: MeasureTheory.integral_neg, MeasureTheory.integral_integral_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
s : Set α
t : Set β
hf : IntegrableOn f (s ×ˢ t) (μ.prod ν)
simp :
  ∀ (hf : Integrable f ((μ.restrict s).prod (ν.restrict t))),
    Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂(μ.restrict s).prod (ν.restrict t))
      (∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂ν ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν) (∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂ν ∂μ)

Tactic:
simp only [← Measure.prod_restrict s t, IntegrableOn] 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 : NormedSpace ℝ E
inst_5 : SFinite μ
f : α × β → E
s : Set α
t : Set β
hf : Integrable f ((μ.restrict s).prod (ν.restrict t))
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂(μ.restrict s).prod (ν.restrict t))
    (∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂ν ∂μ)

Tactic:
integral_prod f hf

Premises used: MeasureTheory.integral_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 : NormedSpace ℝ E
inst_5 : SFinite μ
f : α × β → E
s : Set α
t : Set β
hf : Integrable f ((μ.restrict s).prod (ν.restrict t))
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂(μ.restrict s).prod (ν.restrict t))
    (∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂ν ∂μ)

Tactic:
exact integral_prod f hf

Premises used: MeasureTheory.integral_prod
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
E : Type u_5
F : Type u_6
G : Type u_7
𝕜 : Type u_8
inst_4 : RCLike 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedSpace 𝕜 E
inst_8 : CompleteSpace E
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace ℝ F
inst_11 : NormedSpace 𝕜 F
inst_12 : CompleteSpace F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace ℝ G
inst_15 : NormedSpace 𝕜 G
inst_16 : CompleteSpace G
B : E →L[𝕜] F →L[𝕜] G
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (uncurry fun (x : E) ↦ (⇑((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G))

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
E : Type u_5
F : Type u_6
G : Type u_7
𝕜 : Type u_8
inst_4 : RCLike 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedSpace 𝕜 E
inst_8 : CompleteSpace E
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace ℝ F
inst_11 : NormedSpace 𝕜 F
inst_12 : CompleteSpace F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace ℝ G
inst_15 : NormedSpace 𝕜 G
inst_16 : CompleteSpace G
B : E →L[𝕜] F →L[𝕜] G
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
⊢ Integrable (ε := G) (fun (z : α × β) ↦ (((B : (a : E) → F →L[𝕜] G) (f z.1) : F →L[𝕜] G) : (a : F) → G) (g z.2))
    (μ.prod ν)

Tactic:
have : Integrable (fun z ↦ B (f z.1) (g z.2)) (μ.prod ν) :=
    hf.op_fst_snd (by fun_prop) ⟨‖B‖, B.le_opNorm₂⟩ hg
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
E : Type u_5
F : Type u_6
G : Type u_7
𝕜 : Type u_8
inst_4 : RCLike 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedSpace 𝕜 E
inst_8 : CompleteSpace E
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace ℝ F
inst_11 : NormedSpace 𝕜 F
inst_12 : CompleteSpace F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace ℝ G
inst_15 : NormedSpace 𝕜 G
inst_16 : CompleteSpace G
B : E →L[𝕜] F →L[𝕜] G
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
this :
  Integrable (ε := G) (fun (z : α × β) ↦ (((B : (a : E) → F →L[𝕜] G) (f z.1) : F →L[𝕜] G) : (a : F) → G) (g z.2))
    (μ.prod ν)
simp_rw :
  Eq.{u_7 + 1} (α := G)
    (∫ (x : α), (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (∫ (x : β), g x ∂ν) ∂μ : G)
    (((B : (a : E) → F →L[𝕜] G) (∫ (x : α), f x ∂μ) : (a : F) → G) (∫ (x : β), g x ∂ν) : G)
⊢ Eq.{u_7 + 1} (α := G)
    (∫ (z : α × β), (((B : (a : E) → F →L[𝕜] G) (f z.1) : F →L[𝕜] G) : (a : F) → G) (g z.2) ∂μ.prod ν : G)
    (((B : (a : E) → F →L[𝕜] G) (∫ (x : α), f x ∂μ) : (a : F) → G) (∫ (y : β), g y ∂ν) : G)

Tactic:
simp_rw [integral_prod _ this, ContinuousLinearMap.integral_comp_comm _ hg]

Premises used: ContinuousLinearMap.integral_comp_comm, MeasureTheory.integral_prod
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
E : Type u_5
F : Type u_6
G : Type u_7
𝕜 : Type u_8
inst_4 : RCLike 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedSpace 𝕜 E
inst_8 : CompleteSpace E
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace ℝ F
inst_11 : NormedSpace 𝕜 F
inst_12 : CompleteSpace F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace ℝ G
inst_15 : NormedSpace 𝕜 G
inst_16 : CompleteSpace G
B : E →L[𝕜] F →L[𝕜] G
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
this :
  Integrable (ε := G) (fun (z : α × β) ↦ (((B : (a : E) → F →L[𝕜] G) (f z.1) : F →L[𝕜] G) : (a : F) → G) (g z.2))
    (μ.prod ν)
change :
  Eq.{u_7 + 1} (α := G)
    (∫ (x : α),
        (((ContinuousLinearMap.flip.{u_8, u_8, u_8, u_5, u_6, u_7} (𝕜 := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜) (E := E) (F := F) (G :=
                    G) (σ₂₃ := RingHom.id 𝕜) (σ₁₃ := RingHom.id 𝕜) B :
                  F →L[𝕜] E →L[𝕜] G) :
                (a : F) → E →L[𝕜] G)
              (∫ (y : β), g y ∂ν) :
            (a : E) → G)
          (f x) ∂μ :
      G)
    (((B : (a : E) → F →L[𝕜] G) (∫ (x : α), f x ∂μ) : (a : F) → G) (∫ (x : β), g x ∂ν) : G)
⊢ Eq.{u_7 + 1} (α := G)
    (∫ (x : α), (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (∫ (x : β), g x ∂ν) ∂μ : G)
    (((B : (a : E) → F →L[𝕜] G) (∫ (x : α), f x ∂μ) : (a : F) → G) (∫ (x : β), g x ∂ν) : G)

Tactic:
change ∫ x, B.flip (∫ y, g y ∂ν) (f x) ∂μ = _
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
E : Type u_5
F : Type u_6
G : Type u_7
𝕜 : Type u_8
inst_4 : RCLike 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedSpace 𝕜 E
inst_8 : CompleteSpace E
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace ℝ F
inst_11 : NormedSpace 𝕜 F
inst_12 : CompleteSpace F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace ℝ G
inst_15 : NormedSpace 𝕜 G
inst_16 : CompleteSpace G
B : E →L[𝕜] F →L[𝕜] G
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
this :
  Integrable (ε := G) (fun (z : α × β) ↦ (((B : (a : E) → F →L[𝕜] G) (f z.1) : F →L[𝕜] G) : (a : F) → G) (g z.2))
    (μ.prod ν)
rw :
  Eq.{u_7 + 1} (α := G)
    ((((ContinuousLinearMap.flip.{u_8, u_8, u_8, u_5, u_6, u_7} (𝕜 := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜) (E := E) (F := F) (G := G)
                  (σ₂₃ := RingHom.id 𝕜) (σ₁₃ := RingHom.id 𝕜) B :
                F →L[𝕜] E →L[𝕜] G) :
              (a : F) → E →L[𝕜] G)
            (∫ (y : β), g y ∂ν) :
          (a : E) → G)
        (∫ (x : α), f x ∂μ) :
      G)
    (((B : (a : E) → F →L[𝕜] G) (∫ (x : α), f x ∂μ) : (a : F) → G) (∫ (x : β), g x ∂ν) : G)
⊢ Eq.{u_7 + 1} (α := G)
    (∫ (x : α),
        (((ContinuousLinearMap.flip.{u_8, u_8, u_8, u_5, u_6, u_7} (𝕜 := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜) (E := E) (F := F) (G :=
                    G) (σ₂₃ := RingHom.id 𝕜) (σ₁₃ := RingHom.id 𝕜) B :
                  F →L[𝕜] E →L[𝕜] G) :
                (a : F) → E →L[𝕜] G)
              (∫ (y : β), g y ∂ν) :
            (a : E) → G)
          (f x) ∂μ :
      G)
    (((B : (a : E) → F →L[𝕜] G) (∫ (x : α), f x ∂μ) : (a : F) → G) (∫ (x : β), g x ∂ν) : G)

Tactic:
rw [ContinuousLinearMap.integral_comp_comm _ hf]

Premises used: ContinuousLinearMap.integral_comp_comm
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
E : Type u_5
F : Type u_6
G : Type u_7
𝕜 : Type u_8
inst_4 : RCLike 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedSpace 𝕜 E
inst_8 : CompleteSpace E
inst_9 : NormedAddCommGroup F
inst_10 : NormedSpace ℝ F
inst_11 : NormedSpace 𝕜 F
inst_12 : CompleteSpace F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace ℝ G
inst_15 : NormedSpace 𝕜 G
inst_16 : CompleteSpace G
B : E →L[𝕜] F →L[𝕜] G
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
this :
  Integrable (ε := G) (fun (z : α × β) ↦ (((B : (a : E) → F →L[𝕜] G) (f z.1) : F →L[𝕜] G) : (a : F) → G) (g z.2))
    (μ.prod ν)
⊢ Eq.{u_7 + 1} (α := G)
    ((((ContinuousLinearMap.flip.{u_8, u_8, u_8, u_5, u_6, u_7} (𝕜 := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜) (E := E) (F := F) (G := G)
                  (σ₂₃ := RingHom.id 𝕜) (σ₁₃ := RingHom.id 𝕜) B :
                F →L[𝕜] E →L[𝕜] G) :
              (a : F) → E →L[𝕜] G)
            (∫ (y : β), g y ∂ν) :
          (a : E) → G)
        (∫ (x : α), f x ∂μ) :
      G)
    (((B : (a : E) → F →L[𝕜] G) (∫ (x : α), f x ∂μ) : (a : F) → G) (∫ (x : β), g x ∂ν) : G)

Tactic:
simp
-- 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 μ
𝕜 : Type u_5
inst_6 : RCLike 𝕜
inst_7 : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
pos :
  ∀ (hE : CompleteSpace E),
    ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν =
      HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)
neg :
  ∀ (hE : ¬CompleteSpace E),
    ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν =
      HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν =
    HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)

Tactic:
by_cases hE : CompleteSpace E

Premises used: CompleteSpace
-- 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 μ
𝕜 : Type u_5
inst_6 : RCLike 𝕜
inst_7 : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : ¬CompleteSpace E
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν =
    HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)

Tactic:
simp [integral, hE]

Premises used: MeasureTheory.integral
-- 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 μ
𝕜 : Type u_5
inst_6 : RCLike 𝕜
inst_7 : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : CompleteSpace E
pos :
  ∀ (h : Integrable (ε := E) (fun (z : α × β) ↦ f z.1 • g z.2) (μ.prod ν)),
    ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν =
      HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)
neg :
  ∀ (h : ¬Integrable (ε := E) (fun (z : α × β) ↦ f z.1 • g z.2) (μ.prod ν)),
    ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν =
      HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν =
    HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)

Tactic:
by_cases h : Integrable (fun z : α × β => f z.1 • g z.2) (μ.prod ν)

Premises used: MeasureTheory.Integrable, Prod.fst, MeasureTheory.Measure.prod, HSMul.hSMul, Prod.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
inst_5 : SFinite μ
𝕜 : Type u_5
inst_6 : RCLike 𝕜
inst_7 : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : CompleteSpace E
h : Integrable (ε := E) (fun (z : α × β) ↦ f z.1 • g z.2) (μ.prod ν)
pos :
  ∫ (x : α), ∫ (y : β), f (x, y).1 • g (x, y).2 ∂ν ∂μ =
    HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν =
    HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)

Tactic:
rw [integral_prod _ h]

Premises used: MeasureTheory.integral_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 : NormedSpace ℝ E
inst_5 : SFinite μ
𝕜 : Type u_5
inst_6 : RCLike 𝕜
inst_7 : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : CompleteSpace E
h : Integrable (ε := E) (fun (z : α × β) ↦ f z.1 • g z.2) (μ.prod ν)
pos pos₁ :
  ∫ (x : α), ∫ (y : β), f x • g y ∂ν ∂μ =
    HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)
pos₂ :
  ∫ (x : α), HSMul.hSMul (β := E) (f x) (∫ (a : β), g a ∂ν) ∂μ =
    HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (a : β), g a ∂ν)
⊢ ∫ (x : α), ∫ (y : β), f (x, y).1 • g (x, y).2 ∂ν ∂μ =
    HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)

Tactic:
simp_rw [integral_smul, integral_smul_const]

Premises used: integral_smul_const, MeasureTheory.integral_smul
-- 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 μ
𝕜 : Type u_5
inst_6 : RCLike 𝕜
inst_7 : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : CompleteSpace E
h : ¬Integrable (ε := E) (fun (z : α × β) ↦ f z.1 • g z.2) (μ.prod ν)
contrapose! : ∀ (h : Integrable f μ ∧ Integrable g ν), Integrable (ε := E) (fun (z : α × β) ↦ f z.1 • g z.2) (μ.prod ν)
⊢ ¬Integrable f μ ∨ ¬Integrable g ν

Tactic:
contrapose! h
-- 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 μ
𝕜 : Type u_5
inst_6 : RCLike 𝕜
inst_7 : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : CompleteSpace E
h : Integrable f μ ∧ Integrable g ν
⊢ Integrable (ε := E) (fun (z : α × β) ↦ f z.1 • g z.2) (μ.prod ν)

Tactic:
h.1.smul_prod h.2

Premises used: And.right, And.left, 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 : NormedSpace ℝ E
inst_5 : SFinite μ
𝕜 : Type u_5
inst_6 : RCLike 𝕜
inst_7 : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : CompleteSpace E
h : Integrable f μ ∧ Integrable g ν
⊢ Integrable (ε := E) (fun (z : α × β) ↦ f z.1 • g z.2) (μ.prod ν)

Tactic:
exact h.1.smul_prod h.2

Premises used: And.right, And.left, 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 : NormedSpace ℝ E
inst_5 : SFinite μ
𝕜 : Type u_5
inst_6 : RCLike 𝕜
inst_7 : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : CompleteSpace E
h : ¬Integrable (ε := E) (fun (z : α × β) ↦ f z.1 • g z.2) (μ.prod ν)
⊢ ¬Integrable f μ ∨ ¬Integrable g ν

Tactic:
have H : ¬Integrable f μ ∨ ¬Integrable g ν := by
    contrapose! h
    exact h.1.smul_prod h.2
-- 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 μ
𝕜 : Type u_5
inst_6 : RCLike 𝕜
inst_7 : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : CompleteSpace E
h : ¬Integrable (ε := E) (fun (z : α × β) ↦ f z.1 • g z.2) (μ.prod ν)
H : ¬Integrable f μ ∨ ¬Integrable g ν
neg :
  ∀ (H : ¬Integrable f μ),
    ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν =
      HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)
neg₁ :
  ∀ (H : ¬Integrable g ν),
    ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν =
      HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν =
    HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)

Tactic:
rcases H with H | H
-- 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 μ
𝕜 : Type u_5
inst_6 : RCLike 𝕜
inst_7 : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : CompleteSpace E
h : ¬Integrable (ε := E) (fun (z : α × β) ↦ f z.1 • g z.2) (μ.prod ν)
H : ¬Integrable f μ
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν =
    HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)

Tactic:
simp [integral_undef h, integral_undef H]

Premises used: MeasureTheory.integral_undef