Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case hs
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
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 ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x
Hdg : ∀ 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₂)) volume
⊢ s.Countable

pp: case Hcf
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
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 ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x
Hdg : ∀ 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₂)) volume
⊢ ContinuousOn f (Set.Icc (a₁, a₂) (b₁, b₂))

pp: case Hcg
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
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 ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x
Hdg : ∀ 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₂)) volume
⊢ ContinuousOn g (Set.Icc (a₁, a₂) (b₁, b₂))

pp: case Hdf
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
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 ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x
Hdg : ∀ 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₂)) volume
⊢ ∀ x ∈ Set.Ioo (a₁, a₂).1 (b₁, b₂).1 ×ˢ Set.Ioo (a₁, a₂).2 (b₁, b₂).2 \ s, HasFDerivAt f (f' x) x

pp: case Hdg
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
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 ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x
Hdg : ∀ 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₂)) volume
⊢ ∀ x ∈ Set.Ioo (a₁, a₂).1 (b₁, b₂).1 ×ˢ Set.Ioo (a₁, a₂).2 (b₁, b₂).2 \ s, HasFDerivAt g (g' x) x

pp: case Hi
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
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 ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x
Hdg : ∀ 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₂)) volume
⊢ IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc (a₁, a₂) (b₁, b₂)) volume

Tactic:
<;>

Goal state after:
case hs
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
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 ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x
Hdg : ∀ 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₂)) volume
⊢ s.Countable

case Hcf
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
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 ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x
Hdg : ∀ 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₂)) volume
⊢ ContinuousOn f (Set.Icc (a₁, a₂) (b₁, b₂))

case Hcg
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
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 ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x
Hdg : ∀ 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₂)) volume
⊢ ContinuousOn g (Set.Icc (a₁, a₂) (b₁, b₂))

case Hdf
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
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 ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x
Hdg : ∀ 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₂)) volume
⊢ ∀ x ∈ Set.Ioo (a₁, a₂).1 (b₁, b₂).1 ×ˢ Set.Ioo (a₁, a₂).2 (b₁, b₂).2 \ s, HasFDerivAt f (f' x) x

case Hdg
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
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 ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x
Hdg : ∀ 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₂)) volume
⊢ ∀ x ∈ Set.Ioo (a₁, a₂).1 (b₁, b₂).1 ×ˢ Set.Ioo (a₁, a₂).2 (b₁, b₂).2 \ s, HasFDerivAt g (g' x) x

case Hi
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
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 ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x
Hdg : ∀ 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₂)) volume
⊢ IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc (a₁, a₂) (b₁, b₂)) volume