awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
a₁ b₁ : ℝ
h₁ : a₁ ≤ b₁
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₂
Hcf₁ : ContinuousOn f (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)
⊢ ContinuousOn g (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)

Tactic:
simp only [uIcc_of_le h₁, uIcc_of_le h₂, min_eq_left, max_eq_right, h₁, h₂] at Hcf Hcg Hdf Hdg Hi

Premises used: Set.uIcc_of_le, max_eq_right, min_eq_left
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
a₁ b₁ : ℝ
h₁ : a₁ ≤ b₁
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₂
Hcf₁ : ContinuousOn f (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)
Hcg₁ : ContinuousOn g (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)
⊢ ∀ x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x

Tactic:
simp only [uIcc_of_le h₁, uIcc_of_le h₂, min_eq_left, max_eq_right, h₁, h₂] at Hcf Hcg Hdf Hdg Hi

Premises used: Set.uIcc_of_le, max_eq_right, min_eq_left
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
a₁ b₁ : ℝ
h₁ : a₁ ≤ b₁
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₂
Hcf₁ : ContinuousOn f (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)
Hcg₁ : ContinuousOn g (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)
Hdf₁ : ∀ x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x
⊢ ∀ x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt g (g' x) x

Tactic:
simp only [uIcc_of_le h₁, uIcc_of_le h₂, min_eq_left, max_eq_right, h₁, h₂] at Hcf Hcg Hdf Hdg Hi

Premises used: Set.uIcc_of_le, max_eq_right, min_eq_left
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
a₁ b₁ : ℝ
h₁ : a₁ ≤ b₁
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₂
Hcf₁ : ContinuousOn f (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)
Hcg₁ : ContinuousOn g (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ 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
⊢ 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))
    (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂) volume

Tactic:
simp only [uIcc_of_le h₁, uIcc_of_le h₂, min_eq_left, max_eq_right, h₁, h₂] at Hcf Hcg Hdf Hdg Hi

Premises used: Set.uIcc_of_le, max_eq_right, min_eq_left
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : 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₁ b₁ ×ˢ Set.Icc a₂ b₂)
Hcg : ContinuousOn g (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ 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.{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))
    (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂) volume
⊢ Eq.{u + 1} (α := E)
    (∫ (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))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a₁ b₁)) fun (x : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a₂ b₂)) fun (y : ℝ) ↦
        HAdd.hAdd (α := E) (β := E) ((f' (x, y) : (a : ℝ × ℝ) → E) (1, 0) : E)
          ((g' (x, y) : (a : ℝ × ℝ) → E) (0, 1) : E))

Tactic:
simp only [intervalIntegral.integral_of_le, h₁, h₂,
        setIntegral_congr_set (Ioc_ae_eq_Icc (α := ℝ) (μ := volume))]

Premises used: MeasureTheory.Ioc_ae_eq_Icc, intervalIntegral.integral_of_le, MeasureTheory.setIntegral_congr_set
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : 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₁ b₁ ×ˢ Set.Icc a₂ b₂)
Hcg : ContinuousOn g (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ 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.{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))
    (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂) volume
⊢ Eq.{u + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a₁ b₁)) fun (x : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a₂ b₂)) fun (y : ℝ) ↦
        HAdd.hAdd (α := E) (β := E) ((f' (x, y) : (a : ℝ × ℝ) → E) (1, 0) : E)
          ((g' (x, y) : (a : ℝ × ℝ) → E) (0, 1) : E))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂))
      fun (x : ℝ × ℝ) ↦
      HAdd.hAdd (α := E) (β := E) ((f' x : (a : ℝ × ℝ) → E) (1, 0) : E) ((g' x : (a : ℝ × ℝ) → E) (0, 1) : E))

Tactic:
(setIntegral_prod _ Hi).symm

Premises used: Eq.symm, MeasureTheory.setIntegral_prod
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : 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₁ b₁ ×ˢ Set.Icc a₂ b₂)
Hcg : ContinuousOn g (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ 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.{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))
    (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂) volume
rw :
  ∀ (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.{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))
        (Set.Icc (a₁, a₂) (b₁, b₂)) volume),
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc (a₁, a₂) (b₁, b₂)))
        fun (x : ℝ × ℝ) ↦
        HAdd.hAdd (α := E) (β := E) ((f' x : (a : ℝ × ℝ) → E) (1, 0) : E) ((g' x : (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)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂))
      fun (x : ℝ × ℝ) ↦
      HAdd.hAdd (α := E) (β := E) ((f' x : (a : ℝ × ℝ) → E) (1, 0) : E) ((g' x : (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:
rw [Icc_prod_Icc] at *

Premises used: Set.Icc_prod_Icc
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : 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.{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))
    (Set.Icc (a₁, a₂) (b₁, b₂)) volume
hs₁ : s.Countable
Hcf₁ : ContinuousOn f (Set.Icc (a₁, a₂) (b₁, b₂))
Hcg₁ : ContinuousOn g (Set.Icc (a₁, a₂) (b₁, b₂))
Hdf₁ : ∀ x ∈ Set.Ioo (a₁, a₂).1 (b₁, b₂).1 ×ˢ Set.Ioo (a₁, a₂).2 (b₁, b₂).2 \ s, HasFDerivAt f (f' x) x
Hdg₁ : ∀ x ∈ Set.Ioo (a₁, a₂).1 (b₁, b₂).1 ×ˢ Set.Ioo (a₁, a₂).2 (b₁, b₂).2 \ 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))
    (Set.Icc (a₁, a₂) (b₁, b₂)) volume
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc (a₁, a₂) (b₁, b₂)))
      fun (x : ℝ × ℝ) ↦
      HAdd.hAdd (α := E) (β := E) ((f' x : (a : ℝ × ℝ) → E) (1, 0) : E) ((g' x : (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:
apply integral_divergence_prod_Icc_of_hasFDerivAt_off_countable_of_le f g f' g'
        (a₁, a₂) (b₁, b₂) ⟨h₁, h₂⟩ s

Premises used: MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivAt_off_countable_of_le, Prod.mk, And.intro
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : 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.{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))
    (Set.Icc (a₁, a₂) (b₁, b₂)) volume
⊢ s.Countable

Tactic:
assumption
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : 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.{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))
    (Set.Icc (a₁, a₂) (b₁, b₂)) volume
⊢ ContinuousOn f (Set.Icc (a₁, a₂) (b₁, b₂))

Tactic:
assumption
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : 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.{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))
    (Set.Icc (a₁, a₂) (b₁, b₂)) volume
⊢ ContinuousOn g (Set.Icc (a₁, a₂) (b₁, b₂))

Tactic:
assumption
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : 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.{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))
    (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

Tactic:
assumption
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : 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.{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))
    (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

Tactic:
assumption
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : 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.{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))
    (Set.Icc (a₁, a₂) (b₁, b₂)) volume
⊢ 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))
    (Set.Icc (a₁, a₂) (b₁, b₂)) volume

Tactic:
assumption
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : 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₁ b₁ ×ˢ Set.Icc a₂ b₂)
Hcg : ContinuousOn g (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ 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.{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))
    (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂) volume
x :
  Eq.{u + 1} (α := E)
    (∫ (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))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a₁ b₁)) fun (x : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a₂ b₂)) fun (y : ℝ) ↦
        HAdd.hAdd (α := E) (β := E) ((f' (x, y) : (a : ℝ × ℝ) → E) (1, 0) : E)
          ((g' (x, y) : (a : ℝ × ℝ) → E) (0, 1) : E))
x₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂))
      fun (x : ℝ × ℝ) ↦
      HAdd.hAdd (α := E) (β := E) ((f' x : (a : ℝ × ℝ) → E) (1, 0) : E) ((g' x : (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)

Tactic:
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₂,
        setIntegral_congr_set (Ioc_ae_eq_Icc (α := ℝ) (μ := volume))]
    _ = ∫ x in Icc a₁ b₁ ×ˢ Icc a₂ b₂, f' x (1, 0) + g' x (0, 1) := (setIntegral_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_hasFDerivAt_off_countable_of_le f g f' g'
        (a₁, a₂) (b₁, b₂) ⟨h₁, h₂⟩ s <;> assumption

Premises used: HSub.hSub, intervalIntegral, Prod.mk, Set.Icc, MeasureTheory.MeasureSpace.volume, HAdd.hAdd, OfNat.ofNat, Eq.symm, DFunLike.coe, MeasureTheory.setIntegral_prod
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a₁ a₂ b₁ 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₂), HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂), 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
⊢ ∫ (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:
integral2_divergence_prod_of_hasFDerivAt_off_countable f g f' g' a₁ a₂ b₁ b₂ ∅ countable_empty
    Hcf Hcg (fun x hx ↦ Hdf x hx.1) (fun x hx ↦ Hdg x hx.1) Hi

Premises used: MeasureTheory.integral2_divergence_prod_of_hasFDerivAt_off_countable, And.left, EmptyCollection.emptyCollection, Set.countable_empty
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
F : ℕ → α → G
f : α → G
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
simp : Tendsto (fun (n : ℕ) ↦ setToFun μ (weightedSMul μ) ⋯ (F n)) atTop (𝓝 (setToFun μ (weightedSMul μ) ⋯ f))
⊢ Tendsto.{0, u_3} (β := G) (fun (n : ℕ) ↦ ∫ (a : α), F n a ∂μ) atTop (𝓝 (∫ (a : α), f a ∂μ))

Tactic:
simp only [integral_eq_setToFun]

Premises used: MeasureTheory.integral_eq_setToFun
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
F : ℕ → α → G
f : α → G
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
⊢ Tendsto (fun (n : ℕ) ↦ setToFun μ (weightedSMul μ) ⋯ (F n)) atTop (𝓝 (setToFun μ (weightedSMul μ) ⋯ f))

Tactic:
tendsto_setToFun_of_dominated_convergence (dominatedFinMeasAdditive_weightedSMul μ)
    bound F_measurable bound_integrable h_bound h_lim

Premises used: MeasureTheory.tendsto_setToFun_of_dominated_convergence, MeasureTheory.dominatedFinMeasAdditive_weightedSMul
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
F : ℕ → α → G
f : α → G
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
⊢ Tendsto (fun (n : ℕ) ↦ setToFun μ (weightedSMul μ) ⋯ (F n)) atTop (𝓝 (setToFun μ (weightedSMul μ) ⋯ f))

Tactic:
exact tendsto_setToFun_of_dominated_convergence (dominatedFinMeasAdditive_weightedSMul μ)
    bound F_measurable bound_integrable h_bound h_lim

Premises used: MeasureTheory.tendsto_setToFun_of_dominated_convergence, MeasureTheory.dominatedFinMeasAdditive_weightedSMul