-- Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean
theorem norm_volume_sub_integral_face_upper_sub_lower_smul_le {f : (Fin (n + 1) → ℝ) → E}
    {f' : (Fin (n + 1) → ℝ) →L[ℝ] E} (hfc : ContinuousOn f (Box.Icc I)) {x : Fin (n + 1) → ℝ}
    (hxI : x ∈ (Box.Icc I)) {a : E} {ε : ℝ} (h0 : 0 < ε)
    (hε : ∀ y ∈ (Box.Icc I), ‖f y - a - f' (y - x)‖ ≤ ε * ‖y - x‖) {c : ℝ≥0}
    (hc : I.distortion ≤ c) :
    ‖(∏ j, (I.upper j - I.lower j)) • f' (Pi.single i 1) -
      (integral (I.face i) ⊥ (f ∘ i.insertNth (α := fun _ ↦ ℝ) (I.upper i)) BoxAdditiveMap.volume -
        integral (I.face i) ⊥ (f ∘ i.insertNth (α := fun _ ↦ ℝ) (I.lower i))
          BoxAdditiveMap.volume)‖ ≤
      2 * ε * c * ∏ j, (I.upper j - I.lower j)

Proof state:
case convert_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
y : Fin n → ℝ
hy : y ∈ Box.Icc (I.face i)
g : (Fin (n + 1) → ℝ) → E
hfc : ContinuousOn (fun y => a + f' (y - x) + g y) (Box.Icc I)
Hi :
  ∀ x_1 ∈ Set.Icc (I.lower i) (I.upper i),
    Integrable (I.face i) ⊥ ((fun y => a + f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y => (fun y => a + f' (y - x) + g y) y - a - f' (y - x)
this : ∀ z ∈ Set.Icc (I.lower i) (I.upper i), e z y ∈ Box.Icc I
hε : ∀ y ∈ Box.Icc I, ‖g y‖ ≤ ε * diam (Box.Icc I)
⊢ ‖g (e (I.lower i) y) - g (e (I.upper i) y)‖ ≤ ε * diam (Box.Icc I) + ε * diam (Box.Icc I)

Tactic:
exact norm_sub_le_of_le (hε _ (this _ Hl)) (hε _ (this _ Hu))

Result:
no goals

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
hε : ∀ y ∈ Box.Icc I, ‖f y - a - f' (y - x)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
Hi : ∀ x ∈ Set.Icc (I.lower i) (I.upper i), Integrable (I.face i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
this :
  ∀ y ∈ Box.Icc (I.face i),
    ‖f' (Pi.single i (I.upper i - I.lower i)) - (f (e (I.upper i) y) - f (e (I.lower i) y))‖ ≤ 2 * ε * diam (Box.Icc I)
⊢ (volume ↑(I.face i)).toReal * (2 * ε * ↑c * (I.upper i - I.lower i)) =
    2 * ε * ↑c * ∏ j : Fin (n + 1), (I.upper j - I.lower j)

Tactic:
rw [← Measure.toBoxAdditive_apply, Box.volume_apply, ← I.volume_face_mul i]

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
hε : ∀ y ∈ Box.Icc I, ‖f y - a - f' (y - x)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
Hi : ∀ x ∈ Set.Icc (I.lower i) (I.upper i), Integrable (I.face i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
this :
  ∀ y ∈ Box.Icc (I.face i),
    ‖f' (Pi.single i (I.upper i - I.lower i)) - (f (e (I.upper i) y) - f (e (I.lower i) y))‖ ≤ 2 * ε * diam (Box.Icc I)
⊢ (∏ i_1 : Fin n, ((I.face i).upper i_1 - (I.face i).lower i_1)) * (2 * ε * ↑c * (I.upper i - I.lower i)) =
    2 * ε * ↑c * ((∏ j : Fin n, ((I.face i).upper j - (I.face i).lower j)) * (I.upper i - I.lower i))

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
y✝ : Fin n → ℝ
hy✝ : y✝ ∈ Box.Icc (I.face i)
g : (Fin (n + 1) → ℝ) → E
hε : ∀ y ∈ Box.Icc I, ‖g y‖ ≤ ε * ‖y - x‖
hfc : ContinuousOn (fun y => a + f' (y - x) + g y) (Box.Icc I)
Hi :
  ∀ x_1 ∈ Set.Icc (I.lower i) (I.upper i),
    Integrable (I.face i) ⊥ ((fun y => a + f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y => (fun y => a + f' (y - x) + g y) y - a - f' (y - x)
this : ∀ z ∈ Set.Icc (I.lower i) (I.upper i), e z y✝ ∈ Box.Icc I
y : Fin (n + 1) → ℝ
hy : y ∈ Box.Icc I
⊢ ‖y - x‖ ≤ diam (Box.Icc I)

Tactic:
rw [← dist_eq_norm]

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI : x ∈ Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
y✝ : Fin n → ℝ
hy✝ : y✝ ∈ Box.Icc (I.face i)
g : (Fin (n + 1) → ℝ) → E
hε : ∀ y ∈ Box.Icc I, ‖g y‖ ≤ ε * ‖y - x‖
hfc : ContinuousOn (fun y => a + f' (y - x) + g y) (Box.Icc I)
Hi :
  ∀ x_1 ∈ Set.Icc (I.lower i) (I.upper i),
    Integrable (I.face i) ⊥ ((fun y => a + f' (y - x) + g y) ∘ e x_1) BoxAdditiveMap.volume
hg : g = fun y => (fun y => a + f' (y - x) + g y) y - a - f' (y - x)
this : ∀ z ∈ Set.Icc (I.lower i) (I.upper i), e z y✝ ∈ Box.Icc I
y : Fin (n + 1) → ℝ
hy : y ∈ Box.Icc I
⊢ dist y x ≤ diam (Box.Icc I)