-- Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean
theorem hasIntegral_GP_divergence_of_forall_hasDerivWithinAt
    (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.{0, u, u} I GP (fun x => ∑ i, f' x (Pi.single i 1) i) BoxAdditiveMap.volume
      (∑ i,
        (integral.{0, u, u} (I.face i) GP (fun x => f (i.insertNth (I.upper i) x) i)
            BoxAdditiveMap.volume -
          integral.{0, u, u} (I.face i) GP (fun x => f (i.insertNth (I.lower i) x) i)
            BoxAdditiveMap.volume))

Proof state:
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
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ HasIntegral I GP (fun x => (f' x) (Pi.single i 1) i) BoxAdditiveMap.volume
    (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:
simp only [hasFDerivWithinAt_pi', continuousWithinAt_pi] at Hd Hs

Result:
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
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
Hd :
  ∀ x ∈ Box.Icc I \ s,
    ∀ (i : Fin (n + 1)), HasFDerivWithinAt (fun x => f x i) ((ContinuousLinearMap.proj i).comp (f' x)) (Box.Icc I) x
Hs : ∀ x ∈ s, ∀ (i : Fin (n + 1)), ContinuousWithinAt (fun y => f y i) (Box.Icc I) x
⊢ HasIntegral I GP (fun x => (f' x) (Pi.single i 1) i) BoxAdditiveMap.volume
    (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)

Proof state:
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
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
Hd :
  ∀ x ∈ Box.Icc I \ s,
    ∀ (i : Fin (n + 1)), HasFDerivWithinAt (fun x => f x i) ((ContinuousLinearMap.proj i).comp (f' x)) (Box.Icc I) x
Hs : ∀ x ∈ s, ∀ (i : Fin (n + 1)), ContinuousWithinAt (fun y => f y i) (Box.Icc I) x
⊢ HasIntegral I GP (fun x => (f' x) (Pi.single i 1) i) BoxAdditiveMap.volume
    (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:
exact hasIntegral_GP_pderiv I _ _ s hs (fun x hx => Hs x hx i) (fun x hx => Hd x hx i) i

Result:
no goals

Proof state:
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 : Fin (n + 1), (f' x) (Pi.single i 1) i) BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      (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:
refine HasIntegral.sum fun i _ => ?_

Result:
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
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ HasIntegral I GP (fun x => (f' x) (Pi.single i 1) i) BoxAdditiveMap.volume
    (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)