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 μ
𝕜 : Type u_5
inst_6 : RCLike 𝕜
inst_7 : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : CompleteSpace E
h : ¬Integrable (ε := E) (fun (z : α × β) ↦ f z.1 • g z.2) (μ.prod ν)
H : ¬Integrable g ν
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν =
    HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) (β := E) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)

Tactic:
simp [integral_undef h, integral_undef H]

Premises used: MeasureTheory.integral_undef
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
L : Type u_5
inst_4 : RCLike L
f : α → L
g : β → L
⊢ ∫ (z : α × β), f z.1 * g z.2 ∂μ.prod ν = HMul.hMul (α := L) (∫ (x : α), f x ∂μ) (∫ (y : β), g y ∂ν)

Tactic:
integral_prod_smul f g

Premises used: MeasureTheory.integral_prod_smul
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
L : Type u_5
inst_4 : RCLike L
f : α → L
g : β → L
s : Set α
t : Set β
rw :
  ∫ (z : α × β), f z.1 * g z.2 ∂(μ.restrict s).prod (ν.restrict t) =
    HMul.hMul (α := L) (∫ (x : α) in s, f x ∂μ) (∫ (y : β) in t, g y ∂ν)
⊢ ∫ (z : α × β) in s ×ˢ t, f z.1 * g z.2 ∂μ.prod ν =
    HMul.hMul (α := L) (∫ (x : α) in s, f x ∂μ) (∫ (y : β) in t, g y ∂ν)

Tactic:
rw [← Measure.prod_restrict s t]

Premises used: MeasureTheory.Measure.prod_restrict
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
L : Type u_5
inst_4 : RCLike L
f : α → L
g : β → L
s : Set α
t : Set β
⊢ ∫ (z : α × β), f z.1 * g z.2 ∂(μ.restrict s).prod (ν.restrict t) =
    HMul.hMul (α := L) (∫ (x : α) in s, f x ∂μ) (∫ (y : β) in t, g y ∂ν)

Tactic:
apply integral_prod_mul

Premises used: MeasureTheory.integral_prod_mul
-- 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
⊢ ∫ (z : α × β), f z.2 ∂μ.prod ν = HSMul.hSMul (β := E) (μ.real univ) (∫ (y : β), f y ∂ν)

Tactic:
simpa using integral_prod_smul (1 : α → ℝ) f

Premises used: OfNat.ofNat, MeasureTheory.integral_prod_smul
-- 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
rw : ∫ (z : β × α), f z.swap.1 ∂ν.prod μ = HSMul.hSMul (β := E) (ν.real univ) (∫ (x : α), f x ∂μ)
⊢ ∫ (z : α × β), f z.1 ∂μ.prod ν = HSMul.hSMul (β := E) (ν.real univ) (∫ (x : α), f x ∂μ)

Tactic:
rw [← integral_prod_swap]

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
⊢ ∫ (z : β × α), f z.swap.1 ∂ν.prod μ = HSMul.hSMul (β := E) (ν.real univ) (∫ (x : α), f x ∂μ)

Tactic:
apply integral_fun_snd

Premises used: MeasureTheory.integral_fun_snd
-- Module: Mathlib.MeasureTheory.Integral.Prod
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
hLμ : Integrable.{u_7, u_5} (ε := G) (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → G) μ
hLν : Integrable.{u_7, u_6} (ε := G) (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → G) ν
simp_rw :
  Integrable (ε := G)
    (fun (v : E × F) ↦
      HAdd.hAdd (α := G) (β := G) ((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → G) v.1 : G)
        ((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → G) v.2 : G))
    (μ.prod ν)
⊢ Integrable (ε := G) (fun (v : E × F) ↦ (L : (a : E × F) → G) v) (μ.prod ν)

Tactic:
simp_rw [← L.comp_inl_add_comp_inr]

Premises used: ContinuousLinearMap.comp_inl_add_comp_inr
-- Module: Mathlib.MeasureTheory.Integral.Prod
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
hLμ : Integrable.{u_7, u_5} (ε := G) (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → G) μ
hLν : Integrable.{u_7, u_6} (ε := G) (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → G) ν
⊢ Integrable (ε := G)
    (fun (v : E × F) ↦
      HAdd.hAdd (α := G) (β := G) ((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → G) v.1 : G)
        ((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → G) v.2 : G))
    (μ.prod ν)

Tactic:
(hLμ.comp_fst ν).add (hLν.comp_snd μ)

Premises used: MeasureTheory.Integrable.comp_snd, MeasureTheory.Integrable.comp_fst, MeasureTheory.Integrable.add
-- Module: Mathlib.MeasureTheory.Integral.Prod
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
hLμ : Integrable.{u_7, u_5} (ε := G) (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → G) μ
hLν : Integrable.{u_7, u_6} (ε := G) (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → G) ν
⊢ Integrable (ε := G)
    (fun (v : E × F) ↦
      HAdd.hAdd (α := G) (β := G) ((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → G) v.1 : G)
        ((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → G) v.2 : G))
    (μ.prod ν)

Tactic:
exact (hLμ.comp_fst ν).add (hLν.comp_snd μ)

Premises used: MeasureTheory.Integrable.comp_snd, MeasureTheory.Integrable.comp_fst, MeasureTheory.Integrable.add
-- Module: Mathlib.MeasureTheory.Integral.Prod
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
hμ : Integrable id μ
hν : Integrable id ν
⊢ Integrable (ε := G) (⇑L : (a : E × F) → G) (μ.prod ν)

Tactic:
integrable_continuousLinearMap_prod' (ContinuousLinearMap.integrable_comp _ hμ)
    (ContinuousLinearMap.integrable_comp _ hν)

Premises used: ContinuousLinearMap.integrable_comp, MeasureTheory.integrable_continuousLinearMap_prod'
-- Module: Mathlib.MeasureTheory.Integral.Prod
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_5} (ε := G) (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → G) μ
hLν : Integrable.{u_7, u_6} (ε := G) (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → G) ν
simp_rw :
  ∫ (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 ∂ν)
⊢ ∫ (p : E × F), (L : (a : E × F) → G) p ∂μ.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 ∂ν)

Tactic:
simp_rw [← L.comp_inl_add_comp_inr]

Premises used: ContinuousLinearMap.comp_inl_add_comp_inr
-- Module: Mathlib.MeasureTheory.Integral.Prod
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_5} (ε := G) (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → G) μ
hLν : Integrable.{u_7, u_6} (ε := G) (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → G) ν
⊢ Integrable (ε := G) (fun (x : E × F) ↦ (L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → G) x.1) (μ.prod ν)

Tactic:
replace hLμ := ((memLp_one_iff_integrable.mpr hLμ).comp_fst ν).integrable le_rfl
-- Module: Mathlib.MeasureTheory.Integral.Prod
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 ν)
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.Prod
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 ν)
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 ∂ν)
⊢ ∫ (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 ∂ν)

Tactic:
rw [integral_add hLμ hLν, integral_prod _ hLμ, integral_prod _ hLν]

Premises used: MeasureTheory.integral_add, MeasureTheory.integral_prod
-- Module: Mathlib.MeasureTheory.Integral.Prod
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 ν)
⊢ 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:
simp
-- Module: Mathlib.MeasureTheory.Integral.Prod
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
hμ : Integrable id μ
hν : Integrable id ν
⊢ ∫ (p : E × F), (L : (a : E × F) → G) p ∂μ.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 ∂ν)

Tactic:
integral_continuousLinearMap_prod' (ContinuousLinearMap.integrable_comp _ hμ)
    (ContinuousLinearMap.integrable_comp _ hν)

Premises used: ContinuousLinearMap.integrable_comp, MeasureTheory.integral_continuousLinearMap_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)
⊢ Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
have : Fact (μ U < ∞) := ⟨(IsCompact.image h'f continuous_fst).measure_lt_top⟩
-- 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 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
⊢ Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
have : Fact (ν V < ∞) := ⟨(IsCompact.image h'f continuous_snd).measure_lt_top⟩
-- 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 : ∀ (x : X), Eq.{u_3 + 1} (α := E) (∫ (y : Y), f x y ∂ν) (∫ (y : Y) in V, f x y ∂ν)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ) (∫ (x : X), ∫ (y : Y) in V, f x y ∂ν ∂μ)

Tactic:
congr 1 with x
-- 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
apply : ∀ (y : Y) (hy : y ∉ V), f x y = 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (y : Y), f x y ∂ν) (∫ (y : Y) in V, f x y ∂ν)

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

Premises used: MeasureTheory.setIntegral_eq_integral_of_forall_compl_eq_zero, Eq.symm
-- 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
hy : y ∉ V
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∞))
x : X
y : Y
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∞))
x : X
y : Y
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∞))
x : X
y : Y
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∞))
apply : ∀ (x : X) (hx : x ∉ U), Eq.{u_3 + 1} (α := E) (∫ (y : Y) in V, f x y ∂ν) 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 ∂ν ∂μ)

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

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

Tactic:
contrapose! hx