-- Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean
theorem integral_divergence_of_hasFDerivWithinAt_off_countable (hle : a ≤ b)
    (f : ℝⁿ⁺¹ → Eⁿ⁺¹)
    (f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹)
    (s : Set ℝⁿ⁺¹) (hs : s.Countable) (Hc : ContinuousOn f (Icc a b))
    (Hd : ∀ x ∈ (Set.pi univ fun i => Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x)
    (Hi : IntegrableOn (fun x => ∑ i, f' x (e i) i) (Icc a b)) :
    (∫ x in Icc a b, ∑ i, f' x (e i) i) =
      ∑ i : Fin (n + 1),
        ((∫ x in face i, f (frontFace i x) i) - ∫ x in face i, f (backFace i x) i)

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
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 (Set.Icc a b)
Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Set.Icc a b) volume
this : (Set.univ.pi fun j => Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
i : Fin n
hi : a (j.succAbove i) = b (j.succAbove i)
hi' : Set.Ioc (a (j.succAbove i)) (b (j.succAbove i)) = ∅
hne : j.succAbove i ≠ j
⊢ ENNReal.ofReal ((b ∘ j.succAbove) i - (a ∘ j.succAbove) i) = 0

Tactic:
simp [hi]

Result:
no goals

Proof state:
case inl.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
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 (Set.Icc a b)
Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Set.Icc a b) volume
i : Fin (n + 1)
hi : a i = b i
⊢ ∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i : Fin (n + 1), (f' x) (e i) i =
    ∑ i : Fin (n + 1),
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (a i) x) i)

Tactic:
rw [volume_pi, ← setIntegral_congr_set Measure.univ_pi_Ioc_ae_eq_Icc]

Result:
case inl.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
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 (Set.Icc a b)
Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Set.Icc a b) volume
i : Fin (n + 1)
hi : a i = b i
⊢ (∫ (x : Fin (n + 1) → ℝ) in Set.univ.pi fun i => Set.Ioc (a i) (b i),
      ∑ i : Fin (n + 1), (f' x) (e i) i ∂Measure.pi fun x => volume) =
    ∑ i : Fin (n + 1),
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (a i) x) i)

Proof state:
case inl.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
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 (Set.Icc a b)
Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Set.Icc a b) volume
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this : (Set.univ.pi fun j => Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
⊢ (∫ (x : Fin n → ℝ) in Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove), f (j.insertNth (b j) x) j) -
      ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove), f (j.insertNth (a j) x) j =
    0

Tactic:
rcases eq_or_ne i j with (rfl | hne)

Result:
case inl.intro.inl
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
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 (Set.Icc a b)
Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Set.Icc a b) volume
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this : (Set.univ.pi fun j => Set.Ioc (a j) (b j)) = ∅
⊢ (∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (b i) x) i) -
      ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (a i) x) i =
    0

case inl.intro.inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
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 (Set.Icc a b)
Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Set.Icc a b) volume
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this : (Set.univ.pi fun j => Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
hne : i ≠ j
⊢ (∫ (x : Fin n → ℝ) in Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove), f (j.insertNth (b j) x) j) -
      ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove), f (j.insertNth (a j) x) j =
    0

Proof state:
case inl.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
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 (Set.Icc a b)
Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Set.Icc a b) volume
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
⊢ (∫ (x : Fin (n + 1) → ℝ) in Set.univ.pi fun i => Set.Ioc (a i) (b i),
      ∑ i : Fin (n + 1), (f' x) (e i) i ∂Measure.pi fun x => volume) =
    ∑ i : Fin (n + 1),
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (a i) x) i)

Tactic:
have : (pi Set.univ fun j => Ioc (a j) (b j)) = ∅ := univ_pi_eq_empty hi'

Result:
case inl.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
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 (Set.Icc a b)
Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Set.Icc a b) volume
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this : (Set.univ.pi fun j => Set.Ioc (a j) (b j)) = ∅
⊢ (∫ (x : Fin (n + 1) → ℝ) in Set.univ.pi fun i => Set.Ioc (a i) (b i),
      ∑ i : Fin (n + 1), (f' x) (e i) i ∂Measure.pi fun x => volume) =
    ∑ i : Fin (n + 1),
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (a i) x) i)