-- 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))
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 : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
Hd :
  ∀ (x : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      HasFDerivWithinAt f (f' x) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
i : Fin (n + 1)
Hc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
fI : ℝ → Box (Fin n) → E :=
  fun (y : ℝ) (J : Box (Fin n)) ↦
    integral J GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) y x)) BoxAdditiveMap.volume
fb : (↑(Set.Icc (I.lower i) (I.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I.face i) : WithTop (Box (Fin n)))] E :=
  fun (x : (↑(Set.Icc (I.lower i) (I.upper i)) : Type)) ↦
    Integrable.toBoxAdditive (vol := BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) ⋯
F : Fin (n + 1) →ᵇᵃ[(↑I : WithTop (Box (Fin (n + 1))))] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
refine_1 : Fin (n + 1) →ᵇᵃ[(↑I : WithTop (Box (Fin (n + 1))))] ℝ
refine_2 :
  ∀ (J : Box (Fin (n + 1))),
    LE.le (α := ℝ) (0 : ℝ)
      ((BoxAdditiveMap.restrict (Measure.toBoxAdditive volume) (↑I : WithTop (Box (Fin (n + 1)))) ⋯ :
            (a : Box (Fin (n + 1))) → ℝ)
          J :
        ℝ)
refine_3 :
  ∀ (c : ℝ≥0) (x : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I ∩ s : Set (Fin (n + 1) → ℝ)) x →
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) J ⊆ closedBall x δ →
              Membership.mem (γ := Set (Fin (n + 1) → ℝ))
                  ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) J : Set (Fin (n + 1) → ℝ)) x →
                (GP.bDistortion = true → J.distortion ≤ c) →
                  dist (α := E)
                      ((((BoxAdditiveMap.volume : (a : Box (Fin (n + 1))) → E →L[ℝ] E) J : E →L[ℝ] E) : (a : E) → E)
                          ((f' x : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : E) :
                        E)
                      ((F : (a : Box (Fin (n + 1))) → E) J : E) ≤
                    ε
refine_4 :
  ∀ (c : ℝ≥0) (x : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            (Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) J ⊆ closedBall x δ →
              Membership.mem (γ := Set (Fin (n + 1) → ℝ))
                  ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) J : Set (Fin (n + 1) → ℝ)) x →
                (GP.bDistortion = true → J.distortion ≤ c) →
                  dist (α := E)
                      ((((BoxAdditiveMap.volume : (a : Box (Fin (n + 1))) → E →L[ℝ] E) J : E →L[ℝ] E) : (a : E) → E)
                          ((f' x : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : E) :
                        E)
                      ((F : (a : Box (Fin (n + 1))) → E) J : E) ≤
                    HMul.hMul (β := ℝ) ε
                      ((BoxAdditiveMap.restrict (Measure.toBoxAdditive volume) (↑I : WithTop (Box (Fin (n + 1)))) ⋯ :
                            (a : Box (Fin (n + 1))) → ℝ)
                          J :
                        ℝ)
⊢ HasIntegral (E := E) (F := E) I GP
    (fun (x : Fin (n + 1) → ℝ) ↦
      ((f' x : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : E))
    (BoxAdditiveMap.volume : Fin (n + 1) →ᵇᵃ[⊤] E →L[ℝ] E) ((F : (a : Box (Fin (n + 1))) → E) I : E)

Tactic:
refine HasIntegral.of_le_Henstock_of_forall_isLittleO gp_le ?_ ?_ _ s hs ?_ ?_

Premises used: BoxIntegral.IntegrationParams.gp_le, BoxIntegral.HasIntegral.of_le_Henstock_of_forall_isLittleO