awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (hypothesis)
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
⊢ 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 ∂μ)
have h_int₁ : @Integrable _ _ _ _ Prod.instMeasurableSpace (uncurry f) (Measure.prod (Measure.restrict volume (Ioc b a)) μ)
Tactic: simp only [hab, Set.uIoc_of_ge] at h_int
Cleared hypotheses: h_int
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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)) μ)
⊢ 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 ∂μ)
have 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 ∂μ)
Tactic: rw [integral_integral_swap h_int, integral_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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 ∂μ)
⊢ 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 ∂μ)
have 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 ∂μ)
Tactic: rw [integral_integral_swap h_int, integral_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : 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 ν)
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν) (∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂ν ∂μ)
have 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) ∂ν ∂μ)
Tactic: simp only [← Measure.prod_restrict s t, IntegrableOn] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (hypothesis)
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 ν
⊢ 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)
have this : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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)
    (∫ (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)
have 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)
Tactic: simp_rw [integral_prod _ this, ContinuousLinearMap.integral_comp_comm _ hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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)
    (∫ (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)
have 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)
Tactic: change ∫ x, B.flip (∫ y, g y ∂ν) (f x) ∂μ = _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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)
    (∫ (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)
have 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)
Tactic: rw [ContinuousLinearMap.integral_comp_comm _ hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : 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
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν =
    HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)
have 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 ∂ν)
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : 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 ∂ν)
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν =
    HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)
have 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 ∂ν)
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : 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 ∂ν)
have 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 ∂ν)
Tactic: by_cases h : Integrable (fun z : α × β => f z.1 • g z.2) (μ.prod ν)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : 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 ∂ν)
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν =
    HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)
have 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 ∂ν)
Tactic: by_cases h : Integrable (fun z : α × β => f z.1 • g z.2) (μ.prod ν)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : 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 ν)
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν =
    HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)
have 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 ∂ν)
Tactic: rw [integral_prod _ h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : 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 ν)
⊢ ∫ (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 ∂ν)
have pos : ∫ (x : α), ∫ (y : β), f x • g y ∂ν ∂μ =
  HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)
Tactic: simp_rw [integral_smul, integral_smul_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : 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 ∂ν)
⊢ ∫ (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 ∂ν)
have 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 ∂ν)
Tactic: simp_rw [integral_smul, integral_smul_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : 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 ν
have contrapose! : ∀ (h : Integrable f μ ∧ Integrable g ν), Integrable (ε := E) (fun (z : α × β) ↦ f z.1 • g z.2) (μ.prod ν)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : 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 ν)
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν =
    HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)
have H : ¬Integrable f μ ∨ ¬Integrable g ν
Tactic: have H : ¬Integrable f μ ∨ ¬Integrable g ν := by
    contrapose! h
    exact h.1.smul_prod h.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : 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 ν
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν =
    HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)
have 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 ∂ν)
Tactic: rcases H with H | H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : 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 ∂ν)
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν =
    HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)
have 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 ∂ν)
Tactic: rcases H with H | H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
L : Type u_5
inst_4 : RCLike L
f : α → L
g : β → L
s : Set α
t : Set β
⊢ ∫ (z : α × β) in s ×ˢ t, f z.1 * g z.2 ∂μ.prod ν =
    HMul.hMul (α := L) (∫ (x : α) in s, f x ∂μ) (∫ (y : β) in t, g y ∂ν)
have rw : ∫ (z : α × β), f z.1 * g z.2 ∂(μ.restrict s).prod (ν.restrict t) =
  HMul.hMul (α := L) (∫ (x : α) in s, f x ∂μ) (∫ (y : β) in t, g y ∂ν)
Tactic: rw [← Measure.prod_restrict s t]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
inst_4 : NormedSpace ℝ E
inst_5 : SFinite μ
f : α → E
⊢ ∫ (z : α × β), f z.1 ∂μ.prod ν = HSMul.hSMul (β := E) (ν.real univ) (∫ (x : α), f x ∂μ)
have rw : ∫ (z : β × α), f z.swap.1 ∂ν.prod μ = HSMul.hSMul (β := E) (ν.real univ) (∫ (x : α), f x ∂μ)
Tactic: rw [← integral_prod_swap]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : Measure E
inst_6 : IsProbabilityMeasure μ
ν : Measure F
inst_7 : IsProbabilityMeasure ν
L : E × F →L[ℝ] G
hLμ : Integrable.{u_7, u_5} (ε := G) (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → G) μ
hLν : Integrable.{u_7, u_6} (ε := G) (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → G) ν
⊢ Integrable (ε := G) (fun (v : E × F) ↦ (L : (a : E × F) → G) v) (μ.prod ν)
have simp_rw : Integrable (ε := G)
  (fun (v : E × F) ↦
    HAdd.hAdd (α := G) (β := G) ((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → G) v.1 : G)
      ((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → G) v.2 : G))
  (μ.prod ν)
Tactic: simp_rw [← L.comp_inl_add_comp_inr]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : Measure E
inst_6 : IsProbabilityMeasure μ
ν : Measure F
inst_7 : IsProbabilityMeasure ν
L : E × F →L[ℝ] G
inst_8 : CompleteSpace G
hLμ : Integrable.{u_7, u_5} (ε := G) (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → G) μ
hLν : Integrable.{u_7, u_6} (ε := G) (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → G) ν
⊢ ∫ (p : E × F), (L : (a : E × F) → G) p ∂μ.prod ν =
    HAdd.hAdd (α := G) (∫ (x : E), (L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → G) x ∂μ)
      (∫ (y : F), (L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → G) y ∂ν)
have simp_rw : ∫ (p : E × F),
    HAdd.hAdd (α := G) (β := G) ((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → G) p.1 : G)
      ((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → G) p.2 : G) ∂μ.prod ν =
  HAdd.hAdd (α := G) (∫ (x : E), (L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → G) x ∂μ)
    (∫ (y : F), (L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → G) y ∂ν)
Tactic: simp_rw [← L.comp_inl_add_comp_inr]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (hypothesis)
Goal:
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : Measure E
inst_6 : IsProbabilityMeasure μ
ν : Measure F
inst_7 : IsProbabilityMeasure ν
L : E × F →L[ℝ] G
inst_8 : CompleteSpace G
hLμ : Integrable.{u_7, u_5} (ε := G) (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → G) μ
hLν : Integrable.{u_7, u_6} (ε := G) (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → G) ν
⊢ ∫ (p : E × F),
      HAdd.hAdd (α := G) (β := G) ((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → G) p.1 : G)
        ((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → G) p.2 : G) ∂μ.prod ν =
    HAdd.hAdd (α := G) (∫ (x : E), (L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → G) x ∂μ)
      (∫ (y : F), (L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → G) y ∂ν)
have hLμ₁ : Integrable (ε := G) (fun (x : E × F) ↦ (L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → G) x.1) (μ.prod ν)
Tactic: replace hLμ := ((memLp_one_iff_integrable.mpr hLμ).comp_fst ν).integrable le_rfl
Cleared hypotheses: hLμ