awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Prod
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, y) ∈ support (uncurry f)

Tactic:
have : (x, y) ∈ Function.support f.uncurry := hx
-- Module: Mathlib.MeasureTheory.Integral.Prod
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_2 : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
x : X
y : Y
hx : f x y ≠ 0
this : (x, y) ∈ support (uncurry f)
⊢ x ∈ U

Tactic:
mem_image_of_mem _ (subset_tsupport _ this)

Premises used: Set.Mem, subset_tsupport, Set.mem_image_of_mem
-- Module: Mathlib.MeasureTheory.Integral.Prod
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_2 : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
x : X
y : Y
hx : f x y ≠ 0
this : (x, y) ∈ support (uncurry f)
⊢ x ∈ U

Tactic:
exact mem_image_of_mem _ (subset_tsupport _ this)

Premises used: subset_tsupport, Set.mem_image_of_mem
-- Module: Mathlib.MeasureTheory.Integral.Prod
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

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)
-- Module: Mathlib.MeasureTheory.Integral.Prod
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_2 : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
x : X
hx : x ∉ U
this : ∀ (y : Y), f x y = 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (y : Y) in V, f x y ∂ν) 0

Tactic:
simp [this]
-- Module: Mathlib.MeasureTheory.Integral.Prod
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∞))
hf₁ : Integrable (uncurry f) ((μ.restrict U).prod (ν.restrict V))
⊢ 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 ∂μ ∂ν)

Tactic:
apply integral_integral_swap

Premises used: MeasureTheory.integral_integral_swap
-- Module: Mathlib.MeasureTheory.Integral.Prod
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∞))
hf₁ : IntegrableOn (uncurry f) (tsupport (uncurry f)) ((μ.restrict U).prod (ν.restrict V))
⊢ Integrable (uncurry f) ((μ.restrict U).prod (ν.restrict V))

Tactic:
apply (integrableOn_iff_integrable_of_support_subset (subset_tsupport f.uncurry)).mp

Premises used: subset_tsupport, MeasureTheory.integrableOn_iff_integrable_of_support_subset, Iff.mp, Function.uncurry
-- Module: Mathlib.MeasureTheory.Integral.Prod
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))

Tactic:
⟨(h'f.stronglyMeasurable_of_prod hf).aestronglyMeasurable, ?_⟩

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.Integrable, MeasureTheory.IntegrableOn, And.intro, HasCompactSupport.stronglyMeasurable_of_prod
-- Module: Mathlib.MeasureTheory.Integral.Prod
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∞))
hf₁ : HasFiniteIntegral (uncurry f) (((μ.restrict U).prod (ν.restrict V)).restrict (tsupport (uncurry f)))
⊢ IntegrableOn (uncurry f) (tsupport (uncurry f)) ((μ.restrict U).prod (ν.restrict V))

Tactic:
refine ⟨(h'f.stronglyMeasurable_of_prod hf).aestronglyMeasurable, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.Prod
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∞))
⊢ ∃ (C : ℝ), ∀ (p : X × Y), ‖uncurry f p‖ ≤ C

Tactic:
hf.bounded_above_of_compact_support h'f

Premises used: Continuous.bounded_above_of_compact_support
-- Module: Mathlib.MeasureTheory.Integral.Prod
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∞))
hf₁ :
  ∀ (C : ℝ) (hC : ∀ (p : X × Y), ‖uncurry f p‖ ≤ C),
    HasFiniteIntegral (uncurry f) (((μ.restrict U).prod (ν.restrict V)).restrict (tsupport (uncurry f)))
⊢ 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

Premises used: Continuous.bounded_above_of_compact_support
-- Module: Mathlib.MeasureTheory.Integral.Prod
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∞))
C : ℝ
hC : ∀ (p : X × Y), ‖uncurry f p‖ ≤ C
⊢ HasFiniteIntegral (uncurry f) (((μ.restrict U).prod (ν.restrict V)).restrict (tsupport (uncurry f)))

Tactic:
.of_bounded (C := C) (.of_forall hC)

Premises used: MeasureTheory.HasFiniteIntegral.of_bounded, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Integral.Prod
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∞))
C : ℝ
hC : ∀ (p : X × Y), ‖uncurry f p‖ ≤ C
⊢ HasFiniteIntegral (uncurry f) (((μ.restrict U).prod (ν.restrict V)).restrict (tsupport (uncurry f)))

Tactic:
exact .of_bounded (C := C) (.of_forall hC)
-- Module: Mathlib.MeasureTheory.Integral.Prod
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∞))
apply : ∀ (y : Y) (hy : y ∉ V), Eq.{u_3 + 1} (α := E) (∫ (x : X) in U, f x y ∂μ) 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 ∂μ ∂ν)

Tactic:
apply setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)

Premises used: MeasureTheory.setIntegral_eq_integral_of_forall_compl_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.Prod
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
contrapose! : ∀ (hy : f x y ≠ 0), y ∈ V
⊢ f x y = 0

Tactic:
contrapose! hy
-- Module: Mathlib.MeasureTheory.Integral.Prod
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
⊢ (x, y) ∈ support (uncurry f)

Tactic:
have : (x, y) ∈ Function.support f.uncurry := hy
-- Module: Mathlib.MeasureTheory.Integral.Prod
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_2 : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
y : Y
x : X
hy : f x y ≠ 0
this : (x, y) ∈ support (uncurry f)
⊢ y ∈ V

Tactic:
mem_image_of_mem _ (subset_tsupport _ this)

Premises used: Set.Mem, subset_tsupport, Set.mem_image_of_mem
-- Module: Mathlib.MeasureTheory.Integral.Prod
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_2 : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
y : Y
x : X
hy : f x y ≠ 0
this : (x, y) ∈ support (uncurry f)
⊢ y ∈ V

Tactic:
exact mem_image_of_mem _ (subset_tsupport _ this)

Premises used: subset_tsupport, Set.mem_image_of_mem
-- Module: Mathlib.MeasureTheory.Integral.Prod
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

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)
-- Module: Mathlib.MeasureTheory.Integral.Prod
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_2 : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
y : Y
hy : y ∉ V
this : ∀ (x : X), f x y = 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in U, f x y ∂μ) 0

Tactic:
simp [this]
-- Module: Mathlib.MeasureTheory.Integral.Prod
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∞))
e_f : ∀ (y : Y), Eq.{u_3 + 1} (α := E) (∫ (x : X) in U, f x y ∂μ) (∫ (x : X), f x y ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (y : Y), ∫ (x : X) in U, f x y ∂μ ∂ν) (∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν)

Tactic:
congr 1 with y
-- Module: Mathlib.MeasureTheory.Integral.Prod
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
apply : ∀ (x : X) (hx : x ∉ U), f x y = 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in U, f x y ∂μ) (∫ (x : X), f x y ∂μ)

Tactic:
apply setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)

Premises used: MeasureTheory.setIntegral_eq_integral_of_forall_compl_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.Prod
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
hx : x ∉ U
contrapose! : ∀ (hx : f x y ≠ 0), x ∈ U
⊢ f x y = 0

Tactic:
contrapose! hx