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 : Set.Countable s
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
this :
  ∀ (a₁ b₁ : ℝ),
    ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
        (∀ (x : ℝ × ℝ),
            x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s → HasFDerivAt f (f' x) 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₂]]) →
              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)

E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a₂ b₂ : ℝ
s : Set (ℝ × ℝ)
hs : Set.Countable s
a₁ b₁ : ℝ
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
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)
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 : Set.Countable s
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
⊢ (∫ (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)
wlog h₁ : a₁ ≤ b₁ generalizing a₁ b₁
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 : Set.Countable s
a₁ b₁ : ℝ
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
h₁ : a₁ ≤ b₁
this :
  ∀ (a₂ b₂ : ℝ),
    ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
        (∀ (x : ℝ × ℝ),
            x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s → HasFDerivAt f (f' x) 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₂]]) →
              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)

E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : Set.Countable s
a₁ b₁ : ℝ
h₁ : a₁ ≤ b₁
a₂ b₂ : ℝ
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
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)
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a₂ b₂ : ℝ
s : Set (ℝ × ℝ)
hs : Set.Countable s
a₁ b₁ : ℝ
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
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)
wlog h₂ : a₂ ≤ b₂ generalizing a₂ b₂
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : Set.Countable s
a₁ b₁ : ℝ
h₁ : a₁ ≤ b₁
a₂ b₂ : ℝ
h₂ : a₂ ≤ b₂
Hcf : ContinuousOn f (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)
Hcg : ContinuousOn g (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)
Hdf : ∀ (x : ℝ × ℝ), x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s → HasFDerivAt f (f' x) x
Hdg : ∀ (x : ℝ × ℝ), x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s → HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x => ↑(f' x) (1, 0) + ↑(g' x) (0, 1)) (Set.Icc a₁ b₁ ×ˢ Set.Icc 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)
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : Set.Countable s
a₁ b₁ : ℝ
h₁ : a₁ ≤ b₁
a₂ b₂ : ℝ
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
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)
simp only [uIcc_of_le h₁, uIcc_of_le h₂, min_eq_left, max_eq_right, h₁, h₂] at Hcf Hcg Hdf Hdg Hi
no goals
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : Set.Countable s
a₁ b₁ : ℝ
h₁ : a₁ ≤ b₁
a₂ b₂ : ℝ
h₂ : a₂ ≤ b₂
Hcf : ContinuousOn f (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)
Hcg : ContinuousOn g (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)
Hdf : ∀ (x : ℝ × ℝ), x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s → HasFDerivAt f (f' x) x
Hdg : ∀ (x : ℝ × ℝ), x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s → HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x => ↑(f' x) (1, 0) + ↑(g' x) (0, 1)) (Set.Icc a₁ b₁ ×ˢ Set.Icc 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)
calc
  (∫ x in a₁..b₁, ∫ y in a₂..b₂, f' (x, y) (1, 0) + g' (x, y) (0, 1)) =
      ∫ x in Icc a₁ b₁, ∫ y in Icc a₂ b₂, f' (x, y) (1, 0) + g' (x, y) (0, 1) := by
    simp only [intervalIntegral.integral_of_le, h₁, h₂,
      set_integral_congr_set_ae (Ioc_ae_eq_Icc (α := ℝ) (μ := volume))]
  _ = ∫ x in Icc a₁ b₁ ×ˢ Icc a₂ b₂, f' x (1, 0) + g' x (0, 1) := (set_integral_prod _ Hi).symm
  _ = (((∫ 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) := by
    rw [Icc_prod_Icc] at *
    apply integral_divergence_prod_Icc_of_hasFDerivWithinAt_off_countable_of_le f g f' g'
      (a₁, a₂) (b₁, b₂) ⟨h₁, h₂⟩ s <;> assumption
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 : Set.Countable s
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
h₁ : ¬a₁ ≤ b₁
this :
  ContinuousOn f ([[b₁, a₁]] ×ˢ [[a₂, b₂]]) →
    ContinuousOn g ([[b₁, a₁]] ×ˢ [[a₂, b₂]]) →
      (∀ (x : ℝ × ℝ),
          x ∈ Set.Ioo (min b₁ a₁) (max b₁ a₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s → HasFDerivAt f (f' x) x) →
        (∀ (x : ℝ × ℝ),
            x ∈ Set.Ioo (min b₁ a₁) (max b₁ a₁) ×ˢ 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)) ([[b₁, a₁]] ×ˢ [[a₂, b₂]]) →
            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)
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 : Set.Countable s
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
this :
  ∀ (a₁ b₁ : ℝ),
    ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
        (∀ (x : ℝ × ℝ),
            x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s → HasFDerivAt f (f' x) 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₂]]) →
              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)
specialize this b₁ a₁
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 : Set.Countable s
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
h₁ : ¬a₁ ≤ b₁
this :
  ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
    ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      (∀ (x : ℝ × ℝ),
          x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s → HasFDerivAt f (f' x) 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₂]]) →
            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)
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 : Set.Countable s
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
h₁ : ¬a₁ ≤ b₁
this :
  ContinuousOn f ([[b₁, a₁]] ×ˢ [[a₂, b₂]]) →
    ContinuousOn g ([[b₁, a₁]] ×ˢ [[a₂, b₂]]) →
      (∀ (x : ℝ × ℝ),
          x ∈ Set.Ioo (min b₁ a₁) (max b₁ a₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s → HasFDerivAt f (f' x) x) →
        (∀ (x : ℝ × ℝ),
            x ∈ Set.Ioo (min b₁ a₁) (max b₁ a₁) ×ˢ 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)) ([[b₁, a₁]] ×ˢ [[a₂, b₂]]) →
            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)
rw [uIcc_comm b₁ a₁, min_comm b₁ a₁, max_comm b₁ a₁] at this
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 : Set.Countable s
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
h₁ : ¬a₁ ≤ b₁
this :
  ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
    ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      (∀ (x : ℝ × ℝ),
          x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s → HasFDerivAt f (f' x) 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₂]]) →
            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 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)
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 : Set.Countable s
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
h₁ : ¬a₁ ≤ b₁
this :
  ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
    ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      (∀ (x : ℝ × ℝ),
          x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s → HasFDerivAt f (f' x) 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₂]]) →
            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)
simp only [intervalIntegral.integral_symm b₁ a₁]
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 : Set.Countable s
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
h₁ : ¬a₁ ≤ b₁
this :
  ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
    ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      (∀ (x : ℝ × ℝ),
          x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s → HasFDerivAt f (f' x) 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₂]]) →
            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 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)
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 : Set.Countable s
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
h₁ : ¬a₁ ≤ b₁
this :
  ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
    ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      (∀ (x : ℝ × ℝ),
          x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s → HasFDerivAt f (f' x) 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₂]]) →
            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 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)
refine' (congr_arg Neg.neg (this Hcf Hcg Hdf Hdg Hi (le_of_not_le h₁))).trans _
no goals
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 : Set.Countable s
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
h₁ : ¬a₁ ≤ b₁
this :
  ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
    ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      (∀ (x : ℝ × ℝ),
          x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s → HasFDerivAt f (f' x) 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₂]]) →
            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 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)
abel
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 : Set.Countable s
a₁ b₁ : ℝ
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
h₁ : a₁ ≤ b₁
h₂ : ¬a₂ ≤ b₂
this :
  ContinuousOn f ([[a₁, b₁]] ×ˢ [[b₂, a₂]]) →
    ContinuousOn g ([[a₁, b₁]] ×ˢ [[b₂, a₂]]) →
      (∀ (x : ℝ × ℝ),
          x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min b₂ a₂) (max b₂ a₂) \ s → HasFDerivAt f (f' x) x) →
        (∀ (x : ℝ × ℝ),
            x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min b₂ a₂) (max b₂ a₂) \ s → HasFDerivAt g (g' x) x) →
          IntegrableOn (fun x => ↑(f' x) (1, 0) + ↑(g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[b₂, a₂]]) →
            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)
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 : Set.Countable s
a₁ b₁ : ℝ
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
h₁ : a₁ ≤ b₁
this :
  ∀ (a₂ b₂ : ℝ),
    ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
        (∀ (x : ℝ × ℝ),
            x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s → HasFDerivAt f (f' x) 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₂]]) →
              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)
specialize this b₂ a₂
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 : Set.Countable s
a₁ b₁ : ℝ
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
h₁ : a₁ ≤ b₁
h₂ : ¬a₂ ≤ b₂
this :
  ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
    ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      (∀ (x : ℝ × ℝ),
          x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s → HasFDerivAt f (f' x) 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₂]]) →
            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)
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 : Set.Countable s
a₁ b₁ : ℝ
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
h₁ : a₁ ≤ b₁
h₂ : ¬a₂ ≤ b₂
this :
  ContinuousOn f ([[a₁, b₁]] ×ˢ [[b₂, a₂]]) →
    ContinuousOn g ([[a₁, b₁]] ×ˢ [[b₂, a₂]]) →
      (∀ (x : ℝ × ℝ),
          x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min b₂ a₂) (max b₂ a₂) \ s → HasFDerivAt f (f' x) x) →
        (∀ (x : ℝ × ℝ),
            x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min b₂ a₂) (max b₂ a₂) \ s → HasFDerivAt g (g' x) x) →
          IntegrableOn (fun x => ↑(f' x) (1, 0) + ↑(g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[b₂, a₂]]) →
            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)
rw [uIcc_comm b₂ a₂, min_comm b₂ a₂, max_comm b₂ a₂] at this
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 : Set.Countable s
a₁ b₁ : ℝ
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
h₁ : a₁ ≤ b₁
h₂ : ¬a₂ ≤ b₂
this :
  ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
    ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      (∀ (x : ℝ × ℝ),
          x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s → HasFDerivAt f (f' x) 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₂]]) →
            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₁, ∫ (x_1 : ℝ) in b₂..a₂, ↑(f' (x, x_1)) (1, 0) + ↑(g' (x, x_1)) (0, 1)) =
    (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + -∫ (x : ℝ) in b₂..a₂, f (b₁, x)) -
      -∫ (x : ℝ) in b₂..a₂, f (a₁, x)
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 : Set.Countable s
a₁ b₁ : ℝ
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
h₁ : a₁ ≤ b₁
h₂ : ¬a₂ ≤ b₂
this :
  ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
    ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      (∀ (x : ℝ × ℝ),
          x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s → HasFDerivAt f (f' x) 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₂]]) →
            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)
simp only [intervalIntegral.integral_symm b₂ a₂, intervalIntegral.integral_neg]
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 : Set.Countable s
a₁ b₁ : ℝ
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
h₁ : a₁ ≤ b₁
h₂ : ¬a₂ ≤ b₂
this :
  ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
    ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      (∀ (x : ℝ × ℝ),
          x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s → HasFDerivAt f (f' x) 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₂]]) →
            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₁, 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₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + -∫ (x : ℝ) in b₂..a₂, f (b₁, x)) -
      -∫ (x : ℝ) in b₂..a₂, f (a₁, x)
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 : Set.Countable s
a₁ b₁ : ℝ
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
h₁ : a₁ ≤ b₁
h₂ : ¬a₂ ≤ b₂
this :
  ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
    ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      (∀ (x : ℝ × ℝ),
          x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s → HasFDerivAt f (f' x) 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₂]]) →
            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₁, ∫ (x_1 : ℝ) in b₂..a₂, ↑(f' (x, x_1)) (1, 0) + ↑(g' (x, x_1)) (0, 1)) =
    (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + -∫ (x : ℝ) in b₂..a₂, f (b₁, x)) -
      -∫ (x : ℝ) in b₂..a₂, f (a₁, x)
refine' (congr_arg Neg.neg (this Hcf Hcg Hdf Hdg Hi (le_of_not_le h₂))).trans _
no goals
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 : Set.Countable s
a₁ b₁ : ℝ
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ (x : ℝ × ℝ), 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 : ℝ × ℝ), 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₂]])
h₁ : a₁ ≤ b₁
h₂ : ¬a₂ ≤ b₂
this :
  ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
    ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      (∀ (x : ℝ × ℝ),
          x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s → HasFDerivAt f (f' x) 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₂]]) →
            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₁, 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₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + -∫ (x : ℝ) in b₂..a₂, f (b₁, x)) -
      -∫ (x : ℝ) in b₂..a₂, f (a₁, x)
abel
no goals
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : Set.Countable s
a₁ b₁ : ℝ
h₁ : a₁ ≤ b₁
a₂ b₂ : ℝ
h₂ : a₂ ≤ b₂
Hcf : ContinuousOn f (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)
Hcg : ContinuousOn g (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)
Hdf : ∀ (x : ℝ × ℝ), x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s → HasFDerivAt f (f' x) x
Hdg : ∀ (x : ℝ × ℝ), x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s → HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x => ↑(f' x) (1, 0) + ↑(g' x) (0, 1)) (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)
⊢ (∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, ↑(f' (x, y)) (1, 0) + ↑(g' (x, y)) (0, 1)) =
    ∫ (x : ℝ) in Set.Icc a₁ b₁, ∫ (y : ℝ) in Set.Icc a₂ b₂, ↑(f' (x, y)) (1, 0) + ↑(g' (x, y)) (0, 1)
simp only [intervalIntegral.integral_of_le, h₁, h₂,
  set_integral_congr_set_ae (Ioc_ae_eq_Icc (α := ℝ) (μ := volume))]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : Set.Countable s
a₁ b₁ : ℝ
h₁ : a₁ ≤ b₁
a₂ b₂ : ℝ
h₂ : a₂ ≤ b₂
Hcf : ContinuousOn f (Set.Icc (a₁, a₂) (b₁, b₂))
Hcg : ContinuousOn g (Set.Icc (a₁, a₂) (b₁, b₂))
Hdf : ∀ (x : ℝ × ℝ), x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s → HasFDerivAt f (f' x) x
Hdg : ∀ (x : ℝ × ℝ), x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s → HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x => ↑(f' x) (1, 0) + ↑(g' x) (0, 1)) (Set.Icc (a₁, a₂) (b₁, b₂))
⊢ (∫ (x : ℝ × ℝ) in Set.Icc (a₁, a₂) (b₁, b₂), ↑(f' x) (1, 0) + ↑(g' x) (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)
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : Set.Countable s
a₁ b₁ : ℝ
h₁ : a₁ ≤ b₁
a₂ b₂ : ℝ
h₂ : a₂ ≤ b₂
Hcf : ContinuousOn f (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)
Hcg : ContinuousOn g (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)
Hdf : ∀ (x : ℝ × ℝ), x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s → HasFDerivAt f (f' x) x
Hdg : ∀ (x : ℝ × ℝ), x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s → HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x => ↑(f' x) (1, 0) + ↑(g' x) (0, 1)) (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)
⊢ (∫ (x : ℝ × ℝ) in Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂, ↑(f' x) (1, 0) + ↑(g' x) (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)
rw [Icc_prod_Icc] at *
no goals
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : Set.Countable s
a₁ b₁ : ℝ
h₁ : a₁ ≤ b₁
a₂ b₂ : ℝ
h₂ : a₂ ≤ b₂
Hcf : ContinuousOn f (Set.Icc (a₁, a₂) (b₁, b₂))
Hcg : ContinuousOn g (Set.Icc (a₁, a₂) (b₁, b₂))
Hdf : ∀ (x : ℝ × ℝ), x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s → HasFDerivAt f (f' x) x
Hdg : ∀ (x : ℝ × ℝ), x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s → HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x => ↑(f' x) (1, 0) + ↑(g' x) (0, 1)) (Set.Icc (a₁, a₂) (b₁, b₂))
⊢ (∫ (x : ℝ × ℝ) in Set.Icc (a₁, a₂) (b₁, b₂), ↑(f' x) (1, 0) + ↑(g' x) (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)
apply integral_divergence_prod_Icc_of_hasFDerivWithinAt_off_countable_of_le f g f' g'
  (a₁, a₂) (b₁, b₂) ⟨h₁, h₂⟩ s <;> assumption