awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_6} (ε := G) (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → G) ν
hLμ : Integrable (ε := G) (fun (x : E × F) ↦ (L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → G) x.1) (μ.prod ν)
⊢ ∫ (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.inr ℝ E F : (a : F) → G) x.2) (μ.prod ν)
Tactic: replace hLν := ((memLp_one_iff_integrable.mpr hLν).comp_snd μ).integrable le_rfl
Cleared hypotheses: hLν
-- 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 (ε := G) (fun (x : E × F) ↦ (L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → G) x.1) (μ.prod ν)
hLν : Integrable (ε := G) (fun (x : E × F) ↦ (L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → G) x.2) (μ.prod ν)
⊢ ∫ (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 rw : HAdd.hAdd (α := G) (∫ (x : E), ∫ (y : F), (L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → G) (x, y).1 ∂ν ∂μ)
    (∫ (x : E), ∫ (y : F), (L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → G) (x, y).2 ∂ν ∂μ) =
  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: rw [integral_add hLμ hLν, integral_prod _ hLμ, integral_prod _ hLν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ) (∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν)
have this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: have : Fact (μ U < ∞) := ⟨(IsCompact.image h'f continuous_fst).measure_lt_top⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ) (∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν)
have this₁ : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: have : Fact (ν V < ∞) := ⟨(IsCompact.image h'f continuous_snd).measure_lt_top⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ) (∫ (x : X), ∫ (y : Y) in V, f x y ∂ν ∂μ)
have e_f : ∀ (x : X), Eq.{u_3 + 1} (α := E) (∫ (y : Y), f x y ∂ν) (∫ (y : Y) in V, f x y ∂ν)
Tactic: congr 1 with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
x : X
⊢ Eq.{u_3 + 1} (α := E) (∫ (y : Y), f x y ∂ν) (∫ (y : Y) in V, f x y ∂ν)
have apply : ∀ (y : Y) (hy : y ∉ V), f x y = 0
Tactic: apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
x : X
y : Y
hy : y ∉ V
⊢ f x y = 0
have contrapose! : ∀ (hy : f x y ≠ 0), y ∈ V
Tactic: contrapose! hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
x : X
y : Y
hy : f x y ≠ 0
⊢ y ∈ V
have this₁ : (x, y) ∈ support (uncurry f)
Tactic: have : (x, y) ∈ Function.support f.uncurry := hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), ∫ (y : Y) in V, f x y ∂ν ∂μ) (∫ (x : X) in U, ∫ (y : Y) in V, f x y ∂ν ∂μ)
have apply : ∀ (x : X) (hx : x ∉ U), Eq.{u_3 + 1} (α := E) (∫ (y : Y) in V, f x y ∂ν) 0
Tactic: apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
x : X
hx : x ∉ U
y : Y
⊢ f x y = 0
have contrapose! : ∀ (hx : f x y ≠ 0), x ∈ U
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
x : X
y : Y
hx : f x y ≠ 0
⊢ x ∈ U
have this₁ : (x, y) ∈ support (uncurry f)
Tactic: have : (x, y) ∈ Function.support f.uncurry := hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
x : X
hx : x ∉ U
⊢ Eq.{u_3 + 1} (α := E) (∫ (y : Y) in V, f x y ∂ν) 0
have this₁ : ∀ (y : Y), f x y = 0
Tactic: have : ∀ y, f x y = 0 := by
      intro y
      contrapose! hx
      have : (x, y) ∈ Function.support f.uncurry := hx
      exact mem_image_of_mem _ (subset_tsupport _ this)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in U, ∫ (y : Y) in V, f x y ∂ν ∂μ) (∫ (y : Y) in V, ∫ (x : X) in U, f x y ∂μ ∂ν)
have hf₁ : Integrable (uncurry f) ((μ.restrict U).prod (ν.restrict V))
Tactic: apply integral_integral_swap
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ Integrable (uncurry f) ((μ.restrict U).prod (ν.restrict V))
have hf₁ : IntegrableOn (uncurry f) (tsupport (uncurry f)) ((μ.restrict U).prod (ν.restrict V))
Tactic: apply (integrableOn_iff_integrable_of_support_subset (subset_tsupport f.uncurry)).mp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ IntegrableOn (uncurry f) (tsupport (uncurry f)) ((μ.restrict U).prod (ν.restrict V))
have hf₁ : HasFiniteIntegral (uncurry f) (((μ.restrict U).prod (ν.restrict V)).restrict (tsupport (uncurry f)))
Tactic: refine ⟨(h'f.stronglyMeasurable_of_prod hf).aestronglyMeasurable, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ HasFiniteIntegral (uncurry f) (((μ.restrict U).prod (ν.restrict V)).restrict (tsupport (uncurry f)))
have hf₁ : ∀ (C : ℝ) (hC : ∀ (p : X × Y), ‖uncurry f p‖ ≤ C),
  HasFiniteIntegral (uncurry f) (((μ.restrict U).prod (ν.restrict V)).restrict (tsupport (uncurry f)))
Tactic: obtain ⟨C, hC⟩ : ∃ C, ∀ p, ‖f.uncurry p‖ ≤ C := hf.bounded_above_of_compact_support h'f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ Eq.{u_3 + 1} (α := E) (∫ (y : Y) in V, ∫ (x : X) in U, f x y ∂μ ∂ν) (∫ (y : Y), ∫ (x : X) in U, f x y ∂μ ∂ν)
have apply : ∀ (y : Y) (hy : y ∉ V), Eq.{u_3 + 1} (α := E) (∫ (x : X) in U, f x y ∂μ) 0
Tactic: apply setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
y : Y
hy : y ∉ V
x : X
⊢ f x y = 0
have contrapose! : ∀ (hy : f x y ≠ 0), y ∈ V
Tactic: contrapose! hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
y : Y
x : X
hy : f x y ≠ 0
⊢ y ∈ V
have this₁ : (x, y) ∈ support (uncurry f)
Tactic: have : (x, y) ∈ Function.support f.uncurry := hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
y : Y
hy : y ∉ V
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in U, f x y ∂μ) 0
have this₁ : ∀ (x : X), f x y = 0
Tactic: have : ∀ x, f x y = 0 := by
      intro x
      contrapose! hy
      have : (x, y) ∈ Function.support f.uncurry := hy
      exact mem_image_of_mem _ (subset_tsupport _ this)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ Eq.{u_3 + 1} (α := E) (∫ (y : Y), ∫ (x : X) in U, f x y ∂μ ∂ν) (∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν)
have e_f : ∀ (y : Y), Eq.{u_3 + 1} (α := E) (∫ (x : X) in U, f x y ∂μ) (∫ (x : X), f x y ∂μ)
Tactic: congr 1 with y
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
y : Y
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in U, f x y ∂μ) (∫ (x : X), f x y ∂μ)
have apply : ∀ (x : X) (hx : x ∉ U), f x y = 0
Tactic: apply setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)