-- Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean
theorem integral_divergence_of_hasFDerivWithinAt_off_countable_aux₁ (I : Box (Fin (n + 1)))
    (f : ℝⁿ⁺¹ → Eⁿ⁺¹)
    (f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹) (s : Set ℝⁿ⁺¹)
    (hs : s.Countable) (Hc : ContinuousOn f (Box.Icc I))
    (Hd : ∀ x ∈ (Box.Icc I) \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x)
    (Hi : IntegrableOn (fun x => ∑ i, f' x (e i) i) (Box.Icc I)) :
    (∫ x in Box.Icc I, ∑ i, f' x (e i) i) =
      ∑ i : Fin (n + 1),
        ((∫ x in Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) -
          ∫ x in Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)

Proof state:
case refine_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
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
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y => f y i) (Box.Icc I)
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume
A :
  HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) volume.toBoxAdditive.toSMul
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), (f' x) (e i) i ∂volume)
B :
  HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      (BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x => f (i.insertNth (I.upper i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x => f (i.insertNth (I.lower i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
this✝ : ContinuousOn ((fun y => f y i) ∘ i.insertNth (I.lower i)) (Box.Icc (I.face i))
this : IntegrableOn ((fun y => f y i) ∘ i.insertNth (I.lower i)) (↑(I.face i)) volume
⊢ BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x => f (i.insertNth (I.lower i) x) i)
      BoxAdditiveMap.volume =
    ∫ (x : Fin n → ℝ) in ↑(I.face i), f (i.insertNth (I.lower i) x) i

Tactic:
exact (this.hasBoxIntegral ⊥ rfl).integral_eq

Result:
no goals

Proof state:
case refine_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
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
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y => f y i) (Box.Icc I)
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume
A :
  HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) volume.toBoxAdditive.toSMul
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), (f' x) (e i) i ∂volume)
B :
  HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      (BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x => f (i.insertNth (I.upper i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x => f (i.insertNth (I.lower i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x => f (i.insertNth (I.lower i) x) i)
      BoxAdditiveMap.volume =
    ∫ (x : Fin n → ℝ) in ↑(I.face i), f (i.insertNth (I.lower i) x) i

Tactic:
have := Box.continuousOn_face_Icc (Hc i) (Set.left_mem_Icc.2 (I.lower_le_upper i))

Result:
case refine_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
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
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y => f y i) (Box.Icc I)
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume
A :
  HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) volume.toBoxAdditive.toSMul
    (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), (f' x) (e i) i ∂volume)
B :
  HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) BoxAdditiveMap.volume
    (∑ i : Fin (n + 1),
      (BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x => f (i.insertNth (I.upper i) x) i)
          BoxAdditiveMap.volume -
        BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x => f (i.insertNth (I.lower i) x) i)
          BoxAdditiveMap.volume))
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
this : ContinuousOn ((fun y => f y i) ∘ i.insertNth (I.lower i)) (Box.Icc (I.face i))
⊢ BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x => f (i.insertNth (I.lower i) x) i)
      BoxAdditiveMap.volume =
    ∫ (x : Fin n → ℝ) in ↑(I.face i), f (i.insertNth (I.lower i) x) i

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
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
Hc : ContinuousOn f (Box.Icc I)
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume
⊢ ∫ (x : Fin (n + 1) → ℝ) in Box.Icc I, ∑ i : Fin (n + 1), (f' x) (e i) i =
    ∑ i : Fin (n + 1),
      ((∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) -
        ∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)

Tactic:
simp only [← setIntegral_congr_set (Box.coe_ae_eq_Icc _)]

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
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
Hc : ContinuousOn f (Box.Icc I)
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume
⊢ ∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), (f' x) (e i) i =
    ∑ x : Fin (n + 1),
      ((∫ (x_1 : Fin n → ℝ) in ↑(I.face x), f (x.insertNth (I.upper x) x_1) x) -
        ∫ (x_1 : Fin n → ℝ) in ↑(I.face x), f (x.insertNth (I.lower x) x_1) x)