Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case inr
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : 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 (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) volume
this :
  ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
    ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      (∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt f (f' x) x) →
        (∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max 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 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)
h₁ : ¬a₁ ≤ b₁
⊢ -∫ (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 (b₁, y)) -
      ∫ (y : ℝ) in a₂..b₂, f (a₁, y)

Tactic:
refine (congr_arg Neg.neg (this Hcf Hcg Hdf Hdg Hi (le_of_not_ge h₁))).trans ?_

Goal state after:
case inr
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : 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 (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) volume
this :
  ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
    ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      (∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt f (f' x) x) →
        (∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max 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 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)
h₁ : ¬a₁ ≤ b₁
⊢ -((((∫ (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 b₁..a₁, g (x, b₂)) - -∫ (x : ℝ) in b₁..a₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) -
      ∫ (y : ℝ) in a₂..b₂, f (a₁, y)