-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ 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.pi (α := fun (i : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦ Set.Ioo (a i) (b i)) \ s,
    HasFDerivAt (𝕜 := ℝ) f (f' x) x
Hi :
  IntegrableOn.{0, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : Fin (n + 1) → ℝ) ↦
      ∑ i : Fin (n + 1),
        (f' x : (a : Fin (n + 1) → ℝ) → Fin (n + 1) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) i)
    (Set.Icc a b) volume
inl :
  ∀ (i : Fin (n + 1)) (hi : a i = b i),
    Eq.{u + 1} (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b))
        fun (x : Fin (n + 1) → ℝ) ↦
        ∑ i : Fin (n + 1),
          (f' x : (a : Fin (n + 1) → ℝ) → Fin (n + 1) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) i)
      (∑ i : Fin (n + 1),
        HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
            (Measure.restrict volume (Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove))) fun (x : Fin n → ℝ) ↦
            f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (b i) x) i)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
            (Measure.restrict volume (Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove))) fun (x : Fin n → ℝ) ↦
            f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (a i) x) i))
inr :
  ∀ (hne : ¬∃ (i : Fin (n + 1)), a i = b i),
    Eq.{u + 1} (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b))
        fun (x : Fin (n + 1) → ℝ) ↦
        ∑ i : Fin (n + 1),
          (f' x : (a : Fin (n + 1) → ℝ) → Fin (n + 1) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) i)
      (∑ i : Fin (n + 1),
        HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
            (Measure.restrict volume (Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove))) fun (x : Fin n → ℝ) ↦
            f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (b i) x) i)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
            (Measure.restrict volume (Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove))) fun (x : Fin n → ℝ) ↦
            f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (a i) x) i))
⊢ Eq.{u + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b))
      fun (x : Fin (n + 1) → ℝ) ↦
      ∑ i : Fin (n + 1),
        (f' x : (a : Fin (n + 1) → ℝ) → Fin (n + 1) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) i)
    (∑ i : Fin (n + 1),
      HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume (Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove))) fun (x : Fin n → ℝ) ↦
          f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (b i) x) i)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume (Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove))) fun (x : Fin n → ℝ) ↦
          f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (a i) x) i))

Tactic:
rcases em (∃ i, a i = b i) with (⟨i, hi⟩ | hne)

Premises used: Exists, em, Eq