awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 μ
g : ↥(Lp E 1 (μ.prod ν))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (i : ↥(Lp E 1 (μ.prod ν))) ↦
      ∫⁻ (x : α),
        ∫⁻ (y : β),
          ‖(↑(↑i : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y) -
              (↑(↑g : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y)‖ₑ ∂ν ∂μ)
    (𝓝 g) (𝓝 0)
have this : ∀ (i : ↥(Lp E 1 (μ.prod ν))),
  Measurable (β := ℝ≥0∞) fun (z : α × β) ↦
    ‖(↑(↑i : α × β →ₘ[μ.prod ν] E) : α × β → E) z - (↑(↑g : α × β →ₘ[μ.prod ν] E) : α × β → E) z‖ₑ
Tactic: have this (i : α × β →₁[μ.prod ν] E) : Measurable fun z => ‖i z - g z‖ₑ :=
    ((Lp.stronglyMeasurable i).sub (Lp.stronglyMeasurable g)).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 μ
g : ↥(Lp E 1 (μ.prod ν))
this :
  ∀ (i : ↥(Lp E 1 (μ.prod ν))),
    Measurable (β := ℝ≥0∞) fun (z : α × β) ↦
      ‖(↑(↑i : α × β →ₘ[μ.prod ν] E) : α × β → E) z - (↑(↑g : α × β →ₘ[μ.prod ν] E) : α × β → E) z‖ₑ
⊢ Tendsto (β := ℝ≥0∞)
    (fun (i : ↥(Lp E 1 (μ.prod ν))) ↦
      ∫⁻ (x : α),
        ∫⁻ (y : β),
          ‖(↑(↑i : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y) -
              (↑(↑g : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y)‖ₑ ∂ν ∂μ)
    (𝓝 g) (𝓝 0)
have simp_rw : Tendsto (fun (i : ↥(Lp E 1 (μ.prod ν))) ↦ ENNReal.ofReal ‖i - g‖) (𝓝 g) (𝓝 (ENNReal.ofReal 0))
Tactic: simp_rw [← lintegral_prod _ (this _).aemeasurable, ← L1.ofReal_norm_sub_eq_lintegral,
    ← ofReal_zero]
-- 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 ν))
this :
  ∀ (i : ↥(Lp E 1 (μ.prod ν))),
    Measurable (β := ℝ≥0∞) fun (z : α × β) ↦
      ‖(↑(↑i : α × β →ₘ[μ.prod ν] E) : α × β → E) z - (↑(↑g : α × β →ₘ[μ.prod ν] E) : α × β → E) z‖ₑ
⊢ Tendsto (fun (i : ↥(Lp E 1 (μ.prod ν))) ↦ ENNReal.ofReal ‖i - g‖) (𝓝 g) (𝓝 (ENNReal.ofReal 0))
have refine : Tendsto (β := ℝ) (fun (i : ↥(Lp E 1 (μ.prod ν))) ↦ ‖i - g‖) (𝓝 g) (𝓝 0)
Tactic: refine (continuous_ofReal.tendsto 0).comp ?_
-- 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 ν))
this :
  ∀ (i : ↥(Lp E 1 (μ.prod ν))),
    Measurable (β := ℝ≥0∞) fun (z : α × β) ↦
      ‖(↑(↑i : α × β →ₘ[μ.prod ν] E) : α × β → E) z - (↑(↑g : α × β →ₘ[μ.prod ν] E) : α × β → E) z‖ₑ
⊢ Tendsto (β := ℝ) (fun (i : ↥(Lp E 1 (μ.prod ν))) ↦ ‖i - g‖) (𝓝 g) (𝓝 0)
have rw : Tendsto (fun (i : ↥(Lp E 1 (μ.prod ν))) ↦ i) (𝓝 g) (𝓝 g)
Tactic: rw [← tendsto_iff_norm_sub_tendsto_zero]
-- 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
hf : Integrable f (μ.prod ν)
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ)
have pos : ∀ (hE : CompleteSpace E), Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, 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 μ
f : α × β → E
hf : Integrable f (μ.prod ν)
pos :
  ∀ (hE : CompleteSpace E), Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ)
have neg : ∀ (hE : ¬CompleteSpace E), Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, 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 μ
hE : CompleteSpace E
⊢ ∀ (f : α × β → E) (hf : Integrable f (μ.prod ν)),
    Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ)
have pos : ∀ (c : E) ⦃s : Set (α × β)⦄,
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      Eq.{u_3 + 1} (α := E) (∫ (z : α × β), s.indicator (fun (x : α × β) ↦ c) z ∂μ.prod ν)
        (∫ (x : α), ∫ (y : β), s.indicator (fun (x : α × β) ↦ c) (x, y) ∂ν ∂μ)
Tactic: apply Integrable.induction
-- 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 μ
hE : CompleteSpace E
pos :
  ∀ (c : E) ⦃s : Set (α × β)⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := E) (∫ (z : α × β), s.indicator (fun (x : α × β) ↦ c) z ∂μ.prod ν)
          (∫ (x : α), ∫ (y : β), s.indicator (fun (x : α × β) ↦ c) (x, y) ∂ν ∂μ)
⊢ ∀ (f : α × β → E) (hf : Integrable f (μ.prod ν)),
    Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ)
have pos₁ : ∀ ⦃f g : α × β → E⦄,
  Disjoint (support f) (support g) →
    Integrable f (μ.prod ν) →
      Integrable g (μ.prod ν) →
        Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ) →
          Eq.{u_3 + 1} (α := E) (∫ (z : α × β), g z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ) →
            Eq.{u_3 + 1} (α := E) (∫ (z : α × β), (f + g) z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), (f + g) (x, y) ∂ν ∂μ)
Tactic: apply Integrable.induction
-- 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 μ
hE : CompleteSpace E
pos :
  ∀ (c : E) ⦃s : Set (α × β)⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := E) (∫ (z : α × β), s.indicator (fun (x : α × β) ↦ c) z ∂μ.prod ν)
          (∫ (x : α), ∫ (y : β), s.indicator (fun (x : α × β) ↦ c) (x, y) ∂ν ∂μ)
pos₁ :
  ∀ ⦃f g : α × β → E⦄,
    Disjoint (support f) (support g) →
      Integrable f (μ.prod ν) →
        Integrable g (μ.prod ν) →
          Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ) →
            Eq.{u_3 + 1} (α := E) (∫ (z : α × β), g z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ) →
              Eq.{u_3 + 1} (α := E) (∫ (z : α × β), (f + g) z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), (f + g) (x, y) ∂ν ∂μ)
⊢ ∀ (f : α × β → E) (hf : Integrable f (μ.prod ν)),
    Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ)
have pos₂ : IsClosed (X := ↥(Lp E 1 (μ.prod ν)))
  {f : ↥(Lp E 1 (μ.prod ν)) |
    Eq.{u_3 + 1} (α := E) (∫ (z : α × β), (↑(↑f : α × β →ₘ[μ.prod ν] E) : α × β → E) z ∂μ.prod ν)
      (∫ (x : α), ∫ (y : β), (↑(↑f : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y) ∂ν ∂μ)}
Tactic: apply Integrable.induction
-- 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 μ
hE : CompleteSpace E
pos :
  ∀ (c : E) ⦃s : Set (α × β)⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := E) (∫ (z : α × β), s.indicator (fun (x : α × β) ↦ c) z ∂μ.prod ν)
          (∫ (x : α), ∫ (y : β), s.indicator (fun (x : α × β) ↦ c) (x, y) ∂ν ∂μ)
pos₁ :
  ∀ ⦃f g : α × β → E⦄,
    Disjoint (support f) (support g) →
      Integrable f (μ.prod ν) →
        Integrable g (μ.prod ν) →
          Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ) →
            Eq.{u_3 + 1} (α := E) (∫ (z : α × β), g z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ) →
              Eq.{u_3 + 1} (α := E) (∫ (z : α × β), (f + g) z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), (f + g) (x, y) ∂ν ∂μ)
pos₂ :
  IsClosed (X := ↥(Lp E 1 (μ.prod ν)))
    {f : ↥(Lp E 1 (μ.prod ν)) |
      Eq.{u_3 + 1} (α := E) (∫ (z : α × β), (↑(↑f : α × β →ₘ[μ.prod ν] E) : α × β → E) z ∂μ.prod ν)
        (∫ (x : α), ∫ (y : β), (↑(↑f : α × β →ₘ[μ.prod ν] E) : α × β → E) (x, y) ∂ν ∂μ)}
⊢ ∀ (f : α × β → E) (hf : Integrable f (μ.prod ν)),
    Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ)
have pos₃ : ∀ ⦃f g : α × β → E⦄,
  f =ᶠ[ae (μ.prod ν)] g →
    Integrable f (μ.prod ν) →
      Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ) →
        Eq.{u_3 + 1} (α := E) (∫ (z : α × β), g z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ)
Tactic: apply Integrable.induction
-- 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 μ
hE : CompleteSpace E
c : E
s : Set (α × β)
hs : MeasurableSet s
h2s : LT.lt (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : α × β), s.indicator (fun (x : α × β) ↦ c) z ∂μ.prod ν)
    (∫ (x : α), ∫ (y : β), s.indicator (fun (x : α × β) ↦ c) (x, y) ∂ν ∂μ)
have pos : ENNReal.toReal ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s) • c =
  (∫⁻ (a : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ).toReal • c
Tactic: simp_rw [integral_indicator hs, ← indicator_comp_right, Function.comp_def,
      integral_indicator (measurable_prodMk_left hs), setIntegral_const, integral_smul_const,
      measureReal_def,
      integral_toReal (measurable_measure_prodMk_left hs).aemeasurable
        (ae_measure_lt_top hs h2s.ne)]
-- 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 μ
hE : CompleteSpace E
c : E
s : Set (α × β)
hs : MeasurableSet s
h2s : LT.lt (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.toReal ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s) • c =
    (∫⁻ (a : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ).toReal • c
have pos : (∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ).toReal • c =
  (∫⁻ (a : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ).toReal • c
Tactic: rw [Measure.prod_apply hs]
-- 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 μ
hE : CompleteSpace E
f g : α × β → E
i_f : Integrable f (μ.prod ν)
i_g : Integrable g (μ.prod ν)
hf : Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ)
hg : Eq.{u_3 + 1} (α := E) (∫ (z : α × β), g z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : α × β), (f + g) z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), (f + g) (x, y) ∂ν ∂μ)
have pos : HAdd.hAdd (α := E) (∫ (a : α × β), f a ∂μ.prod ν) (∫ (a : α × β), g a ∂μ.prod ν) =
  ∫ (x : α), ∫ (y : β), (f + g) (x, y) ∂ν ∂μ
Tactic: simp_rw [integral_add' i_f i_g, integral_integral_add' i_f i_g, hf, hg]
-- 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 μ
hE : CompleteSpace E
f g : α × β → E
i_f : Integrable f (μ.prod ν)
i_g : Integrable g (μ.prod ν)
hf : Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ)
hg : Eq.{u_3 + 1} (α := E) (∫ (z : α × β), g z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ)
pos :
  HAdd.hAdd (α := E) (∫ (a : α × β), f a ∂μ.prod ν) (∫ (a : α × β), g a ∂μ.prod ν) =
    ∫ (x : α), ∫ (y : β), (f + g) (x, y) ∂ν ∂μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : α × β), (f + g) z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), (f + g) (x, y) ∂ν ∂μ)
have pos₁ : HAdd.hAdd (α := E) (∫ (a : α × β), f a ∂μ.prod ν) (∫ (a : α × β), g a ∂μ.prod ν) =
  HAdd.hAdd (α := E) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ) (∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ)
Tactic: simp_rw [integral_add' i_f i_g, integral_integral_add' i_f i_g, hf, hg]
-- 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 μ
hE : CompleteSpace E
f g : α × β → E
i_f : Integrable f (μ.prod ν)
i_g : Integrable g (μ.prod ν)
hf : Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ)
hg : Eq.{u_3 + 1} (α := E) (∫ (z : α × β), g z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ)
pos :
  HAdd.hAdd (α := E) (∫ (a : α × β), f a ∂μ.prod ν) (∫ (a : α × β), g a ∂μ.prod ν) =
    ∫ (x : α), ∫ (y : β), (f + g) (x, y) ∂ν ∂μ
pos₁ :
  HAdd.hAdd (α := E) (∫ (a : α × β), f a ∂μ.prod ν) (∫ (a : α × β), g a ∂μ.prod ν) =
    HAdd.hAdd (α := E) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ) (∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : α × β), (f + g) z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), (f + g) (x, y) ∂ν ∂μ)
have pos₂ : HAdd.hAdd (α := E) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ) (∫ (a : α × β), g a ∂μ.prod ν) =
  HAdd.hAdd (α := E) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ) (∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ)
Tactic: simp_rw [integral_add' i_f i_g, integral_integral_add' i_f i_g, hf, hg]
-- 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 μ
hE : CompleteSpace E
f g : α × β → E
hfg : f =ᶠ[ae (μ.prod ν)] g
hf : Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : α × β), g z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ)
have h : Eq.{u_3 + 1} (α := E) (∫ (z : α × β), g z ∂μ.prod ν) (∫ (z : α × β), f z ∂μ.prod ν)
Tactic: convert! hf using 1
-- 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 μ
hE : CompleteSpace E
f g : α × β → E
hfg : f =ᶠ[ae (μ.prod ν)] g
hf : Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ)
h : Eq.{u_3 + 1} (α := E) (∫ (z : α × β), g z ∂μ.prod ν) (∫ (z : α × β), f z ∂μ.prod ν)
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : α × β), g z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ)
have h₁ : Eq.{u_3 + 1} (α := E) (∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ)
Tactic: convert! hf using 1
-- 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 μ
hE : CompleteSpace E
f g : α × β → E
hfg : f =ᶠ[ae (μ.prod ν)] g
hf : Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ)
have h : EventuallyEq.{u_1, u_3} (β := E) (ae μ) (fun (a : α) ↦ ∫ (y : β), g (a, y) ∂ν) fun (a : α) ↦ ∫ (y : β), f (a, y) ∂ν
Tactic: apply 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 μ
hE : CompleteSpace E
f g : α × β → E
hfg : f =ᶠ[ae (μ.prod ν)] g
hf : Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ)
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae μ) (fun (a : α) ↦ ∫ (y : β), g (a, y) ∂ν) fun (a : α) ↦ ∫ (y : β), f (a, y) ∂ν
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ∀ᵐ (y : β) ∂ν, f (x, y) = g (x, y)) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            (fun (x : α) ↦
                Eq.{u_3 + 1} (α := E) ((fun (a : α) ↦ (∫ (y : β), g (a, y) ∂ν : E)) x)
                  ((fun (a : α) ↦ (∫ (y : β), f (a, y) ∂ν : E)) x))
              x}
          x}
    a
Tactic: filter_upwards [ae_ae_of_ae_prod hfg] with x hfgx using integral_congr_ae (ae_eq_symm hfgx)
-- 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 μ
hE : CompleteSpace E
f g : α × β → E
hfg : f =ᶠ[ae (μ.prod ν)] g
hf : Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ)
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ∀ᵐ (y : β) ∂ν, f (x, y) = g (x, y)) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦
                  Eq.{u_3 + 1} (α := E) ((fun (a : α) ↦ (∫ (y : β), g (a, y) ∂ν : E)) x)
                    ((fun (a : α) ↦ (∫ (y : β), f (a, y) ∂ν : E)) x))
                x}
            x}
      a
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae μ) (fun (a : α) ↦ ∫ (y : β), g (a, y) ∂ν) fun (a : α) ↦ ∫ (y : β), f (a, y) ∂ν
have h₁ : ∀ (a : α),
  (∀ᵐ (y : β) ∂ν, f (a, y) = g (a, y)) → Eq.{u_3 + 1} (α := E) (∫ (y : β), g (a, y) ∂ν) (∫ (y : β), f (a, y) ∂ν)
Tactic: filter_upwards [ae_ae_of_ae_prod hfg] with x hfgx using integral_congr_ae (ae_eq_symm hfgx)
-- 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
hf : Integrable f (μ.prod ν)
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν)
have rw : Eq.{u_3 + 1} (α := E) (∫ (z : β × α), f z.swap ∂ν.prod μ) (∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν)
Tactic: rw [← integral_prod_swap f]
-- 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
h_int : @Integrable _ _ _ _ Prod.instMeasurableSpace (uncurry f) (Measure.prod (Measure.restrict volume (uIoc a b)) μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : ℝ) in a..b, ∫ (y : α), f x y ∂μ) (∫ (y : α), ∫ (x : ℝ) in a..b, f x y ∂μ)
have 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 ∂μ)
Tactic: rcases le_total a b with (hab | hab)
-- 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
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 ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : ℝ) in a..b, ∫ (y : α), f x y ∂μ) (∫ (y : α), ∫ (x : ℝ) in a..b, f x y ∂μ)
have 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 ∂μ)
Tactic: rcases le_total a b with (hab | hab)
-- 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
h_int : @Integrable _ _ _ _ Prod.instMeasurableSpace (uncurry f) (Measure.prod (Measure.restrict volume (uIoc a b)) μ)
hab : a ≤ b
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : ℝ) in a..b, ∫ (y : α), f x y ∂μ) (∫ (y : α), ∫ (x : ℝ) in a..b, f x y ∂μ)
have 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 ∂μ)
Tactic: simp_rw [intervalIntegral.integral_of_le hab]
-- 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 : 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 ∂μ)
have h_int₁ : @Integrable _ _ _ _ Prod.instMeasurableSpace (uncurry f) (Measure.prod (Measure.restrict volume (Ioc a b)) μ)
Tactic: simp only [hab, Set.uIoc_of_le] 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
h_int : @Integrable _ _ _ _ Prod.instMeasurableSpace (uncurry f) (Measure.prod (Measure.restrict volume (uIoc a b)) μ)
hab : b ≤ a
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : ℝ) in a..b, ∫ (y : α), f x y ∂μ) (∫ (y : α), ∫ (x : ℝ) in a..b, f x y ∂μ)
have 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 ∂μ)
Tactic: simp_rw [intervalIntegral.integral_of_ge hab]