-- 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:
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)
⊢ ‖integral (I.face i) ⊥
        (fun x => f' (Pi.single i (I.upper i - I.lower i)) - (f (e (I.upper i) x) - f (e (I.lower i) x)))
        BoxAdditiveMap.volume‖ ≤
    (volume ↑(I.face i)).toReal * (2 * ε * ↑c * (I.upper i - I.lower i))

Tactic:
refine norm_integral_le_of_le_const (fun y hy => (this y hy).trans ?_) volume

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)
y : Fin n → ℝ
hy : y ∈ Box.Icc (I.face i)
⊢ 2 * ε * diam (Box.Icc I) ≤ 2 * ε * ↑c * (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) → ℝ) → 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 : Fin (n + 1), (I.upper j - I.lower j)) • f' (Pi.single i 1) -
        (integral (I.face i) ⊥ (f ∘ i.insertNth (I.upper i)) BoxAdditiveMap.volume -
          integral (I.face i) ⊥ (f ∘ i.insertNth (I.lower i)) BoxAdditiveMap.volume)‖ ≤
    2 * ε * ↑c * ∏ j : Fin (n + 1), (I.upper j - I.lower j)

Tactic:
set e : ℝ → (Fin n → ℝ) → (Fin (n + 1) → ℝ) := i.insertNth (α := fun _ ↦ ℝ)

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
⊢ ‖(∏ j : Fin (n + 1), (I.upper j - I.lower j)) • f' (Pi.single i 1) -
        (integral (I.face i) ⊥ (f ∘ e (I.upper i)) BoxAdditiveMap.volume -
          integral (I.face i) ⊥ (f ∘ e (I.lower i)) BoxAdditiveMap.volume)‖ ≤
    2 * ε * ↑c * ∏ j : Fin (n + 1), (I.upper j - I.lower j)

Proof state:
case h.e'_3
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)
⊢ ‖f' (Pi.single i (I.upper i - I.lower i)) -
        ((fun y => a + f' (y - x) + g y) (e (I.upper i) y) - (fun y => a + f' (y - x) + g y) (e (I.lower i) y))‖ =
    ‖g (e (I.lower i) y) - g (e (I.upper i) y)‖

Tactic:
congr 1

Result:
case h.e'_3.e_a
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)
⊢ f' (Pi.single i (I.upper i - I.lower i)) -
      ((fun y => a + f' (y - x) + g y) (e (I.upper i) y) - (fun y => a + f' (y - x) + g y) (e (I.lower i) y)) =
    g (e (I.lower i) y) - g (e (I.upper i) y)