-- 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₁ 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 (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
inr :
  ∀
    (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)
⊢ ∫ (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 wlog : ∀ (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)
Tactic: wlog h₁ : a₁ ≤ b₁ generalizing a₁ b₁
Cleared hypotheses: a₁, b₁, Hcf, Hcg, Hdf, Hdg, Hi