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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
⊢ HasSum (fun n ↦ ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
⊢ HasSum (fun n ↦ (cauchyPowerSeries f c R n) fun x ↦ w) ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
hf : CircleIntegrable f c ↑R
hR : 0 < R
y✝ : ℂ
hy : y✝ ∈ eball 0 ↑R
⊢ ‖y✝‖ < ↑R

Tactic:
by

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

Goal state before:
pp: c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : HasSum (fun n ↦ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ = 2 * ↑π * I

Tactic:
by

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

Goal state before:
pp: c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
⊢ ∀ (n : ℕ), n ≠ 0 → ∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1) = 0

Tactic:
by

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

Goal state before:
pp: c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → ∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1) = 0
⊢ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹ = 2 * ↑π * I

Tactic:
by

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

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
I : Box (Fin (n + 1))
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 (Box.Icc I)
Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc I) volume
J : ℕ →o Box (Fin (n + 1))
hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I
hJl : ∀ (x : Fin (n + 1)), Tendsto (fun i ↦ (Box.lower ∘ ⇑J) i x) atTop (𝓝 (I.lower x))
hJu : ∀ (x : Fin (n + 1)), Tendsto (fun i ↦ (Box.upper ∘ ⇑J) i x) atTop (𝓝 (I.upper x))
hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I
hJ_le : ∀ (k : ℕ), J k ≤ I
HcJ : ∀ (k : ℕ), ContinuousOn f (Box.Icc (J k))
HdJ : ∀ (k : ℕ), ∀ x ∈ Box.Icc (J k) \ s, HasFDerivWithinAt f (f' x) (Box.Icc (J k)) x
HiJ : ∀ (k : ℕ), IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc (J k)) volume
HJ_eq :
  ∀ (k : ℕ),
    ∫ (x : Fin (n + 1) → ℝ) in Box.Icc (J k), ∑ i, (f' x) (e i) i =
      ∑ i,
        ((∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).upper i) x) i) -
          ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).lower i) x) i)
i : Fin (n + 1)
c : ℕ → ℝ
d : ℝ
hc : ∀ (k : ℕ), c k ∈ Set.Icc (I.lower i) (I.upper i)
hcd : Tendsto c atTop (𝓝 d)
hd : d ∈ Set.Icc (I.lower i) (I.upper i)
Hic : ∀ (k : ℕ), IntegrableOn (fun x ↦ f (i.insertNth (c k) x) i) (Box.Icc (I.face i)) volume
Hid : IntegrableOn (fun x ↦ f (i.insertNth d x) i) (Box.Icc (I.face i)) volume
⊢ Tendsto (fun k ↦ ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth d x) i) atTop
    (𝓝 (∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth d x) i))

Tactic:
by

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

Goal state before:
pp: c w : ℂ
R : ℝ
hw : w ∈ ball c R
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ = 2 * ↑π * I

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Complex

Goal state before:
pp: ⊢ MeasurePreserving (⇑measurableEquivPi) volume volume

Tactic:
by

Goal state after:
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 ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ

Tactic:
by

Goal state after:
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]] ×ℂ [[z.im, w.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]] ×ℂ [[z.im, w.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
⊢ ∀ (p : ℝ × ℝ), (-(I • F' p)) (1, 0) + (F' p) (0, 1) = -(I • (f' (e p)) 1 - (f' (e p)) I)

Tactic:
by

Goal state after:
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 ∂μ.prod ν = ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν

Tactic:
by

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

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

Tactic:
by

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 a..b, ∫ (y : ℝ) in c..d, F x y = ∫ (y : ℝ) in c..d, ∫ (x : ℝ) in a..b, F x y

Tactic:
by

Goal state after:
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
s : Set α
t : Set β
hf : IntegrableOn f (s ×ˢ t) (μ.prod ν)
⊢ ∫ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν = ∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂ν ∂μ

Tactic:
by

Goal state after:
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 ν
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry fun x ↦ ⇑(B x))

Tactic:
by

Goal state after:
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 ν
⊢ ∫ (z : α × β), (B (f z.1)) (g z.2) ∂μ.prod ν = (B (∫ (x : α), f x ∂μ)) (∫ (y : β), g y ∂ν)

Tactic:
by

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

Goal state before:
pp: case neg
α : 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
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν = (∫ (x : α), f x ∂μ) • ∫ (y : β), g y ∂ν

Tactic:
simp [integral, hE]

Goal state after:
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 μ
𝕜 : 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 ν)
⊢ ¬Integrable f μ ∨ ¬Integrable g ν

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: 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
this✝ :
  ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ y₁ ∈ closedBall x δ ∩ Box.Icc I, ∀ y₂ ∈ closedBall x δ ∩ Box.Icc I, ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ : ∀ y₁ ∈ closedBall x δ ∩ Box.Icc I, ∀ y₂ ∈ closedBall x δ ∩ Box.Icc I, ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ Box.Icc J
x✝ : GP.bDistortion = true → J.distortion ≤ c
Hl : J.lower i ∈ Set.Icc (J.lower i) (J.upper i)
Hu : J.upper i ∈ Set.Icc (J.lower i) (J.upper i)
Hi : ∀ x ∈ Set.Icc (J.lower i) (J.upper i), Integrable (J.face i) GP (fun y ↦ f (i.insertNth x y)) BoxAdditiveMap.volume
hJδ' : Box.Icc J ⊆ closedBall x δ ∩ Box.Icc I
Hmaps : ∀ z ∈ Set.Icc (J.lower i) (J.upper i), MapsTo (i.insertNth z) (Box.Icc (J.face i)) (closedBall x δ ∩ Box.Icc I)
this : ∀ (j : Fin (n + 1)), |J.upper j - J.lower j| ≤ 2 * δ
⊢ ∏ j, |J.upper j - J.lower j| ≤ ∏ j, 2 * δ

Tactic:
by

Goal state after:
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 μ
𝕜 : Type u_5
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν = (∫ (x : α), f x ∂μ) • ∫ (y : β), g y ∂ν

Tactic:
by

Goal state after:
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 : α × β) in s ×ˢ t, f z.1 * g z.2 ∂μ.prod ν = (∫ (x : α) in s, f x ∂μ) * ∫ (y : β) in t, g y ∂ν

Tactic:
by

Goal state after:
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.2 ∂μ.prod ν = μ.real univ • ∫ (y : β), f y ∂ν

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: 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
this✝ :
  ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ y₁ ∈ closedBall x δ ∩ Box.Icc I, ∀ y₂ ∈ closedBall x δ ∩ Box.Icc I, ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ : ∀ y₁ ∈ closedBall x δ ∩ Box.Icc I, ∀ y₂ ∈ closedBall x δ ∩ Box.Icc I, ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ Box.Icc J
x✝ : GP.bDistortion = true → J.distortion ≤ c
Hl : J.lower i ∈ Set.Icc (J.lower i) (J.upper i)
Hu : J.upper i ∈ Set.Icc (J.lower i) (J.upper i)
Hi : ∀ x ∈ Set.Icc (J.lower i) (J.upper i), Integrable (J.face i) GP (fun y ↦ f (i.insertNth x y)) BoxAdditiveMap.volume
hJδ' : Box.Icc J ⊆ closedBall x δ ∩ Box.Icc I
Hmaps : ∀ z ∈ Set.Icc (J.lower i) (J.upper i), MapsTo (i.insertNth z) (Box.Icc (J.face i)) (closedBall x δ ∩ Box.Icc I)
this : ∀ (j : Fin (n + 1)), |J.upper j - J.lower j| ≤ 2 * δ
⊢ ∏ j, 2 * δ = (2 * δ) ^ (n + 1)

Tactic:
by

Goal state after:
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.1 ∂μ.prod ν = ν.real univ • ∫ (x : α), f x ∂μ

Tactic:
by

Goal state after:
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
hLμ : Integrable (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F)) μ
hLν : Integrable (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F)) ν
⊢ Integrable (⇑L) (μ.prod ν)

Tactic:
by

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

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
I : Box (Fin (n + 1))
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 (Box.Icc I)
Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc I) volume
J : ℕ →o Box (Fin (n + 1))
hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I
hJl : ∀ (x : Fin (n + 1)), Tendsto (fun i ↦ (Box.lower ∘ ⇑J) i x) atTop (𝓝 (I.lower x))
hJu : ∀ (x : Fin (n + 1)), Tendsto (fun i ↦ (Box.upper ∘ ⇑J) i x) atTop (𝓝 (I.upper x))
hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I
hJ_le : ∀ (k : ℕ), J k ≤ I
HcJ : ∀ (k : ℕ), ContinuousOn f (Box.Icc (J k))
HdJ : ∀ (k : ℕ), ∀ x ∈ Box.Icc (J k) \ s, HasFDerivWithinAt f (f' x) (Box.Icc (J k)) x
HiJ : ∀ (k : ℕ), IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc (J k)) volume
HJ_eq :
  ∀ (k : ℕ),
    ∫ (x : Fin (n + 1) → ℝ) in Box.Icc (J k), ∑ i, (f' x) (e i) i =
      ∑ i,
        ((∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).upper i) x) i) -
          ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).lower i) x) i)
i : Fin (n + 1)
c : ℕ → ℝ
d : ℝ
hc : ∀ (k : ℕ), c k ∈ Set.Icc (I.lower i) (I.upper i)
hcd : Tendsto c atTop (𝓝 d)
hd : d ∈ Set.Icc (I.lower i) (I.upper i)
Hic : ∀ (k : ℕ), IntegrableOn (fun x ↦ f (i.insertNth (c k) x) i) (Box.Icc (I.face i)) volume
Hid : IntegrableOn (fun x ↦ f (i.insertNth d x) i) (Box.Icc (I.face i)) volume
H :
  Tendsto (fun k ↦ ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth d x) i) atTop
    (𝓝 (∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth d x) i))
ε : ℝ
εpos : 0 < ε
hvol_pos : ∀ (J : Box (Fin n)), 0 < ∏ j, (J.upper j - J.lower j)
δ : ℝ
δpos : δ > 0
hδ :
  ∀ x ∈ Box.Icc I, ∀ y ∈ Box.Icc I, dist x y ≤ δ → dist (f x) (f y) ≤ ε / ∏ j, ((I.face i).upper j - (I.face i).lower j)
k : ℕ
hk : dist (c k) d < δ
Hsub : Box.Icc ((J k).face i) ⊆ Box.Icc (I.face i)
⊢ ‖∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth d x) i - f (i.insertNth (c k) x) i‖ ≤
    (ε / ∏ j, ((I.face i).upper j - (I.face i).lower j)) * (volume (Box.Icc ((J k).face i))).toReal

Tactic:
refine norm_setIntegral_le_of_norm_le_const (((J k).face i).measure_Icc_lt_top _)
        fun x hx => ?_
      rw [← dist_eq_norm]
      calc
        dist (f (i.insertNth d x) i) (f (i.insertNth (c k) x) i) ≤
            dist (f (i.insertNth d x)) (f (i.insertNth (c k) x)) :=
          dist_le_pi_dist (f (i.insertNth d x)) (f (i.insertNth (c k) x)) i
        _ ≤ ε / ∏ j, ((I.face i).upper j - (I.face i).lower j) :=
          hδ _ (I.mapsTo_insertNth_face_Icc hd <| Hsub hx) _
            (I.mapsTo_insertNth_face_Icc (hc _) <| Hsub hx) ?_
      rw [Fin.dist_insertNth_insertNth, dist_self, dist_comm]
      exact max_le hk.le δpos.lt.le

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

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
I : Box (Fin (n + 1))
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 (Box.Icc I)
Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc I) volume
J : ℕ →o Box (Fin (n + 1))
hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I
hJl : ∀ (x : Fin (n + 1)), Tendsto (fun i ↦ (Box.lower ∘ ⇑J) i x) atTop (𝓝 (I.lower x))
hJu : ∀ (x : Fin (n + 1)), Tendsto (fun i ↦ (Box.upper ∘ ⇑J) i x) atTop (𝓝 (I.upper x))
hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I
hJ_le : ∀ (k : ℕ), J k ≤ I
HcJ : ∀ (k : ℕ), ContinuousOn f (Box.Icc (J k))
HdJ : ∀ (k : ℕ), ∀ x ∈ Box.Icc (J k) \ s, HasFDerivWithinAt f (f' x) (Box.Icc (J k)) x
HiJ : ∀ (k : ℕ), IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc (J k)) volume
HJ_eq :
  ∀ (k : ℕ),
    ∫ (x : Fin (n + 1) → ℝ) in Box.Icc (J k), ∑ i, (f' x) (e i) i =
      ∑ i,
        ((∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).upper i) x) i) -
          ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).lower i) x) i)
i : Fin (n + 1)
c : ℕ → ℝ
d : ℝ
hc : ∀ (k : ℕ), c k ∈ Set.Icc (I.lower i) (I.upper i)
hcd : Tendsto c atTop (𝓝 d)
hd : d ∈ Set.Icc (I.lower i) (I.upper i)
Hic : ∀ (k : ℕ), IntegrableOn (fun x ↦ f (i.insertNth (c k) x) i) (Box.Icc (I.face i)) volume
Hid : IntegrableOn (fun x ↦ f (i.insertNth d x) i) (Box.Icc (I.face i)) volume
H :
  Tendsto (fun k ↦ ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth d x) i) atTop
    (𝓝 (∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth d x) i))
ε : ℝ
εpos : 0 < ε
hvol_pos : ∀ (J : Box (Fin n)), 0 < ∏ j, (J.upper j - J.lower j)
δ : ℝ
δpos : δ > 0
hδ :
  ∀ x ∈ Box.Icc I, ∀ y ∈ Box.Icc I, dist x y ≤ δ → dist (f x) (f y) ≤ ε / ∏ j, ((I.face i).upper j - (I.face i).lower j)
k : ℕ
hk : dist (c k) d < δ
Hsub : Box.Icc ((J k).face i) ⊆ Box.Icc (I.face i)
⊢ ‖∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth d x) i - f (i.insertNth (c k) x) i‖ ≤
    (ε / ∏ j, ((I.face i).upper j - (I.face i).lower j)) * (volume (Box.Icc ((J k).face i))).toReal

Tactic:
by

Goal state after:
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 (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F)) μ
hLν : Integrable (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F)) ν
⊢ ∫ (p : E × F), L p ∂μ.prod ν =
    ∫ (x : E), (L ∘SL ContinuousLinearMap.inl ℝ E F) x ∂μ + ∫ (y : F), (L ∘SL ContinuousLinearMap.inr ℝ E F) y ∂ν

Tactic:
by

Goal state after:
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]] ×ℂ [[z.im, w.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]] ×ℂ [[z.im, w.im]]) volume
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (↑x + ↑y * I)) 1 - (f' (↑x + ↑y * I)) I

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: 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
this :
  ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ y₁ ∈ closedBall x δ ∩ Box.Icc I, ∀ y₂ ∈ closedBall x δ ∩ Box.Icc I, ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ : ∀ y₁ ∈ closedBall x δ ∩ Box.Icc I, ∀ y₂ ∈ closedBall x δ ∩ Box.Icc I, ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : Box.Icc J ⊆ closedBall x δ
x✝² : x ∈ Box.Icc J
x✝¹ : GP.bDistortion = true → J.distortion ≤ c
Hl : J.lower i ∈ Set.Icc (J.lower i) (J.upper i)
Hu : J.upper i ∈ Set.Icc (J.lower i) (J.upper i)
Hi : ∀ x ∈ Set.Icc (J.lower i) (J.upper i), Integrable (J.face i) GP (fun y ↦ f (i.insertNth x y)) BoxAdditiveMap.volume
hJδ' : Box.Icc J ⊆ closedBall x δ ∩ Box.Icc I
Hmaps : ∀ z ∈ Set.Icc (J.lower i) (J.upper i), MapsTo (i.insertNth z) (Box.Icc (J.face i)) (closedBall x δ ∩ Box.Icc I)
j : Fin n
x✝ : j ∈ Finset.univ
⊢ δ + δ ≤ 1 / 2 + 1 / 2

Tactic:
by

Goal state after: