awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
inst_4 : NormedSpace ℝ E
inst_5 : SFinite μ
g : ↥(Lp E 1 (μ.prod ν))
⊢ 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:
fun i => lintegral_mono fun x => enorm_integral_le_lintegral_enorm _

Premises used: MeasureTheory.AEEqFun.cast, HSub.hSub, MeasureTheory.enorm_integral_le_lintegral_enorm, Prod.mk, MeasureTheory.lintegral_mono, Subtype.val
-- 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 μ
g : ↥(Lp E 1 (μ.prod ν))
⊢ 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:
exact fun i => lintegral_mono fun x => enorm_integral_le_lintegral_enorm _

Premises used: MeasureTheory.enorm_integral_le_lintegral_enorm, MeasureTheory.lintegral_mono
-- 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 μ
g : ↥(Lp E 1 (μ.prod ν))
⊢ ∀ (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
-- 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 μ
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‖ₑ
simp_rw : Tendsto (fun (i : ↥(Lp E 1 (μ.prod ν))) ↦ ENNReal.ofReal ‖i - g‖) (𝓝 g) (𝓝 (ENNReal.ofReal 0))
⊢ 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:
simp_rw [← lintegral_prod _ (this _).aemeasurable, ← L1.ofReal_norm_sub_eq_lintegral,
    ← ofReal_zero]

Premises used: Measurable.aemeasurable, MeasureTheory.lintegral_prod, ENNReal.ofReal_zero, MeasureTheory.L1.ofReal_norm_sub_eq_lintegral
-- 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 μ
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))

Tactic:
(continuous_ofReal.tendsto 0).comp ?_

Premises used: ENNReal.ofNNReal, ENNReal.ofReal, ENNReal.continuous_ofReal, WithTop.some, Continuous.tendsto, Filter.Tendsto.comp, OfNat.ofNat
-- 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 μ
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‖ₑ
refine : Tendsto (β := ℝ) (fun (i : ↥(Lp E 1 (μ.prod ν))) ↦ ‖i - g‖) (𝓝 g) (𝓝 0)
⊢ Tendsto (fun (i : ↥(Lp E 1 (μ.prod ν))) ↦ ENNReal.ofReal ‖i - g‖) (𝓝 g) (𝓝 (ENNReal.ofReal 0))

Tactic:
refine (continuous_ofReal.tendsto 0).comp ?_

Premises used: ENNReal.continuous_ofReal, Continuous.tendsto, Filter.Tendsto.comp, OfNat.ofNat
-- 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 μ
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‖ₑ
rw : Tendsto (fun (i : ↥(Lp E 1 (μ.prod ν))) ↦ i) (𝓝 g) (𝓝 g)
⊢ Tendsto (β := ℝ) (fun (i : ↥(Lp E 1 (μ.prod ν))) ↦ ‖i - g‖) (𝓝 g) (𝓝 0)

Tactic:
rw [← tendsto_iff_norm_sub_tendsto_zero]

Premises used: tendsto_iff_norm_sub_tendsto_zero
-- 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 μ
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)

Tactic:
tendsto_id

Premises used: Set.Mem, Filter.tendsto_id, setOf
-- 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 μ
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)

Tactic:
exact tendsto_id

Premises used: Filter.tendsto_id
-- 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
hf : Integrable f (μ.prod ν)
pos :
  ∀ (hE : CompleteSpace E), Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ)
neg :
  ∀ (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) ∂ν ∂μ)

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 μ
f : α × β → E
hf : Integrable f (μ.prod ν)
hE : ¬CompleteSpace E
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ)

Tactic:
simp only [integral, dif_neg hE]

Premises used: dif_neg, 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 μ
f : α × β → E
hf : Integrable f (μ.prod ν)
hE : CompleteSpace E
pos :
  ∀ (f : α × β → E) (hf : Integrable f (μ.prod ν)),
    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) ∂ν ∂μ)

Tactic:
revert f
-- 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 μ
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) ∂ν ∂μ)}
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) ∂ν ∂μ)
⊢ ∀ (f : α × β → E) (hf : Integrable f (μ.prod ν)),
    Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ)

Tactic:
apply Integrable.induction
-- 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 μ
hE : CompleteSpace E
c : E
s : Set (α × β)
hs : MeasurableSet s
h2s : LT.lt (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos :
  ENNReal.toReal ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s) • c =
    (∫⁻ (a : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ).toReal • c
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : α × β), s.indicator (fun (x : α × β) ↦ c) z ∂μ.prod ν)
    (∫ (x : α), ∫ (y : β), s.indicator (fun (x : α × β) ↦ c) (x, y) ∂ν ∂μ)

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)]

Premises used: MeasureTheory.integral_indicator, Measurable.aemeasurable, integral_smul_const, Set.indicator_comp_right, Function.comp_def, measurable_measure_prodMk_left, MeasureTheory.Measure.ae_measure_lt_top, MeasureTheory.measureReal_def, measurable_prodMk_left, LT.lt.ne, MeasureTheory.integral_toReal, MeasureTheory.setIntegral_const
-- 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 μ
hE : CompleteSpace E
c : E
s : Set (α × β)
hs : MeasurableSet s
h2s : LT.lt (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos pos₁ :
  (∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ).toReal • c =
    (∫⁻ (a : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ).toReal • c
⊢ ENNReal.toReal ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s) • c =
    (∫⁻ (a : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ).toReal • c

Tactic:
rw [Measure.prod_apply hs]

Premises used: MeasureTheory.Measure.prod_apply
-- 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 μ
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) ∂ν ∂μ)
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) ∂ν ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : α × β), (f + g) z ∂μ.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]

Premises used: MeasureTheory.integral_add', MeasureTheory.integral_integral_add'
-- 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 μ
hE : CompleteSpace E
⊢ 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:
isClosed_eq continuous_integral continuous_integral_integral

Premises used: MeasureTheory.continuous_integral_integral, isClosed_eq, MeasureTheory.continuous_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 μ
hE : CompleteSpace E
⊢ 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:
exact isClosed_eq continuous_integral continuous_integral_integral

Premises used: MeasureTheory.continuous_integral_integral, isClosed_eq, MeasureTheory.continuous_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 μ
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 : α × β), f z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ)

Tactic:
hf
-- 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 μ
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 ν)
h₁ : Eq.{u_3 + 1} (α := E) (∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : α × β), g z ∂μ.prod ν) (∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ)

Tactic:
convert! hf using 1
-- 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 μ
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 ν) (∫ (z : α × β), f z ∂μ.prod ν)

Tactic:
integral_congr_ae hfg.symm

Premises used: MeasureTheory.integral_congr_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
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 ν) (∫ (z : α × β), f z ∂μ.prod ν)

Tactic:
exact integral_congr_ae hfg.symm

Premises used: MeasureTheory.integral_congr_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
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 : EventuallyEq.{u_1, u_3} (β := E) (ae μ) (fun (a : α) ↦ ∫ (y : β), g (a, y) ∂ν) fun (a : α) ↦ ∫ (y : β), f (a, y) ∂ν
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ) (∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ)

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- 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 μ
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) ∂ν ∂μ)
x : α
hfgx : ∀ᵐ (y : β) ∂ν, f (x, y) = g (x, y)
⊢ Eq.{u_3 + 1} (α := E) (∫ (y : β), g (x, y) ∂ν) (∫ (y : β), f (x, y) ∂ν)

Tactic:
integral_congr_ae (ae_eq_symm hfgx)

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.ae_eq_symm
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
inst_4 : 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
h₁ h₂ :
  ∀ (x : α) (hfgx : ∀ᵐ (y : β) ∂ν, f (x, y) = g (x, y)),
    Eq.{u_3 + 1} (α := E) (∫ (y : β), g (x, y) ∂ν) (∫ (y : β), f (x, y) ∂ν)
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae μ) (fun (a : α) ↦ ∫ (y : β), g (a, y) ∂ν) fun (a : α) ↦ ∫ (y : β), f (a, y) ∂ν

Tactic:
filter_upwards [ae_ae_of_ae_prod hfg] with x hfgx using integral_congr_ae (ae_eq_symm hfgx)

Premises used: MeasureTheory.Measure.ae_ae_of_ae_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
hf : Integrable f (μ.prod ν)
rw : Eq.{u_3 + 1} (α := E) (∫ (z : β × α), f z.swap ∂ν.prod μ) (∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν)
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : α × β), f z ∂μ.prod ν) (∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν)

Tactic:
rw [← integral_prod_swap f]

Premises used: MeasureTheory.integral_prod_swap
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
inst_4 : NormedSpace ℝ E
inst_5 : SFinite μ
f : α × β → E
hf : Integrable f (μ.prod ν)
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : β × α), f z.swap ∂ν.prod μ) (∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν)

Tactic:
integral_prod _ hf.swap

Premises used: MeasureTheory.Integrable.swap, Prod.swap, 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
hf : Integrable f (μ.prod ν)
⊢ Eq.{u_3 + 1} (α := E) (∫ (z : β × α), f z.swap ∂ν.prod μ) (∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν)

Tactic:
exact integral_prod _ hf.swap

Premises used: MeasureTheory.Integrable.swap, 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
hf : Integrable (uncurry f) (μ.prod ν)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α), ∫ (y : β), f x y ∂ν ∂μ) (∫ (z : α × β), f z.1 z.2 ∂μ.prod ν)

Tactic:
(integral_prod _ hf).symm

Premises used: Eq.symm, 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
hf : Integrable (uncurry f) (μ.prod ν)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α), ∫ (y : β), f x y ∂ν ∂μ) (∫ (z : β × α), f z.2 z.1 ∂ν.prod μ)

Tactic:
(integral_prod_symm _ hf.swap).symm

Premises used: MeasureTheory.Integrable.swap, MeasureTheory.integral_prod_symm, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
inst_4 : NormedSpace ℝ E
inst_5 : SFinite μ
f : α → β → E
hf : Integrable (uncurry f) (μ.prod ν)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α), ∫ (y : β), f x y ∂ν ∂μ) (∫ (y : β), ∫ (x : α), f x y ∂μ ∂ν)

Tactic:
(integral_integral hf).trans (integral_prod_symm _ hf)

Premises used: MeasureTheory.integral_integral, MeasureTheory.integral_prod_symm, Eq.trans