-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
x : Fin (n + 1) → ℝ
hxI :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) x
a : E
ε : ℝ
h0 : 0 < ε
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ)
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 :
  Membership.mem (γ := Set (Fin n → ℝ)) ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i) : Set (Fin n → ℝ)) y
g : (y : Fin (n + 1) → ℝ) → E
hε :
  ∀ (y : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) y →
      ‖g y‖ ≤ ε * ‖y - x‖
hfc :
  ContinuousOn.{0, u} (Y := E)
    (fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y)
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
Hi :
  ∀ x_1 ∈ Set.Icc (I.lower i) (I.upper i),
    Integrable.{0, u, u} (E := E) (I.face i) ⊥
      ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y) ∘ e x_1)
      BoxAdditiveMap.volume
hg :
  g = fun (y : Fin (n + 1) → ℝ) ↦
    HSub.hSub (β := E)
      ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y) y - a)
      ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)
this :
  HSub.hSub (α := (j : Fin (n + 1)) → ℝ) (i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ) (I.upper i) y)
      (i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ) (I.lower i) y) =
    Pi.single (M := fun (x : Fin (n + 1)) ↦ ℝ) i (I.upper i - I.lower i)
h :
  HSub.hSub (α := E) (β := E)
        ((f' : (a : Fin (n + 1) → ℝ) → E) (i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ) (I.upper i) y) : E)
        ((f' : (a : Fin (n + 1) → ℝ) → E) (i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ) (I.lower i) y) : E) -
      (a +
            HSub.hSub (α := E) (β := E) ((f' : (a : Fin (n + 1) → ℝ) → E) (e (I.upper i) y) : E)
              ((f' : (a : Fin (n + 1) → ℝ) → E) x : E) +
          g (e (I.upper i) y) -
        (a +
            HSub.hSub (α := E) (β := E) ((f' : (a : Fin (n + 1) → ℝ) → E) (e (I.lower i) y) : E)
              ((f' : (a : Fin (n + 1) → ℝ) → E) x : E) +
          g (e (I.lower i) y))) =
    g (e (I.lower i) y) - g (e (I.upper i) y)
⊢ HSub.hSub (α := E)
      ((f' : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i (I.upper i - I.lower i)) : E)
      (HSub.hSub (α := E)
        ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y)
          (e (I.upper i) y))
        ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y)
          (e (I.lower i) y))) =
    g (e (I.lower i) y) - g (e (I.upper i) y)

Tactic:
simp only [← this, f'.map_sub]

Premises used: ContinuousLinearMap.map_sub