-- 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.Ioo I \ s, HasFDerivAt f (f' x) x)
    (Hi : IntegrableOn (∑ i, f' · (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 intro.intro.intro.intro.intro
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.Ioo I \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume
J : ℕ →o Box (Fin (n + 1))
hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I
hJl : ∀ (x : Fin (n + 1)), Tendsto (fun i => (Box.lower ∘ ⇑J) i x) atTop (𝓝 (I.lower x))
hJu : ∀ (x : Fin (n + 1)), Tendsto (fun i => (Box.upper ∘ ⇑J) i x) atTop (𝓝 (I.upper x))
hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I
hJ_le : ∀ (k : ℕ), J k ≤ I
HcJ : ∀ (k : ℕ), ContinuousOn f (Box.Icc (J k))
HdJ : ∀ (k : ℕ), ∀ x ∈ Box.Icc (J k) \ s, HasFDerivWithinAt f (f' x) (Box.Icc (J k)) x
HiJ : ∀ (k : ℕ), IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc (J k)) volume
HJ_eq :
  ∀ (k : ℕ),
    ∫ (x : Fin (n + 1) → ℝ) in Box.Icc (J k), ∑ i : Fin (n + 1), (f' x) (e i) i =
      ∑ i : Fin (n + 1),
        ((∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).upper i) x) i) -
          ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).lower i) x) i)
i : Fin (n + 1)
c : ℕ → ℝ
d : ℝ
hc : ∀ (k : ℕ), c k ∈ Set.Icc (I.lower i) (I.upper i)
hcd : Tendsto c atTop (𝓝 d)
hd : d ∈ Set.Icc (I.lower i) (I.upper i)
Hic : ∀ (k : ℕ), IntegrableOn (fun x => f (i.insertNth (c k) x) i) (Box.Icc (I.face i)) volume
Hid : IntegrableOn (fun x => f (i.insertNth d x) i) (Box.Icc (I.face i)) volume
H :
  Tendsto (fun k => ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth d x) i) atTop
    (𝓝 (∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth d x) i))
ε : ℝ
εpos : 0 < ε
hvol_pos : ∀ (J : Box (Fin n)), 0 < ∏ j : Fin n, (J.upper j - J.lower j)
δ : ℝ
δpos : δ > 0
hδ :
  ∀ x ∈ Box.Icc I,
    ∀ y ∈ Box.Icc I, dist x y ≤ δ → dist (f x) (f y) ≤ ε / ∏ j : Fin n, ((I.face i).upper j - (I.face i).lower j)
k : ℕ
hk : dist (c k) d < δ
Hsub : Box.Icc ((J k).face i) ⊆ Box.Icc (I.face i)
⊢ ‖∫ (a : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth d a) i - f (i.insertNth (c k) a) i ∂volume‖ ≤ ε

Tactic:
calc
  ‖∫ x in Box.Icc ((J k).face i), f (i.insertNth d x) i - f (i.insertNth (c k) x) i‖ ≤
      (ε / ∏ j, ((I.face i).upper j - (I.face i).lower j)) *
        (volume (Box.Icc ((J k).face i))).toReal := by
    refine norm_setIntegral_le_of_norm_le_const' (((J k).face i).measure_Icc_lt_top _)
      ((J k).face i).measurableSet_Icc fun x hx => ?_
    rw [← dist_eq_norm]
    calc
      dist (f (i.insertNth d x) i) (f (i.insertNth (c k) x) i) ≤
          dist (f (i.insertNth d x)) (f (i.insertNth (c k) x)) :=
        dist_le_pi_dist (f (i.insertNth d x)) (f (i.insertNth (c k) x)) i
      _ ≤ ε / ∏ j, ((I.face i).upper j - (I.face i).lower j) :=
        hδ _ (I.mapsTo_insertNth_face_Icc hd <| Hsub hx) _
          (I.mapsTo_insertNth_face_Icc (hc _) <| Hsub hx) ?_
    rw [Fin.dist_insertNth_insertNth, dist_self, dist_comm]
    exact max_le hk.le δpos.lt.le
  _ ≤ ε := by
    rw [Box.Icc_def, Real.volume_Icc_pi_toReal ((J k).face i).lower_le_upper,
      ← le_div_iff₀ (hvol_pos _)]
    gcongr
    exacts [hvol_pos _, fun _ _ ↦ sub_nonneg.2 (Box.lower_le_upper _ _),
      (hJ_sub' _ (J _).upper_mem_Icc).2 _, (hJ_sub' _ (J _).lower_mem_Icc).1 _]

Result:
no goals