mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: case h_ae
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
hE : CompleteSpace E
f g : α × β → E
hfg : f =ᵐ[μ.prod ν] g
hf : ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
⊢ ∫ (z : α × β), g z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ

Tactic:
convert! hf using 1

Goal state after:
case e'_2
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
hE : CompleteSpace E
f g : α × β → E
hfg : f =ᵐ[μ.prod ν] g
hf : ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
⊢ ∫ (z : α × β), g z ∂μ.prod ν = ∫ (z : α × β), f z ∂μ.prod ν

case e'_3
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
hE : CompleteSpace E
f g : α × β → E
hfg : f =ᵐ[μ.prod ν] g
hf : ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
⊢ ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Complex

Goal state before:
pp: case e'_6
⊢ ((Pi.basisFun ℝ (Fin 2)).map ↑basisOneI.equivFun.toContinuousLinearEquiv.symm).addHaar = volume

Tactic:
]

Goal state after:
case e'_6
⊢ ((Pi.basisFun ℝ (Fin 2)).map ↑basisOneI.equivFun.toContinuousLinearEquiv.symm).addHaar = volume
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α × β → E
hf : Integrable f (μ.prod ν)
⊢ ∫ (z : β × α), f z.swap ∂ν.prod μ = ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α × β → E
hf : Integrable f (μ.prod ν)
⊢ ∫ (z : β × α), f z.swap ∂ν.prod μ = ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: case inr
α : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
a b : ℝ
f : ℝ → α → E
hab : b ≤ a
h_int : Integrable (uncurry f) ((volume.restrict (Ioc b a)).prod μ)
⊢ -∫ (y : α), ∫ (x : ℝ) in Ioc b a, f x y ∂μ = -∫ (a_1 : α), ∫ (x : ℝ) in Ioc b a, f x a_1 ∂volume ∂μ

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
F : ℝ → ℝ → E
a b c d : ℝ
h : IntegrableOn (uncurry F) (uIoc a b ×ˢ uIoc c d) volume
⊢ ∫ (x : ℝ) in c..d, (if a ≤ b then 1 else -1) • ∫ (y : ℝ) in uIoc a b, F y x ∂volume =
    ∫ (y : ℝ) in c..d, ∫ (x : ℝ) in a..b, F x y

pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
F : ℝ → ℝ → E
a b c d : ℝ
h : IntegrableOn (uncurry F) (uIoc a b ×ˢ uIoc c d) volume
⊢ Integrable (uncurry fun y x ↦ F x y) ((volume.restrict (uIoc c d)).prod (volume.restrict (uIoc a b)))

Tactic:
]

Goal state after:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
F : ℝ → ℝ → E
a b c d : ℝ
h : IntegrableOn (uncurry F) (uIoc a b ×ˢ uIoc c d) volume
⊢ ∫ (x : ℝ) in c..d, (if a ≤ b then 1 else -1) • ∫ (y : ℝ) in uIoc a b, F y x ∂volume =
    ∫ (y : ℝ) in c..d, ∫ (x : ℝ) in a..b, F x y

E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
F : ℝ → ℝ → E
a b c d : ℝ
h : IntegrableOn (uncurry F) (uIoc a b ×ˢ uIoc c d) volume
⊢ Integrable (uncurry fun y x ↦ F x y) ((volume.restrict (uIoc c d)).prod (volume.restrict (uIoc a b)))
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z ↦ I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he₁ : e (1, 0) = 1
he₂ : e (0, 1) = I
he : ∀ (x y : ℝ), True
F : ℝ × ℝ → E := f ∘ ⇑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p ↦ f' (e p) ∘SL ↑e
hF' : ∀ (p : ℝ × ℝ), (-(I • F' p)) (1, 0) + (F' p) (0, 1) = -(I • (f' (e p)) 1 - (f' (e p)) I)
R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]
t : Set (ℝ × ℝ) := ⇑e ⁻¹' s
⊢ (((∫ (x : ℝ) in z.re..w.re, f (e (x, z.im))) - ∫ (x : ℝ) in z.re..w.re, f (e (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (e (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (e (z.re, y)) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (e (x, y))) 1 - (f' (e (x, y))) I

Tactic:
]

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z ↦ I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he₁ : e (1, 0) = 1
he₂ : e (0, 1) = I
he : ∀ (x y : ℝ), True
F : ℝ × ℝ → E := f ∘ ⇑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p ↦ f' (e p) ∘SL ↑e
hF' : ∀ (p : ℝ × ℝ), (-(I • F' p)) (1, 0) + (F' p) (0, 1) = -(I • (f' (e p)) 1 - (f' (e p)) I)
R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]
t : Set (ℝ × ℝ) := ⇑e ⁻¹' s
⊢ (((∫ (x : ℝ) in z.re..w.re, f (e (x, z.im))) - ∫ (x : ℝ) in z.re..w.re, f (e (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (e (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (e (z.re, y)) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (e (x, y))) 1 - (f' (e (x, y))) I
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
F : ℝ → ℝ → E
a b c d : ℝ
h : IntegrableOn (uncurry F) (uIoc a b ×ˢ uIoc c d) volume
⊢ IntegrableOn ((uncurry fun y x ↦ F x y) ∘ Prod.swap) (uIoc a b ×ˢ uIoc c d) volume

Tactic:
]

Goal state after:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
F : ℝ → ℝ → E
a b c d : ℝ
h : IntegrableOn (uncurry F) (uIoc a b ×ˢ uIoc c d) volume
⊢ IntegrableOn ((uncurry fun y x ↦ F x y) ∘ Prod.swap) (uIoc a b ×ˢ uIoc c d) volume
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹⁶ : MeasurableSpace α
inst✝¹⁵ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹⁴ : SFinite ν
inst✝¹³ : SFinite μ
E : Type u_5
F : Type u_6
G : Type u_7
𝕜 : Type u_8
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
B : E →L[𝕜] F →L[𝕜] G
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
this : Integrable (fun z ↦ (B (f z.1)) (g z.2)) (μ.prod ν)
⊢ (B.flip (∫ (y : β), g y ∂ν)) (∫ (x : α), f x ∂μ) = (B (∫ (x : α), f x ∂μ)) (∫ (x : β), g x ∂ν)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹⁶ : MeasurableSpace α
inst✝¹⁵ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹⁴ : SFinite ν
inst✝¹³ : SFinite μ
E : Type u_5
F : Type u_6
G : Type u_7
𝕜 : Type u_8
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
B : E →L[𝕜] F →L[𝕜] G
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
this : Integrable (fun z ↦ (B (f z.1)) (g z.2)) (μ.prod ν)
⊢ (B.flip (∫ (y : β), g y ∂ν)) (∫ (x : α), f x ∂μ) = (B (∫ (x : α), f x ∂μ)) (∫ (x : β), g x ∂ν)
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max w.im z.im) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z ↦ I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he₁ : e (1, 0) = 1
he₂ : e (0, 1) = I
he : ∀ (x y : ℝ), True
F : ℝ × ℝ → E := f ∘ ⇑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p ↦ f' (e p) ∘SL ↑e
hF' : ∀ (p : ℝ × ℝ), (-(I • F' p)) (1, 0) + (F' p) (0, 1) = -(I • (f' (e p)) 1 - (f' (e p)) I)
R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]
t : Set (ℝ × ℝ) := ⇑e ⁻¹' s
⊢ (((∫ (x : ℝ) in z.re..w.re, f (e (x, z.im))) - ∫ (x : ℝ) in z.re..w.re, f (e (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (e (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (e (z.re, y)) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (e (x, y))) 1 - (f' (e (x, y))) I

Tactic:
]

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max w.im z.im) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z ↦ I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he₁ : e (1, 0) = 1
he₂ : e (0, 1) = I
he : ∀ (x y : ℝ), True
F : ℝ × ℝ → E := f ∘ ⇑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p ↦ f' (e p) ∘SL ↑e
hF' : ∀ (p : ℝ × ℝ), (-(I • F' p)) (1, 0) + (F' p) (0, 1) = -(I • (f' (e p)) 1 - (f' (e p)) I)
R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]
t : Set (ℝ × ℝ) := ⇑e ⁻¹' s
⊢ (((∫ (x : ℝ) in z.re..w.re, f (e (x, z.im))) - ∫ (x : ℝ) in z.re..w.re, f (e (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (e (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (e (z.re, y)) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (e (x, y))) 1 - (f' (e (x, y))) I
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
𝕜 : Type u_5
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : CompleteSpace E
h : Integrable (fun z ↦ f z.1 • g z.2) (μ.prod ν)
⊢ ∫ (x : α), ∫ (y : β), f (x, y).1 • g (x, y).2 ∂ν ∂μ = (∫ (x : α), f x ∂μ) • ∫ (y : β), g y ∂ν

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
𝕜 : Type u_5
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : CompleteSpace E
h : Integrable (fun z ↦ f z.1 • g z.2) (μ.prod ν)
⊢ ∫ (x : α), ∫ (y : β), f (x, y).1 • g (x, y).2 ∂ν ∂μ = (∫ (x : α), f x ∂μ) • ∫ (y : β), g y ∂ν
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
L : Type u_5
inst✝ : RCLike L
f : α → L
g : β → L
s : Set α
t : Set β
⊢ ∫ (z : α × β), f z.1 * g z.2 ∂(μ.restrict s).prod (ν.restrict t) = (∫ (x : α) in s, f x ∂μ) * ∫ (y : β) in t, g y ∂ν

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
L : Type u_5
inst✝ : RCLike L
f : α → L
g : β → L
s : Set α
t : Set β
⊢ ∫ (z : α × β), f z.1 * g z.2 ∂(μ.restrict s).prod (ν.restrict t) = (∫ (x : α) in s, f x ∂μ) * ∫ (y : β) in t, g y ∂ν
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → E
⊢ ∫ (z : β × α), f z.swap.1 ∂ν.prod μ = ν.real univ • ∫ (x : α), f x ∂μ

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → E
⊢ ∫ (z : β × α), f z.swap.1 ∂ν.prod μ = ν.real univ • ∫ (x : α), f x ∂μ
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: E : Type u_5
F : Type u_6
G : Type u_7
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
mF : MeasurableSpace F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
μ : Measure E
inst✝² : IsProbabilityMeasure μ
ν : Measure F
inst✝¹ : IsProbabilityMeasure ν
L : E × F →L[ℝ] G
inst✝ : CompleteSpace G
hLμ : Integrable (fun x ↦ (L ∘SL ContinuousLinearMap.inl ℝ E F) x.1) (μ.prod ν)
hLν : Integrable (fun x ↦ (L ∘SL ContinuousLinearMap.inr ℝ E F) x.2) (μ.prod ν)
⊢ ∫ (x : E), ∫ (y : F), (L ∘SL ContinuousLinearMap.inl ℝ E F) (x, y).1 ∂ν ∂μ +
      ∫ (x : E), ∫ (y : F), (L ∘SL ContinuousLinearMap.inr ℝ E F) (x, y).2 ∂ν ∂μ =
    ∫ (x : E), (L ∘SL ContinuousLinearMap.inl ℝ E F) x ∂μ + ∫ (y : F), (L ∘SL ContinuousLinearMap.inr ℝ E F) y ∂ν

Tactic:
]

Goal state after:
E : Type u_5
F : Type u_6
G : Type u_7
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
mF : MeasurableSpace F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
μ : Measure E
inst✝² : IsProbabilityMeasure μ
ν : Measure F
inst✝¹ : IsProbabilityMeasure ν
L : E × F →L[ℝ] G
inst✝ : CompleteSpace G
hLμ : Integrable (fun x ↦ (L ∘SL ContinuousLinearMap.inl ℝ E F) x.1) (μ.prod ν)
hLν : Integrable (fun x ↦ (L ∘SL ContinuousLinearMap.inr ℝ E F) x.2) (μ.prod ν)
⊢ ∫ (x : E), ∫ (y : F), (L ∘SL ContinuousLinearMap.inl ℝ E F) (x, y).1 ∂ν ∂μ +
      ∫ (x : E), ∫ (y : F), (L ∘SL ContinuousLinearMap.inr ℝ E F) (x, y).2 ∂ν ∂μ =
    ∫ (x : E), (L ∘SL ContinuousLinearMap.inl ℝ E F) x ∂μ + ∫ (y : F), (L ∘SL ContinuousLinearMap.inr ℝ E F) y ∂ν
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max w.im z.im) \ s, HasFDerivAt f (f' x) x
Hi :
  IntegrableOn ((fun z ↦ I • (f' z) 1 - (f' z) I) ∘ ⇑measurableEquivRealProd.symm)
    (⇑measurableEquivRealProd.symm ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]])) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he₁ : e (1, 0) = 1
he₂ : e (0, 1) = I
he : ∀ (x y : ℝ), True
F : ℝ × ℝ → E := f ∘ ⇑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p ↦ f' (e p) ∘SL ↑e
hF' : ∀ (p : ℝ × ℝ), (-(I • F' p)) (1, 0) + (F' p) (0, 1) = -(I • (f' (e p)) 1 - (f' (e p)) I)
R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]
t : Set (ℝ × ℝ) := ⇑e ⁻¹' s
hR : ⇑e ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R
htc : ContinuousOn F R
htd : ∀ p ∈ Ioo (min z.re w.re) (max z.re w.re) ×ˢ Ioo (min w.im z.im) (max w.im z.im) \ t, HasFDerivAt F (F' p) p
⊢ IntegrableOn (fun x ↦ (-(I • F' x)) (1, 0) + (F' x) (0, 1)) ([[z.re, w.re]] ×ˢ [[w.im, z.im]]) volume

Tactic:
]

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max w.im z.im) \ s, HasFDerivAt f (f' x) x
Hi :
  IntegrableOn ((fun z ↦ I • (f' z) 1 - (f' z) I) ∘ ⇑measurableEquivRealProd.symm)
    (⇑measurableEquivRealProd.symm ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]])) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he₁ : e (1, 0) = 1
he₂ : e (0, 1) = I
he : ∀ (x y : ℝ), True
F : ℝ × ℝ → E := f ∘ ⇑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p ↦ f' (e p) ∘SL ↑e
hF' : ∀ (p : ℝ × ℝ), (-(I • F' p)) (1, 0) + (F' p) (0, 1) = -(I • (f' (e p)) 1 - (f' (e p)) I)
R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]
t : Set (ℝ × ℝ) := ⇑e ⁻¹' s
hR : ⇑e ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R
htc : ContinuousOn F R
htd : ∀ p ∈ Ioo (min z.re w.re) (max z.re w.re) ×ˢ Ioo (min w.im z.im) (max w.im z.im) \ t, HasFDerivAt F (F' p) p
⊢ IntegrableOn (fun x ↦ (-(I • F' x)) (1, 0) + (F' x) (0, 1)) ([[z.re, w.re]] ×ˢ [[w.im, z.im]]) volume
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
⊢ ∮ (z : ℂ) in C(c, rexp b), (z - c)⁻¹ • f z = ∮ (z : ℂ) in C(c, rexp a), (z - c)⁻¹ • f z

Tactic:
]

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
⊢ ∮ (z : ℂ) in C(c, rexp b), (z - c)⁻¹ • f z = ∮ (z : ℂ) in C(c, rexp a), (z - c)⁻¹ • f z
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case inl
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ (Set.univ.pi fun i ↦ Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Set.Icc a b) volume
i : Fin (n + 1)
hi : a i = b i
⊢ (∫ (x : Fin (n + 1) → ℝ) in Set.univ.pi fun i ↦ Set.Ioc (a i) (b i), ∑ i, (f' x) (e i) i ∂Measure.pi fun x ↦ volume) =
    ∑ i,
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (a i) x) i)

Tactic:
]

Goal state after:
case inl
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ (Set.univ.pi fun i ↦ Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Set.Icc a b) volume
i : Fin (n + 1)
hi : a i = b i
⊢ (∫ (x : Fin (n + 1) → ℝ) in Set.univ.pi fun i ↦ Set.Ioc (a i) (b i), ∑ i, (f' x) (e i) i ∂Measure.pi fun x ↦ volume) =
    ∑ i,
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (a i) x) i)
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: case refine_4.refine_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J ↦ integral J GP (fun x ↦ f (i.insertNth y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x ↦ ⋯.toBoxAdditive
F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ Box.Icc I \ s
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε'0 : 0 < ε'
hlt : 2 * ↑c * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : closedBall x δ ∩ Box.Icc I ⊆ {x_1 | (fun x_2 ↦ ‖f x_2 - f x - (f' x) (x_2 - x)‖ ≤ ε' * ‖x_2 - x‖) x_1}
J : Box (Fin (n + 1))
hle : J ≤ I
hJδ : Box.Icc J ⊆ closedBall x δ
hxJ : x ∈ Box.Icc J
hJc : GP.bDistortion = true → J.distortion ≤ c
⊢ 2 * ↑c * ε' * volume.toBoxAdditive J ≤ ε * (volume.toBoxAdditive.restrict ↑I ⋯) J

Tactic:
]

Goal state after:
case refine_4.refine_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J ↦ integral J GP (fun x ↦ f (i.insertNth y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x ↦ ⋯.toBoxAdditive
F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ Box.Icc I \ s
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε'0 : 0 < ε'
hlt : 2 * ↑c * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : closedBall x δ ∩ Box.Icc I ⊆ {x_1 | (fun x_2 ↦ ‖f x_2 - f x - (f' x) (x_2 - x)‖ ≤ ε' * ‖x_2 - x‖) x_1}
J : Box (Fin (n + 1))
hle : J ≤ I
hJδ : Box.Icc J ⊆ closedBall x δ
hxJ : x ∈ Box.Icc J
hJc : GP.bDistortion = true → J.distortion ≤ c
⊢ 2 * ↑c * ε' * volume.toBoxAdditive J ≤ ε * (volume.toBoxAdditive.restrict ↑I ⋯) J