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
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.{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) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := ContinuousLinearEquiv.symm (ContinuousLinearEquiv.finTwoArrow ℝ ℝ)
x : ℝ × ℝ
⊢ HAdd.hAdd (α := E) (β := E) ((f' x : (a : ℝ × ℝ) → E) (1, 0) : E) ((g' x : (a : ℝ × ℝ) → E) (0, 1) : E) =
    HAdd.hAdd (α := E) (β := E)
      ((![f', g'] 0 x : (a : ℝ × ℝ) → E)
          ((e.symm : (a : Fin (1 + 1) → ℝ) → ℝ × ℝ) (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ ℝ) 0 1) :
            ℝ × ℝ) :
        E)
      ((![f', g'] 1 x : (a : ℝ × ℝ) → E)
          ((e.symm : (a : Fin (1 + 1) → ℝ) → ℝ × ℝ) (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ ℝ) 1 1) :
            ℝ × ℝ) :
        E)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f_1 g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a_1 b_1 : ℝ × ℝ
hle : a_1 ≤ b_1
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f_1 (Set.Icc a_1 b_1)
Hcg : ContinuousOn g (Set.Icc a_1 b_1)
Hdf : ∀ x ∈ Set.Ioo a_1.1 b_1.1 ×ˢ Set.Ioo a_1.2 b_1.2 \ s, HasFDerivAt f_1 (f' x) x
Hdg : ∀ x ∈ Set.Ioo a_1.1 b_1.1 ×ˢ Set.Ioo a_1.2 b_1.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_1 b_1) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := ContinuousLinearEquiv.symm (ContinuousLinearEquiv.finTwoArrow ℝ ℝ)
a b : Fin 1 → ℝ
f : (Fin 1 → ℝ) → E
⊢ Eq.{u + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b)) fun (y : Fin 1 → ℝ) ↦ f y)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume
        ((⇑(MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ)) : (a : ℝ) → Fin 1 → ℝ) ⁻¹' Set.Icc a b))
      fun (x : ℝ) ↦ f ((MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ) : (a : ℝ) → Fin 1 → ℝ) x))

Tactic:
(((volume_preserving_funUnique (Fin 1) ℝ).symm _).setIntegral_preimage_emb
              (MeasurableEquiv.measurableEmbedding _) f _).symm

Premises used: MeasurableEquiv.measurableEmbedding, Real, MeasureTheory.MeasurePreserving.symm, MeasureTheory.MeasurePreserving.setIntegral_preimage_emb, OfNat.ofNat, Eq.symm, Fin, MeasureTheory.volume_preserving_funUnique
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f_1 g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a_1 b_1 : ℝ × ℝ
hle : a_1 ≤ b_1
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f_1 (Set.Icc a_1 b_1)
Hcg : ContinuousOn g (Set.Icc a_1 b_1)
Hdf : ∀ x ∈ Set.Ioo a_1.1 b_1.1 ×ˢ Set.Ioo a_1.2 b_1.2 \ s, HasFDerivAt f_1 (f' x) x
Hdg : ∀ x ∈ Set.Ioo a_1.1 b_1.1 ×ˢ Set.Ioo a_1.2 b_1.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_1 b_1) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := ContinuousLinearEquiv.symm (ContinuousLinearEquiv.finTwoArrow ℝ ℝ)
a b : Fin 1 → ℝ
f : (Fin 1 → ℝ) → E
h :
  Set.Icc (a 0) (b 0) =
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ)) : (a : ℝ) → Fin 1 → ℝ) ⁻¹' Set.Icc a b
⊢ Eq.{u + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b)) fun (x : Fin 1 → ℝ) ↦ f x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc (a 0) (b 0))) fun (x : ℝ) ↦
      f fun (x_1 : Fin 1) ↦ x)

Tactic:
convert!
          (((volume_preserving_funUnique (Fin 1) ℝ).symm _).setIntegral_preimage_emb
              (MeasurableEquiv.measurableEmbedding _) f _).symm

Premises used: MeasurableEquiv.measurableEmbedding, Real, MeasureTheory.MeasurePreserving.symm, MeasureTheory.MeasurePreserving.setIntegral_preimage_emb, OfNat.ofNat, Eq.symm, Fin, MeasureTheory.volume_preserving_funUnique
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f_1 g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a_1 b_1 : ℝ × ℝ
hle : a_1 ≤ b_1
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f_1 (Set.Icc a_1 b_1)
Hcg : ContinuousOn g (Set.Icc a_1 b_1)
Hdf : ∀ x ∈ Set.Ioo a_1.1 b_1.1 ×ˢ Set.Ioo a_1.2 b_1.2 \ s, HasFDerivAt f_1 (f' x) x
Hdg : ∀ x ∈ Set.Ioo a_1.1 b_1.1 ×ˢ Set.Ioo a_1.2 b_1.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_1 b_1) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := ContinuousLinearEquiv.symm (ContinuousLinearEquiv.finTwoArrow ℝ ℝ)
a b : Fin 1 → ℝ
f : (Fin 1 → ℝ) → E
⊢ Set.Icc (a 0) (b 0) =
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ)) : (a : ℝ) → Fin 1 → ℝ) ⁻¹' Set.Icc a b

Tactic:
((OrderIso.funUnique (Fin 1) ℝ).symm.preimage_Icc a b).symm

Premises used: Real, OrderIso.funUnique, OrderIso.symm, OrderIso.preimage_Icc, Equiv.funUnique, OfNat.ofNat, Eq.symm, Fin
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f_1 g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a_1 b_1 : ℝ × ℝ
hle : a_1 ≤ b_1
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f_1 (Set.Icc a_1 b_1)
Hcg : ContinuousOn g (Set.Icc a_1 b_1)
Hdf : ∀ x ∈ Set.Ioo a_1.1 b_1.1 ×ˢ Set.Ioo a_1.2 b_1.2 \ s, HasFDerivAt f_1 (f' x) x
Hdg : ∀ x ∈ Set.Ioo a_1.1 b_1.1 ×ˢ Set.Ioo a_1.2 b_1.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_1 b_1) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := ContinuousLinearEquiv.symm (ContinuousLinearEquiv.finTwoArrow ℝ ℝ)
a b : Fin 1 → ℝ
f : (Fin 1 → ℝ) → E
⊢ Set.Icc (a 0) (b 0) =
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ)) : (a : ℝ) → Fin 1 → ℝ) ⁻¹' Set.Icc a b

Tactic:
exact ((OrderIso.funUnique (Fin 1) ℝ).symm.preimage_Icc a b).symm

Premises used: Real, OrderIso.funUnique, OrderIso.symm, OrderIso.preimage_Icc, OfNat.ofNat, Eq.symm, Fin
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ 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.{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) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := ContinuousLinearEquiv.symm (ContinuousLinearEquiv.finTwoArrow ℝ ℝ)
⊢ ∀ (a b : Fin 1 → ℝ) (f : (Fin 1 → ℝ) → E),
    Eq.{u + 1} (α := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b)) fun (x : Fin 1 → ℝ) ↦
        f x)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc (a 0) (b 0))) fun (x : ℝ) ↦
        f fun (x_1 : Fin 1) ↦ x)

Tactic:
have : ∀ (a b : ℝ¹) (f : ℝ¹ → E),
          ∫ x in Icc a b, f x = ∫ x in Icc (a 0) (b 0), f fun _ => x := fun a b f ↦ by
        convert!
          (((volume_preserving_funUnique (Fin 1) ℝ).symm _).setIntegral_preimage_emb
              (MeasurableEquiv.measurableEmbedding _) f _).symm
        exact ((OrderIso.funUnique (Fin 1) ℝ).symm.preimage_Icc a b).symm
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ 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.{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) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := ContinuousLinearEquiv.symm (ContinuousLinearEquiv.finTwoArrow ℝ ℝ)
simp :
  HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.2 b.2)) fun (y : ℝ) ↦
          f (b.1, y))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.2 b.2)) fun (y : ℝ) ↦
          f (a.1, y)) +
      HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.1 b.1)) fun (x : ℝ) ↦
          g (x, b.2))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.1 b.1)) fun (x : ℝ) ↦
          g (x, a.2)) =
    (HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.1 b.1)) fun (x : ℝ) ↦
            g (x, b.2))
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.1 b.1)) fun (x : ℝ) ↦
            g (x, a.2)) +
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.2 b.2)) fun (y : ℝ) ↦
          f (b.1, y)) -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.2 b.2)) fun (y : ℝ) ↦
        f (a.1, y)
⊢ HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.2 b.2)) fun (y : ℝ) ↦
          f (b.1, y))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.2 b.2)) fun (y : ℝ) ↦
          f (a.1, y)) +
      HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.1 b.1)) fun (x : ℝ) ↦
          g (x, b.2))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.1 b.1)) fun (x : ℝ) ↦
          g (x, a.2)) =
    (HSub.hSub (α := E) (∫ (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)

Tactic:
simp only [intervalIntegral.integral_of_le hle.1, intervalIntegral.integral_of_le hle.2,
        setIntegral_congr_set (Ioc_ae_eq_Icc (α := ℝ) (μ := volume))]

Premises used: MeasureTheory.Ioc_ae_eq_Icc, intervalIntegral.integral_of_le, And.right, And.left, 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
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.{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) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := ContinuousLinearEquiv.symm (ContinuousLinearEquiv.finTwoArrow ℝ ℝ)
⊢ HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.2 b.2)) fun (y : ℝ) ↦
          f (b.1, y))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.2 b.2)) fun (y : ℝ) ↦
          f (a.1, y)) +
      HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.1 b.1)) fun (x : ℝ) ↦
          g (x, b.2))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.1 b.1)) fun (x : ℝ) ↦
          g (x, a.2)) =
    (HSub.hSub (α := E)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.1 b.1)) fun (x : ℝ) ↦
            g (x, b.2))
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.1 b.1)) fun (x : ℝ) ↦
            g (x, a.2)) +
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.2 b.2)) fun (y : ℝ) ↦
          f (b.1, y)) -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a.2 b.2)) fun (y : ℝ) ↦
        f (a.1, y)

Tactic:
abel
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a b : ℝ × ℝ
hle : a ≤ b
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, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2, 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) volume
⊢ Set.Countable (α := ℝ × ℝ) ∅

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a b : ℝ × ℝ
hle : a ≤ b
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, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2, 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) volume
⊢ ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ ∅, HasFDerivAt f (f' x) x

Tactic:
simpa only [diff_empty]

Premises used: Set.diff_empty
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a b : ℝ × ℝ
hle : a ≤ b
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, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2, 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) volume
⊢ ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ ∅, HasFDerivAt g (g' x) x

Tactic:
simpa only [diff_empty]

Premises used: Set.diff_empty
-- 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₂ : ℝ
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.{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
this :
  ∀ (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₁),
    ∫ (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)
h₁ : ¬a₁ ≤ b₁
⊢ ∀ (Hcf : ContinuousOn f ([[b₁, a₁]] ×ˢ [[a₂, b₂]])) (Hcg : ContinuousOn g ([[b₁, a₁]] ×ˢ [[a₂, b₂]]))
    (Hdf : ∀ x ∈ Set.Ioo (min b₁ a₁) (max b₁ a₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt f (f' x) x)
    (Hdg : ∀ x ∈ Set.Ioo (min b₁ a₁) (max b₁ a₁) ×ˢ 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))
        ([[b₁, a₁]] ×ˢ [[a₂, b₂]]) volume)
    (h₁ : b₁ ≤ a₁),
    ∫ (x : ℝ) in b₁..a₁,
        ∫ (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 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)

Tactic:
specialize this b₁ a₁
-- 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₂ : ℝ
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.{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₁
this :
  ∀ (Hcf : ContinuousOn f ([[b₁, a₁]] ×ˢ [[a₂, b₂]])) (Hcg : ContinuousOn g ([[b₁, a₁]] ×ˢ [[a₂, b₂]]))
    (Hdf : ∀ x ∈ Set.Ioo (min b₁ a₁) (max b₁ a₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt f (f' x) x)
    (Hdg : ∀ x ∈ Set.Ioo (min b₁ a₁) (max b₁ a₁) ×ˢ 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))
        ([[b₁, a₁]] ×ˢ [[a₂, b₂]]) volume)
    (h₁ : b₁ ≤ a₁),
    ∫ (x : ℝ) in b₁..a₁,
        ∫ (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 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)
⊢ ∀ (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₁ : b₁ ≤ a₁),
    ∫ (x : ℝ) in b₁..a₁,
        ∫ (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 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)

Tactic:
rw [uIcc_comm b₁ a₁, min_comm b₁ a₁, max_comm b₁ a₁] at this

Premises used: min_comm, Set.uIcc_comm, max_comm
-- 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₂ : ℝ
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.{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₁
this :
  ∀ (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₁ : b₁ ≤ a₁),
    ∫ (x : ℝ) in b₁..a₁,
        ∫ (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 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)
inr :
  -∫ (x : ℝ) in b₁..a₁,
        ∫ (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 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)
⊢ ∫ (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:
simp only [intervalIntegral.integral_symm b₁ a₁]

Premises used: intervalIntegral.integral_symm