-- Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean
theorem integral_divergence_prod_Icc_of_hasFDerivWithinAt_off_countable_of_le (f g : ℝ × ℝ → E)
    (f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E) (a b : ℝ × ℝ) (hle : a ≤ b) (s : Set (ℝ × ℝ)) (hs : s.Countable)
    (Hcf : ContinuousOn f (Icc a b)) (Hcg : ContinuousOn g (Icc a b))
    (Hdf : ∀ x ∈ Ioo a.1 b.1 ×ˢ Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x)
    (Hdg : ∀ x ∈ Ioo a.1 b.1 ×ˢ Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x)
    (Hi : IntegrableOn (fun x => f' x (1, 0) + g' x (0, 1)) (Icc a b)) :
    (∫ x in Icc a b, f' x (1, 0) + g' x (0, 1)) =
      (((∫ x in a.1..b.1, g (x, b.2)) - ∫ x in a.1..b.1, g (x, a.2)) +
          ∫ y in a.2..b.2, f (b.1, y)) -
        ∫ y in a.2..b.2, f (a.1, y) :=
  let e : (ℝ × ℝ) ≃L[ℝ] ℝ² := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm
  calc
    (∫ x in Icc a b, f' x (1, 0) + g' x (0, 1)) =
        ∑ i : Fin 2,
          ((∫ x in Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove),
              ![f, g] i (e.symm <| i.insertNth (e b i) x)) -
            ∫ x in Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove),
              ![f, g] i (e.symm <| i.insertNth (e a i) x))

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a b : ℝ × ℝ
hle : a ≤ b
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f (Set.Icc a b)
Hcg : ContinuousOn g (Set.Icc a b)
Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm
⊢ ((∫ (y : ℝ) in Set.Icc a.2 b.2, f (b.1, y)) - ∫ (y : ℝ) in Set.Icc a.2 b.2, f (a.1, y)) +
      ((∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, b.2)) - ∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, a.2)) =
    (((∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, b.2)) - ∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, a.2)) +
        ∫ (y : ℝ) in Set.Icc a.2 b.2, f (b.1, y)) -
      ∫ (y : ℝ) in Set.Icc a.2 b.2, f (a.1, y)

Tactic:
abel

Result:
no goals

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a b : ℝ × ℝ
hle : a ≤ b
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f (Set.Icc a b)
Hcg : ContinuousOn g (Set.Icc a b)
Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm
this :
  ∀ (a b : Fin 1 → ℝ) (f : (Fin 1 → ℝ) → E),
    ∫ (x : Fin 1 → ℝ) in Set.Icc a b, f x = ∫ (x : ℝ) in Set.Icc (a 0) (b 0), f fun x_1 => x
⊢ ((∫ (x : ℝ) in Set.Icc ((e a ∘ Fin.succAbove 0) 0) ((e b ∘ Fin.succAbove 0) 0),
          ![f, g] 0 (e.symm (Fin.insertNth 0 (e b 0) fun x_1 => x))) -
        ∫ (x : ℝ) in Set.Icc ((e a ∘ Fin.succAbove 0) 0) ((e b ∘ Fin.succAbove 0) 0),
          ![f, g] 0 (e.symm (Fin.insertNth 0 (e a 0) fun x_1 => x))) +
      ((∫ (x : ℝ) in Set.Icc ((e a ∘ Fin.succAbove 1) 0) ((e b ∘ Fin.succAbove 1) 0),
          ![f, g] 1 (e.symm (Fin.insertNth 1 (e b 1) fun x_1 => x))) -
        ∫ (x : ℝ) in Set.Icc ((e a ∘ Fin.succAbove 1) 0) ((e b ∘ Fin.succAbove 1) 0),
          ![f, g] 1 (e.symm (Fin.insertNth 1 (e a 1) fun x_1 => x))) =
    ((∫ (y : ℝ) in Set.Icc a.2 b.2, f (b.1, y)) - ∫ (y : ℝ) in Set.Icc a.2 b.2, f (a.1, y)) +
      ((∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, b.2)) - ∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, a.2))

Tactic:
rfl

Result:
no goals

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a b : ℝ × ℝ
hle : a ≤ b
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f (Set.Icc a b)
Hcg : ContinuousOn g (Set.Icc a b)
Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm
this :
  ∀ (a b : Fin 1 → ℝ) (f : (Fin 1 → ℝ) → E),
    ∫ (x : Fin 1 → ℝ) in Set.Icc a b, f x = ∫ (x : ℝ) in Set.Icc (a 0) (b 0), f fun x_1 => x
⊢ ∑ i : Fin 2,
      ((∫ (x : Fin 1 → ℝ) in Set.Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove),
          ![f, g] i (e.symm (i.insertNth (e b i) x))) -
        ∫ (x : Fin 1 → ℝ) in Set.Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove),
          ![f, g] i (e.symm (i.insertNth (e a i) x))) =
    ((∫ (y : ℝ) in Set.Icc a.2 b.2, f (b.1, y)) - ∫ (y : ℝ) in Set.Icc a.2 b.2, f (a.1, y)) +
      ((∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, b.2)) - ∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, a.2))

Tactic:
simp only [Fin.sum_univ_two, this]

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a b : ℝ × ℝ
hle : a ≤ b
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f (Set.Icc a b)
Hcg : ContinuousOn g (Set.Icc a b)
Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm
this :
  ∀ (a b : Fin 1 → ℝ) (f : (Fin 1 → ℝ) → E),
    ∫ (x : Fin 1 → ℝ) in Set.Icc a b, f x = ∫ (x : ℝ) in Set.Icc (a 0) (b 0), f fun x_1 => x
⊢ ((∫ (x : ℝ) in Set.Icc ((e a ∘ Fin.succAbove 0) 0) ((e b ∘ Fin.succAbove 0) 0),
          ![f, g] 0 (e.symm (Fin.insertNth 0 (e b 0) fun x_1 => x))) -
        ∫ (x : ℝ) in Set.Icc ((e a ∘ Fin.succAbove 0) 0) ((e b ∘ Fin.succAbove 0) 0),
          ![f, g] 0 (e.symm (Fin.insertNth 0 (e a 0) fun x_1 => x))) +
      ((∫ (x : ℝ) in Set.Icc ((e a ∘ Fin.succAbove 1) 0) ((e b ∘ Fin.succAbove 1) 0),
          ![f, g] 1 (e.symm (Fin.insertNth 1 (e b 1) fun x_1 => x))) -
        ∫ (x : ℝ) in Set.Icc ((e a ∘ Fin.succAbove 1) 0) ((e b ∘ Fin.succAbove 1) 0),
          ![f, g] 1 (e.symm (Fin.insertNth 1 (e a 1) fun x_1 => x))) =
    ((∫ (y : ℝ) in Set.Icc a.2 b.2, f (b.1, y)) - ∫ (y : ℝ) in Set.Icc a.2 b.2, f (a.1, y)) +
      ((∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, b.2)) - ∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, a.2))

Proof state:
case refine_3
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a b : ℝ × ℝ
hle : a ≤ b
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f (Set.Icc a b)
Hcg : ContinuousOn g (Set.Icc a b)
Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm
⊢ ∀ (i : Fin (1 + 1)), ContinuousOn (![f, g] i) (Set.Icc a b)

Tactic:
exact Fin.forall_fin_two.2 ⟨Hcf, Hcg⟩

Result:
no goals