-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ 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 (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ 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))
    ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) volume
h₁ : a₁ ≤ b₁
this :
  ∀ (a₂ b₂ : ℝ) (Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])) (Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]))
    (Hdf : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt f (f' x) x)
    (Hdg : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ 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))
        ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) volume)
    (h₂ : a₂ ≤ b₂),
    ∫ (x : ℝ) in a₁..b₁,
        ∫ (y : ℝ) in a₂..b₂,
          HAdd.hAdd (α := E) (β := E) ((f' (x, y) : (a : ℝ × ℝ) → E) (1, 0) : E)
            ((g' (x, y) : (a : ℝ × ℝ) → E) (0, 1) : E) =
      (HSub.hSub (α := E) (∫ (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₂,
        HAdd.hAdd (α := E) (β := E) ((f' (x, y) : (a : ℝ × ℝ) → E) (1, 0) : E)
          ((g' (x, y) : (a : ℝ × ℝ) → E) (0, 1) : E) =
    (HSub.hSub (α := E) (∫ (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)
have this₁ : ∀ (Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[b₂, a₂]])) (Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[b₂, a₂]]))
  (Hdf : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min b₂ a₂) (max b₂ a₂) \ s, HasFDerivAt f (f' x) x)
  (Hdg : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min b₂ a₂) (max b₂ a₂) \ 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))
      ([[a₁, b₁]] ×ˢ [[b₂, a₂]]) volume)
  (h₂ : b₂ ≤ a₂),
  ∫ (x : ℝ) in a₁..b₁,
      ∫ (y : ℝ) in b₂..a₂,
        HAdd.hAdd (α := E) (β := E) ((f' (x, y) : (a : ℝ × ℝ) → E) (1, 0) : E)
          ((g' (x, y) : (a : ℝ × ℝ) → E) (0, 1) : E) =
    (HSub.hSub (α := E) (∫ (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)
Tactic: specialize this b₂ a₂
Cleared hypotheses: this