mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z w : ℂ
Hd : DifferentiableOn ℝ f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hi : IntegrableOn (fun z ↦ I • (fderiv ℝ f z) 1 - (fderiv ℝ f z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
x : ℂ
hx : x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ ∅
⊢ [[z.re, w.re]] ×ℂ [[z.im, w.im]] ∈ 𝓝 x

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
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, DifferentiableAt ℂ f x
⊢ (((∫ (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) =
    0

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)
⊢ (ε / ∏ 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.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
this : ∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp a) θ)
⊢ ∮ (z : ℂ) in C(c, rexp b), (z - c)⁻¹ • f z = ∮ (z : ℂ) in C(c, rexp a), (z - c)⁻¹ • f z

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
⊢ ∫ (x : Fin (n + 1) → ℝ) in Box.Icc I, ∑ i, (f' x) (e i) i =
    ∑ i,
      ((∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) -
        ∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)

Tactic:
by

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

Goal state before:
pp: E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this✝ : Fact (μ U < ∞)
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (ν V < ∞)
⊢ ∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ = ∫ (x : X), ∫ (y : Y) in V, f x y ∂ν ∂μ

Tactic:
by

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

Goal state before:
pp: case refine_4
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}
⊢ ∃ δ > 0,
    ∀ J ≤ I,
      Box.Icc J ⊆ closedBall x δ →
        x ∈ Box.Icc J →
          (GP.bDistortion = true → J.distortion ≤ c) →
            dist ((BoxAdditiveMap.volume J) ((f' x) (Pi.single i 1))) (F J) ≤ ε * (volume.toBoxAdditive.restrict ↑I ⋯) J

Tactic:
refine ⟨δ, δ0, fun J hle hJδ hxJ hJc => ?_⟩

Goal state after:
case refine_4
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
⊢ dist ((BoxAdditiveMap.volume J) ((f' x) (Pi.single i 1))) (F J) ≤ ε * (volume.toBoxAdditive.restrict ↑I ⋯) J
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this✝ : Fact (μ U < ∞)
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (ν V < ∞)
x : X
hx : x ∉ U
⊢ ∀ (y : Y), f x y = 0

Tactic:
by

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

Goal state before:
pp: E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this✝ : Fact (μ U < ∞)
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (ν V < ∞)
⊢ ∫ (x : X), ∫ (y : Y) in V, f x y ∂ν ∂μ = ∫ (x : X) in U, ∫ (y : Y) in V, 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
c : ℂ
f : ℂ → E
s : Set ℂ
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
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun x ↦ c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
⊢ MapsTo g R A

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
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)
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun x ↦ c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
h_maps : MapsTo g R A
hc : ContinuousOn (f ∘ g) R
z : ℂ
hz : z ∈ Ioo (min a b) (max a b) ×ℂ Ioo (min 0 (2 * π)) (max 0 (2 * π)) \ g ⁻¹' s
⊢ g z ∈ ball c (rexp b) \ closedBall c (rexp a)

Tactic:
simpa [g, dist_eq, norm_exp, hle, and_comm] using hz.1.1

Goal state after:
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
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)
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun x ↦ c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
h_maps : MapsTo g R A
hc : ContinuousOn (f ∘ g) R
⊢ ∀ z ∈ Ioo (min a b) (max a b) ×ℂ Ioo (min 0 (2 * π)) (max 0 (2 * π)) \ g ⁻¹' s, DifferentiableAt ℂ (f ∘ g) z

Tactic:
by

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

Goal state before:
pp: E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this✝ : Fact (μ U < ∞)
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (ν V < ∞)
⊢ ∫ (x : X) in U, ∫ (y : Y) in V, f x y ∂ν ∂μ = ∫ (y : Y) in V, ∫ (x : X) in U, 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
c : ℂ
r R : ℝ
h0 : 0 < r
hle : r ≤ R
f : ℂ → E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ ball c r)
hd : ∀ z ∈ (ball c R \ closedBall c r) \ s, DifferentiableAt ℂ f z
⊢ ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z = ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z

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
ε' : ℝ
ε'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
⊢ 0 ≤ volume.toBoxAdditive J

Tactic:
by

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

Goal state before:
pp: E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this✝ : Fact (μ U < ∞)
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (ν V < ∞)
y : Y
hy : y ∉ V
⊢ ∀ (x : X), f x y = 0

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
ε' : ℝ
ε'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
⊢ volume.toBoxAdditive J ≤ (volume.toBoxAdditive.restrict ↑I ⋯) J

Tactic:
by

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

Goal state before:
pp: E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this✝ : Fact (μ U < ∞)
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (ν V < ∞)
⊢ ∫ (y : Y) in V, ∫ (x : X) in U, f x y ∂μ ∂ν = ∫ (y : Y), ∫ (x : X) in U, f x y ∂μ ∂ν

Tactic:
by

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

Goal state before:
pp: 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
this : (Set.univ.pi fun j ↦ Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
i : Fin n
hi : a (j.succAbove i) = b (j.succAbove i)
hi' : Set.Ioc (a (j.succAbove i)) (b (j.succAbove i)) = ∅
hne : j.succAbove i ≠ j
⊢ Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove) =ᵐ[volume] ∅

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)
⊢ HasIntegral I GP (fun x ↦ (f' x) (Pi.single i 1)) BoxAdditiveMap.volume
    (integral (I.face i) GP (fun x ↦ f (i.insertNth (I.upper i) x)) BoxAdditiveMap.volume -
      integral (I.face i) GP (fun x ↦ f (i.insertNth (I.lower i) x)) BoxAdditiveMap.volume)

Tactic:
by

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

Goal state before:
pp: case inl.inr
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
this✝ : (Set.univ.pi fun j ↦ Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
i : Fin n
hi : a (j.succAbove i) = b (j.succAbove i)
hi' : Set.Ioc (a (j.succAbove i)) (b (j.succAbove i)) = ∅
hne : j.succAbove i ≠ j
this : Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove) =ᵐ[volume] ∅
⊢ (∫ (x : Fin n → ℝ) in Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove), f (j.insertNth (b j) x) j) -
      ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove), f (j.insertNth (a j) x) j =
    0

Tactic:
setIntegral_congr_set this,

Goal state after:
case inl.inr
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
this✝ : (Set.univ.pi fun j ↦ Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
i : Fin n
hi : a (j.succAbove i) = b (j.succAbove i)
hi' : Set.Ioc (a (j.succAbove i)) (b (j.succAbove i)) = ∅
hne : j.succAbove i ≠ j
this : Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove) =ᵐ[volume] ∅
⊢ (∫ (x : Fin n → ℝ) in ∅, f (j.insertNth (b j) x) j) -
      ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove), f (j.insertNth (a j) x) j =
    0
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this✝ : Fact (μ U < ∞)
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (ν V < ∞)
⊢ ∫ (y : Y), ∫ (x : X) in U, f x y ∂μ ∂ν = ∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν

Tactic:
by

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

Goal state before:
pp: case inl.inr
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
this✝ : (Set.univ.pi fun j ↦ Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
i : Fin n
hi : a (j.succAbove i) = b (j.succAbove i)
hi' : Set.Ioc (a (j.succAbove i)) (b (j.succAbove i)) = ∅
hne : j.succAbove i ≠ j
this : Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove) =ᵐ[volume] ∅
⊢ (∫ (x : Fin n → ℝ) in ∅, f (j.insertNth (b j) x) j) -
      ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove), f (j.insertNth (a j) x) j =
    0

Tactic:
setIntegral_congr_set this,

Goal state after:
case inl.inr
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
this✝ : (Set.univ.pi fun j ↦ Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
i : Fin n
hi : a (j.succAbove i) = b (j.succAbove i)
hi' : Set.Ioc (a (j.succAbove i)) (b (j.succAbove i)) = ∅
hne : j.succAbove i ≠ j
this : Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove) =ᵐ[volume] ∅
⊢ (∫ (x : Fin n → ℝ) in ∅, f (j.insertNth (b j) x) j) - ∫ (x : Fin n → ℝ) in ∅, f (j.insertNth (a j) x) j = 0
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) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → 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
⊢ HasIntegral I GP (fun x ↦ ∑ i, (f' x) (Pi.single i 1) i) BoxAdditiveMap.volume
    (∑ i,
      (integral (I.face i) GP (fun x ↦ f (i.insertNth (I.upper i) x) i) BoxAdditiveMap.volume -
        integral (I.face i) GP (fun x ↦ f (i.insertNth (I.lower i) x) i) BoxAdditiveMap.volume))

Tactic:
by

Goal state after: