-- Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean
theorem integral2_divergence_prod_of_hasFDerivWithinAt_off_countable (f g : ℝ × ℝ → E)
    (f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E) (a₁ a₂ b₁ b₂ : ℝ) (s : Set (ℝ × ℝ)) (hs : s.Countable)
    (Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]))
    (Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]))
    (Hdf : ∀ x ∈ Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Ioo (min a₂ b₂) (max a₂ b₂) \ s,
      HasFDerivAt f (f' x) x)
    (Hdg : ∀ x ∈ Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Ioo (min a₂ b₂) (max a₂ b₂) \ s,
      HasFDerivAt g (g' x) x)
    (Hi : IntegrableOn (fun x => f' x (1, 0) + g' x (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]])) :
    (∫ x in a₁..b₁, ∫ y in a₂..b₂, f' (x, y) (1, 0) + g' (x, y) (0, 1)) =
      (((∫ x in a₁..b₁, g (x, b₂)) - ∫ x in a₁..b₁, g (x, a₂)) + ∫ y in a₂..b₂, f (b₁, y)) -
        ∫ y in a₂..b₂, f (a₁, y)

Proof state:
case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a₂ b₂ : ℝ
s : Set (ℝ × ℝ)
hs : s.Countable
a₁ b₁ : ℝ
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ x ∈ Set.Ioo (a₁ ⊓ b₁) (a₁ ⊔ b₁) ×ˢ Set.Ioo (a₂ ⊓ b₂) (a₂ ⊔ b₂) \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo (a₁ ⊓ b₁) (a₁ ⊔ b₁) ×ˢ Set.Ioo (a₂ ⊓ b₂) (a₂ ⊔ b₂) \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) volume
h₁ : a₁ ≤ b₁
h₂ : ¬a₂ ≤ b₂
this :
  ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
    ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      (∀ x ∈ Set.Ioo (a₁ ⊓ b₁) (a₁ ⊔ b₁) ×ˢ Set.Ioo (a₂ ⊓ b₂) (a₂ ⊔ b₂) \ s, HasFDerivAt f (f' x) x) →
        (∀ x ∈ Set.Ioo (a₁ ⊓ b₁) (a₁ ⊔ b₁) ×ˢ Set.Ioo (a₂ ⊓ b₂) (a₂ ⊔ b₂) \ s, HasFDerivAt g (g' x) x) →
          IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) volume →
            b₂ ≤ a₂ →
              ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in b₂..a₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) =
                (((∫ (x : ℝ) in a₁..b₁, g (x, a₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, b₂)) + ∫ (y : ℝ) in b₂..a₂, f (b₁, y)) -
                  ∫ (y : ℝ) in b₂..a₂, f (a₁, y)
⊢ ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) =
    (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) -
      ∫ (y : ℝ) in a₂..b₂, f (a₁, y)

Tactic:
simp only [intervalIntegral.integral_symm b₂ a₂, intervalIntegral.integral_neg]

Result:
case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a₂ b₂ : ℝ
s : Set (ℝ × ℝ)
hs : s.Countable
a₁ b₁ : ℝ
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ x ∈ Set.Ioo (a₁ ⊓ b₁) (a₁ ⊔ b₁) ×ˢ Set.Ioo (a₂ ⊓ b₂) (a₂ ⊔ b₂) \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo (a₁ ⊓ b₁) (a₁ ⊔ b₁) ×ˢ Set.Ioo (a₂ ⊓ b₂) (a₂ ⊔ b₂) \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) volume
h₁ : a₁ ≤ b₁
h₂ : ¬a₂ ≤ b₂
this :
  ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
    ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      (∀ x ∈ Set.Ioo (a₁ ⊓ b₁) (a₁ ⊔ b₁) ×ˢ Set.Ioo (a₂ ⊓ b₂) (a₂ ⊔ b₂) \ s, HasFDerivAt f (f' x) x) →
        (∀ x ∈ Set.Ioo (a₁ ⊓ b₁) (a₁ ⊔ b₁) ×ˢ Set.Ioo (a₂ ⊓ b₂) (a₂ ⊔ b₂) \ s, HasFDerivAt g (g' x) x) →
          IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) volume →
            b₂ ≤ a₂ →
              ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in b₂..a₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) =
                (((∫ (x : ℝ) in a₁..b₁, g (x, a₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, b₂)) + ∫ (y : ℝ) in b₂..a₂, f (b₁, y)) -
                  ∫ (y : ℝ) in b₂..a₂, f (a₁, y)
⊢ -∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in b₂..a₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) =
    (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + -∫ (y : ℝ) in b₂..a₂, f (b₁, y)) -
      -∫ (y : ℝ) in b₂..a₂, f (a₁, y)

Proof state:
case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a₁ a₂ b₁ b₂ : ℝ
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ x ∈ Set.Ioo (a₁ ⊓ b₁) (a₁ ⊔ b₁) ×ˢ Set.Ioo (a₂ ⊓ b₂) (a₂ ⊔ b₂) \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo (a₁ ⊓ b₁) (a₁ ⊔ b₁) ×ˢ Set.Ioo (a₂ ⊓ b₂) (a₂ ⊔ b₂) \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) volume
this :
  ∀ (a₁ b₁ : ℝ),
    ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
        (∀ x ∈ Set.Ioo (a₁ ⊓ b₁) (a₁ ⊔ b₁) ×ˢ Set.Ioo (a₂ ⊓ b₂) (a₂ ⊔ b₂) \ s, HasFDerivAt f (f' x) x) →
          (∀ x ∈ Set.Ioo (a₁ ⊓ b₁) (a₁ ⊔ b₁) ×ˢ Set.Ioo (a₂ ⊓ b₂) (a₂ ⊔ b₂) \ s, HasFDerivAt g (g' x) x) →
            IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) volume →
              a₁ ≤ b₁ →
                ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) =
                  (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) +
                      ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) -
                    ∫ (y : ℝ) in a₂..b₂, f (a₁, y)
h₁ : ¬a₁ ≤ b₁
⊢ ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) =
    (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) -
      ∫ (y : ℝ) in a₂..b₂, f (a₁, y)

Tactic:
specialize this b₁ a₁

Result:
case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a₁ a₂ b₁ b₂ : ℝ
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ x ∈ Set.Ioo (a₁ ⊓ b₁) (a₁ ⊔ b₁) ×ˢ Set.Ioo (a₂ ⊓ b₂) (a₂ ⊔ b₂) \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo (a₁ ⊓ b₁) (a₁ ⊔ b₁) ×ˢ Set.Ioo (a₂ ⊓ b₂) (a₂ ⊔ b₂) \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) volume
h₁ : ¬a₁ ≤ b₁
this :
  ContinuousOn f ([[b₁, a₁]] ×ˢ [[a₂, b₂]]) →
    ContinuousOn g ([[b₁, a₁]] ×ˢ [[a₂, b₂]]) →
      (∀ x ∈ Set.Ioo (b₁ ⊓ a₁) (b₁ ⊔ a₁) ×ˢ Set.Ioo (a₂ ⊓ b₂) (a₂ ⊔ b₂) \ s, HasFDerivAt f (f' x) x) →
        (∀ x ∈ Set.Ioo (b₁ ⊓ a₁) (b₁ ⊔ a₁) ×ˢ Set.Ioo (a₂ ⊓ b₂) (a₂ ⊔ b₂) \ s, HasFDerivAt g (g' x) x) →
          IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) ([[b₁, a₁]] ×ˢ [[a₂, b₂]]) volume →
            b₁ ≤ a₁ →
              ∫ (x : ℝ) in b₁..a₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) =
                (((∫ (x : ℝ) in b₁..a₁, g (x, b₂)) - ∫ (x : ℝ) in b₁..a₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (a₁, y)) -
                  ∫ (y : ℝ) in a₂..b₂, f (b₁, y)
⊢ ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) =
    (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) -
      ∫ (y : ℝ) in a₂..b₂, f (a₁, y)