-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a b : ℝ × ℝ
hle : a ≤ b
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f (Set.Icc a b)
Hcg : ContinuousOn g (Set.Icc a b)
Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x
Hi :
  IntegrableOn.{0, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ × ℝ) ↦
      HAdd.hAdd (α := E) (β := E) ((f' x : (a : ℝ × ℝ) → E) (1, 0) : E) ((g' x : (a : ℝ × ℝ) → E) (0, 1) : E))
    (Set.Icc a b) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := ContinuousLinearEquiv.symm (ContinuousLinearEquiv.finTwoArrow ℝ ℝ)
this :
  ∀ (a b : Fin 1 → ℝ) (f : (Fin 1 → ℝ) → E),
    Eq.{u + 1} (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b)) fun (x : Fin 1 → ℝ) ↦
        f x)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc (a 0) (b 0))) fun (x : ℝ) ↦
        f fun (x_1 : Fin 1) ↦ x)
⊢ ∑ i : Fin 2,
      HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume
            (Set.Icc ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) a ∘ i.succAbove) ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) b ∘ i.succAbove)))
          fun (x : Fin 1 → ℝ) ↦
          ![f, g] i
            ((e.symm : (a : Fin 2 → ℝ) → ℝ × ℝ)
              (i.insertNth (α := fun (a : Fin 2) ↦ ℝ) ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) b i) x)))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume
            (Set.Icc ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) a ∘ i.succAbove) ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) b ∘ i.succAbove)))
          fun (x : Fin 1 → ℝ) ↦
          ![f, g] i
            ((e.symm : (a : Fin 2 → ℝ) → ℝ × ℝ)
              (i.insertNth (α := fun (a : Fin 2) ↦ ℝ) ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) a i) x))) =
    HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.2 b.2)) fun (y : ℝ) ↦
          f (b.1, y))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.2 b.2)) fun (y : ℝ) ↦
          f (a.1, y)) +
      HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.1 b.1)) fun (x : ℝ) ↦
          g (x, b.2))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.1 b.1)) fun (x : ℝ) ↦
          g (x, a.2))
have simp : HSub.hSub (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume
          (Set.Icc (comp (α := Fin 1) ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) a) (Fin.succAbove 0) 0)
            (comp (α := Fin 1) ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) b) (Fin.succAbove 0) 0)))
        fun (x : ℝ) ↦
        ![f, g] 0
          ((e.symm : (a : Fin 2 → ℝ) → ℝ × ℝ)
            (Fin.insertNth (α := fun (a : Fin 2) ↦ ℝ) 0 ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) b 0) fun (x_1 : Fin 1) ↦ x)))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume
          (Set.Icc (comp (α := Fin 1) ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) a) (Fin.succAbove 0) 0)
            (comp (α := Fin 1) ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) b) (Fin.succAbove 0) 0)))
        fun (x : ℝ) ↦
        ![f, g] 0
          ((e.symm : (a : Fin 2 → ℝ) → ℝ × ℝ)
            (Fin.insertNth (α := fun (a : Fin 2) ↦ ℝ) 0 ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) a 0) fun (x_1 : Fin 1) ↦ x))) +
    HSub.hSub (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume
          (Set.Icc (comp (α := Fin 1) ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) a) (Fin.succAbove 1) 0)
            (comp (α := Fin 1) ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) b) (Fin.succAbove 1) 0)))
        fun (x : ℝ) ↦
        ![f, g] 1
          ((e.symm : (a : Fin 2 → ℝ) → ℝ × ℝ)
            (Fin.insertNth (α := fun (a : Fin 2) ↦ ℝ) 1 ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) b 1) fun (x_1 : Fin 1) ↦ x)))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
        (Measure.restrict volume
          (Set.Icc (comp (α := Fin 1) ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) a) (Fin.succAbove 1) 0)
            (comp (α := Fin 1) ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) b) (Fin.succAbove 1) 0)))
        fun (x : ℝ) ↦
        ![f, g] 1
          ((e.symm : (a : Fin 2 → ℝ) → ℝ × ℝ)
            (Fin.insertNth (α := fun (a : Fin 2) ↦ ℝ) 1 ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) a 1) fun (x_1 : Fin 1) ↦ x))) =
  HSub.hSub (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.2 b.2)) fun (y : ℝ) ↦
        f (b.1, y))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.2 b.2)) fun (y : ℝ) ↦
        f (a.1, y)) +
    HSub.hSub (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.1 b.1)) fun (x : ℝ) ↦
        g (x, b.2))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.1 b.1)) fun (x : ℝ) ↦
        g (x, a.2))
Tactic: simp only [Fin.sum_univ_two, this]