awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)‖ₑ ≤ ENNReal.ofReal C * ‖f z.1‖ₑ * ‖g z.2‖ₑ
have hfg : ‖op (f z.1) (g z.2)‖ ≤ (↑C.toNNReal : ℝ) * ‖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]
-- 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
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‖
have hfg : C * ‖f z.1‖ * ‖g z.2‖ ≤ (↑C.toNNReal : ℝ) * ‖f z.1‖ * ‖g z.2‖
Tactic: refine (hC _ _).trans ?_
-- 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
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 * ‖f z.1‖ * ‖g z.2‖ ≤ (↑C.toNNReal : ℝ) * ‖f z.1‖ * ‖g z.2‖
have hfg : C ≤ (↑C.toNNReal : ℝ)
Tactic: gcongr
-- 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
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‖
⊢ HasFiniteIntegral (ε := G) (fun (z : α × β) ↦ op (f z.1) (g z.2)) (μ.prod ν)
have ν₁ : ∫⁻ (z : α × β), ‖op (f z.1) (g z.2)‖ₑ ∂μ.prod ν ≤ ∫⁻ (z : α × β), ENNReal.ofReal C * ‖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]
-- 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
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 ν
⊢ HasFiniteIntegral (ε := G) (fun (z : α × β) ↦ op (f z.1) (g z.2)) (μ.prod ν)
have ν₂ : ∫⁻ (x : α), ∫⁻ (y : β), ENNReal.ofReal C * ‖f x‖ₑ * ‖g y‖ₑ ∂ν ∂μ ≤
  (ENNReal.ofReal C * ∫⁻ (x : α), ‖f x‖ₑ ∂μ) * ∫⁻ (y : β), ‖g y‖ₑ ∂ν
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]
-- 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
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‖ₑ ∂ν
⊢ HasFiniteIntegral (ε := G) (fun (z : α × β) ↦ op (f z.1) (g z.2)) (μ.prod ν)
have ν₃ : (ENNReal.ofReal C * ∫⁻ (x : α), ‖f x‖ₑ ∂μ) * ∫⁻ (y : β), ‖g y‖ₑ ∂ν < ∞
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]
-- 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 α
inst_2 : NormedAddCommGroup E
f : α → E
hf : Integrable f μ
ν : Measure β
inst_3 : IsFiniteMeasure ν
⊢ Integrable (ε := E) (fun (x : α × β) ↦ f x.1) (μ.prod ν)
have rw : ∀ (hf : MemLp f 1 μ) (ν : Measure β) [IsFiniteMeasure ν], MemLp (ε := E) (fun (x : α × β) ↦ f x.1) 1 (μ.prod ν)
Tactic: rw [← memLp_one_iff_integrable] at hf ⊢
Cleared hypotheses: hf, ν, inst_3
-- 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 β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : β → E
hf : Integrable f ν
μ : Measure α
inst_4 : IsFiniteMeasure μ
⊢ Integrable (ε := E) (fun (x : α × β) ↦ f x.2) (μ.prod ν)
have rw : ∀ (hf : MemLp f 1 ν) (μ : Measure α) [IsFiniteMeasure μ], MemLp (ε := E) (fun (x : α × β) ↦ f x.2) 1 (μ.prod ν)
Tactic: rw [← memLp_one_iff_integrable] at hf ⊢
Cleared hypotheses: hf, μ, inst_4
-- 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 : SFinite μ
f : α × β → E
s : Set α
t : Set β
hf : IntegrableOn f (s ×ˢ t) (μ.prod ν)
⊢ IntegrableOn (f ∘ Prod.swap) (t ×ˢ s) (ν.prod μ)
have rw : ∀ (hf : Integrable f ((μ.restrict s).prod (ν.restrict t))),
  Integrable (f ∘ Prod.swap) ((ν.restrict t).prod (μ.restrict s))
Tactic: rw [IntegrableOn, ← Measure.prod_restrict] at hf ⊢
Cleared hypotheses: hf
-- 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 ν
f : β → E
hf : Integrable (ε := E) (fun (x : α × β) ↦ f x.2) (μ.prod ν)
hμ : μ ≠ 0
⊢ Integrable f ν
have hf_meas : AEStronglyMeasurable (β := E) (fun (x : α × β) ↦ f x.2) (μ.prod ν)
Tactic: rcases hf with ⟨hf_meas, hf_fin⟩
Cleared hypotheses: hf
-- 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 ν
f : β → E
hf : Integrable (ε := E) (fun (x : α × β) ↦ f x.2) (μ.prod ν)
hμ : μ ≠ 0
hf_meas : AEStronglyMeasurable (β := E) (fun (x : α × β) ↦ f x.2) (μ.prod ν)
⊢ Integrable f ν
have hf_fin : HasFiniteIntegral (ε := E) (fun (x : α × β) ↦ f x.2) (μ.prod ν)
Tactic: rcases hf with ⟨hf_meas, hf_fin⟩
Cleared hypotheses: 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 ν
f : β → E
hμ : μ ≠ 0
hf_meas : AEStronglyMeasurable (β := E) (fun (x : α × β) ↦ f x.2) (μ.prod ν)
hf_fin : HasFiniteIntegral (ε := E) (fun (x : α × β) ↦ f x.2) (μ.prod ν)
⊢ Integrable f ν
have right : HasFiniteIntegral f ν
Tactic: use hf_meas.of_comp_snd 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 ν
f : β → E
hμ : μ ≠ 0
hf_meas : AEStronglyMeasurable (β := E) (fun (x : α × β) ↦ f x.2) (μ.prod ν)
hf_fin : HasFiniteIntegral (ε := E) (fun (x : α × β) ↦ f x.2) (μ.prod ν)
⊢ HasFiniteIntegral f ν
have this : AEMeasurable (β := ℝ≥0∞) (fun (x : α × β) ↦ ‖f x.2‖ₑ) (μ.prod ν)
Tactic: have := hf_meas.enorm
-- 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 μ
s : Set α
t : Set β
f : α × β → E
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : β × α) in t ×ˢ s, f z.swap ∂ν.prod μ) (∫ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν)
have rw : Eq.{u_3 + 1} (α := E) (∫ (z : β × α), f z.swap ∂(ν.restrict t).prod (μ.restrict s))
  (∫ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν)
Tactic: rw [← Measure.prod_restrict, ← Measure.prod_restrict, integral_prod_swap]
-- 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 μ
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 ν)
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : β × α) in t ×ˢ s, f z.swap ∂ν.prod μ) (∫ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν)
have rw₁ : Eq.{u_3 + 1} (α := E) (∫ (z : β × α), f z.swap ∂(ν.restrict t).prod (μ.restrict s))
  (∫ (z : α × β), f z ∂(μ.restrict s).prod (ν.restrict t))
Tactic: rw [← Measure.prod_restrict, ← Measure.prod_restrict, integral_prod_swap]
-- 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 μ
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))
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : β × α) in t ×ˢ s, f z.swap ∂ν.prod μ) (∫ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν)
have rw₂ : Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂(μ.restrict s).prod (ν.restrict t))
  (∫ (z : α × β), f z ∂(μ.restrict s).prod (ν.restrict t))
Tactic: rw [← Measure.prod_restrict, ← Measure.prod_restrict, integral_prod_swap]
-- 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 μ
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) ∂ν)) ∂μ)
have 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) ∂ν))
Tactic: refine integral_congr_ae ?_
-- 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 μ
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 ν)
⊢ 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) ∂ν))
have 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) ∂ν))
Tactic: filter_upwards [hf.prod_right_ae, hg.prod_right_ae] with _ h2f h2g
-- 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 μ
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) ∂ν)) ∂μ)
have 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) ∂ν))
Tactic: refine integral_congr_ae ?_
-- 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 μ
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 ν)
⊢ 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) ∂ν))
have 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) ∂ν))
Tactic: filter_upwards [hf.prod_right_ae, hg.prod_right_ae] with _ h2f h2g
-- 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 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) ∂ν)) ∂μ
have 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) ∂ν))
Tactic: refine lintegral_congr_ae ?_
-- 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 g : α × β → E
F : E → ℝ≥0∞
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
⊢ (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) ∂ν))
have 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) ∂ν))
Tactic: filter_upwards [hf.prod_right_ae, hg.prod_right_ae] with _ h2f h2g
-- 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 μ
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 (μ.prod ν))) ↦
    ∫ (x : α), ∫ (y : β), (↑(↑f : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y) ∂ν ∂μ
have rw : ∀ (x : ↥(Lp E 1 (μ.prod ν))),
  ContinuousAt (Y := E)
    (fun (f : ↥(Lp E 1 (μ.prod ν))) ↦ ∫ (x : α), ∫ (y : β), (↑(↑f : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y) ∂ν ∂μ) x
Tactic: rw [continuous_iff_continuousAt]
-- 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 μ
g : ↥(Lp E 1 (μ.prod ν))
⊢ ContinuousAt (Y := E)
    (fun (f : ↥(Lp E 1 (μ.prod ν))) ↦ ∫ (x : α), ∫ (y : β), (↑(↑f : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y) ∂ν ∂μ) g
have 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)
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) ?_
-- 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 μ
g : ↥(Lp E 1 (μ.prod ν))
⊢ 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)
have 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)
Tactic: simp_rw [← lintegral_fn_integral_sub _ (L1.integrable_coeFn _) (L1.integrable_coeFn g)]
-- 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 μ
g : ↥(Lp E 1 (μ.prod ν))
⊢ 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)
have apply : ↥(Lp E 1 (μ.prod ν)) → ℝ≥0∞
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds _ (fun i => zero_le) _
-- 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 μ
g : ↥(Lp E 1 (μ.prod ν))
apply : ↥(Lp E 1 (μ.prod ν)) → ℝ≥0∞
⊢ 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)
have 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)
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds _ (fun i => zero_le) _
-- 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 μ
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)
⊢ 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)
have 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)‖ₑ ∂ν ∂μ
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds _ (fun i => zero_le) _