awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hi : IntegrableOn (mα := Real.measurableSpace) f' (Set.Ioc a b) volume
e : ℝ ≃L[ℝ] Fin 1 → ℝ := ContinuousLinearEquiv.symm (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ)
F' : ℝ → ℝ →L[ℝ] E := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Set.Icc a b) volume

Tactic:
Hi.congr_set_ae Ioc_ae_eq_Icc.symm

Premises used: MeasureTheory.Ioc_ae_eq_Icc, MeasureTheory.IntegrableOn.congr_set_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hi : IntegrableOn (mα := Real.measurableSpace) f' (Set.Ioc a b) volume
e : ℝ ≃L[ℝ] Fin 1 → ℝ := ContinuousLinearEquiv.symm (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ)
F' : ℝ → ℝ →L[ℝ] E := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Set.Icc a b) volume

Tactic:
exact Hi.congr_set_ae Ioc_ae_eq_Icc.symm

Premises used: MeasureTheory.Ioc_ae_eq_Icc, MeasureTheory.IntegrableOn.congr_set_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ Set.Ioo a b \ s, HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
e : ℝ ≃L[ℝ] Fin 1 → ℝ := ContinuousLinearEquiv.symm (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ)
F' : ℝ → ℝ →L[ℝ] E := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
⊢ ∑ i : Fin 1,
      HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume
            (Set.Icc ((e : (a : ℝ) → Fin 1 → ℝ) a ∘ i.succAbove) ((e : (a : ℝ) → Fin 1 → ℝ) b ∘ i.succAbove)))
          fun (x : Fin 0 → ℝ) ↦
          f ((e.symm : (a : Fin 1 → ℝ) → ℝ) (i.insertNth (α := fun (a : Fin 1) ↦ ℝ) ((e : (a : ℝ) → Fin 1 → ℝ) b i) x)))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume
            (Set.Icc ((e : (a : ℝ) → Fin 1 → ℝ) a ∘ i.succAbove) ((e : (a : ℝ) → Fin 1 → ℝ) b ∘ i.succAbove)))
          fun (x : Fin 0 → ℝ) ↦
          f
            ((e.symm : (a : Fin 1 → ℝ) → ℝ)
              (i.insertNth (α := fun (a : Fin 1) ↦ ℝ) ((e : (a : ℝ) → Fin 1 → ℝ) a i) x))) =
    f b - f a

Tactic:
simp [e, Subsingleton.elim (const (Fin 0) _) isEmptyElim, volume_pi,
        Measure.pi_of_empty fun _ : Fin 0 ↦ _]

Premises used: MeasureTheory.volume_pi, MeasureTheory.Measure.pi_of_empty, isEmptyElim, Function.const, Subsingleton.elim, OfNat.ofNat, Fin
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f [[a, b]]
Hd : ∀ x ∈ Set.Ioo (min a b) (max a b) \ s, HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
inl : ∀ (hab : a ≤ b), ∫ (x : ℝ) in a..b, f' x = f b - f a
inr : ∀ (hab : b ≤ a), ∫ (x : ℝ) in a..b, f' x = f b - f a
⊢ ∫ (x : ℝ) in a..b, f' x = f b - f a

Tactic:
rcases le_total a b with hab | hab

Premises used: le_total
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f [[a, b]]
Hd : ∀ x ∈ Set.Ioo (min a b) (max a b) \ s, HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
hab : a ≤ b
⊢ ContinuousOn f (Set.Icc a b)

Tactic:
simp only [uIcc_of_le hab, min_eq_left hab, max_eq_right hab] at *

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
inst_2 : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f [[a, b]]
Hd : ∀ x ∈ Set.Ioo (min a b) (max a b) \ s, HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
hab : a ≤ b
Hc₁ : ContinuousOn f (Set.Icc a b)
⊢ ∀ x ∈ Set.Ioo a b \ s, HasDerivAt f (f' x) x

Tactic:
simp only [uIcc_of_le hab, min_eq_left hab, max_eq_right hab] at *

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
inst_2 : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : s.Countable
Hi : IntervalIntegrable f' volume a b
hab : a ≤ b
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ Set.Ioo a b \ s, HasDerivAt f (f' x) x
⊢ ∫ (x : ℝ) in a..b, f' x = f b - f a

Tactic:
integral_eq_of_hasDerivAt_off_countable_of_le f f' hab hs Hc Hd Hi

Premises used: MeasureTheory.integral_eq_of_hasDerivAt_off_countable_of_le
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : s.Countable
Hi : IntervalIntegrable f' volume a b
hab : a ≤ b
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ Set.Ioo a b \ s, HasDerivAt f (f' x) x
⊢ ∫ (x : ℝ) in a..b, f' x = f b - f a

Tactic:
exact integral_eq_of_hasDerivAt_off_countable_of_le f f' hab hs Hc Hd Hi

Premises used: MeasureTheory.integral_eq_of_hasDerivAt_off_countable_of_le
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f [[a, b]]
Hd : ∀ x ∈ Set.Ioo (min a b) (max a b) \ s, HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
hab : b ≤ a
⊢ ContinuousOn f (Set.Icc b a)

Tactic:
simp only [uIcc_of_ge hab, min_eq_right hab, max_eq_left hab] at *

Premises used: Set.uIcc_of_ge, max_eq_left, min_eq_right
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f [[a, b]]
Hd : ∀ x ∈ Set.Ioo (min a b) (max a b) \ s, HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
hab : b ≤ a
Hc₁ : ContinuousOn f (Set.Icc b a)
⊢ ∀ x ∈ Set.Ioo b a \ s, HasDerivAt f (f' x) x

Tactic:
simp only [uIcc_of_ge hab, min_eq_right hab, max_eq_left hab] at *

Premises used: Set.uIcc_of_ge, max_eq_left, min_eq_right
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : s.Countable
Hi : IntervalIntegrable f' volume a b
hab : b ≤ a
Hc : ContinuousOn f (Set.Icc b a)
Hd : ∀ x ∈ Set.Ioo b a \ s, HasDerivAt f (f' x) x
inr : ∫ (x : ℝ) in b..a, f' x = f a - f b
⊢ ∫ (x : ℝ) in a..b, f' x = f b - f a

Tactic:
rw [intervalIntegral.integral_symm, neg_eq_iff_eq_neg, neg_sub]

Premises used: neg_sub, neg_eq_iff_eq_neg, intervalIntegral.integral_symm
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : s.Countable
Hi : IntervalIntegrable f' volume a b
hab : b ≤ a
Hc : ContinuousOn f (Set.Icc b a)
Hd : ∀ x ∈ Set.Ioo b a \ s, HasDerivAt f (f' x) x
⊢ ∫ (x : ℝ) in b..a, f' x = f a - f b

Tactic:
integral_eq_of_hasDerivAt_off_countable_of_le f f' hab hs Hc Hd Hi.symm

Premises used: MeasureTheory.integral_eq_of_hasDerivAt_off_countable_of_le, IntervalIntegrable.symm
-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : s.Countable
Hi : IntervalIntegrable f' volume a b
hab : b ≤ a
Hc : ContinuousOn f (Set.Icc b a)
Hd : ∀ x ∈ Set.Ioo b a \ s, HasDerivAt f (f' x) x
⊢ ∫ (x : ℝ) in b..a, f' x = f a - f b

Tactic:
exact integral_eq_of_hasDerivAt_off_countable_of_le f f' hab hs Hc Hd Hi.symm

Premises used: MeasureTheory.integral_eq_of_hasDerivAt_off_countable_of_le, IntervalIntegrable.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 ℝ ℝ)
⊢ Eq.{u + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b)) fun (x : ℝ × ℝ) ↦
      HAdd.hAdd (α := E) (β := E) ((f' x : (a : ℝ × ℝ) → E) (1, 0) : E) ((g' x : (a : ℝ × ℝ) → E) (0, 1) : E))
    (∑ i : Fin 2,
      HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume
            (Set.Icc ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) a ∘ i.succAbove) ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) b ∘ i.succAbove)))
          fun (x : Fin 1 → ℝ) ↦
          ![f, g] i
            ((e.symm : (a : Fin 2 → ℝ) → ℝ × ℝ)
              (i.insertNth (α := fun (a : Fin 2) ↦ ℝ) ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) b i) x)))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume
            (Set.Icc ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) a ∘ i.succAbove) ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) b ∘ i.succAbove)))
          fun (x : Fin 1 → ℝ) ↦
          ![f, g] i
            ((e.symm : (a : Fin 2 → ℝ) → ℝ × ℝ)
              (i.insertNth (α := fun (a : Fin 2) ↦ ℝ) ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) a i) x))))

Tactic:
integral_divergence_of_hasFDerivAt_off_countable_of_equiv e ?_ ?_ ![f, g]
        ![f', g'] s hs a b hle ?_ (fun x hx => ?_) _ ?_ Hi

Premises used: MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable_of_equiv, Matrix.vecEmpty, Matrix.vecCons
-- 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 ℝ ℝ)
refine_1 :
  ∀ (x y : ℝ × ℝ),
    LE.le (α := Fin (HAdd.hAdd (α := ℕ) 1 1) → ℝ)
        ((e : (a : ℝ × ℝ) → Fin (1 + 1) → ℝ) x : Fin (HAdd.hAdd (α := ℕ) 1 1) → ℝ)
        ((e : (a : ℝ × ℝ) → Fin (1 + 1) → ℝ) y : Fin (HAdd.hAdd (α := ℕ) 1 1) → ℝ) ↔
      x ≤ y
refine_2 :
  MeasurePreserving (α := ℝ × ℝ) (β := Fin (HAdd.hAdd (α := ℕ) 1 1) → ℝ) (⇑e : (a : ℝ × ℝ) → Fin (1 + 1) → ℝ) volume
    volume
refine_3 : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), ContinuousOn (![f, g] i) (Set.Icc a b)
refine_4 :
  ∀ (x : ℝ × ℝ) (hx : x ∈ interior (Set.Icc a b) \ s) (i : Fin (HAdd.hAdd (α := ℕ) 1 1)),
    HasFDerivAt (![f, g] i) (![f', g'] i x) x
refine_5 :
  ∀ (x : ℝ × ℝ),
    HAdd.hAdd (α := E) (β := E) ((f' x : (a : ℝ × ℝ) → E) (1, 0) : E) ((g' x : (a : ℝ × ℝ) → E) (0, 1) : E) =
      ∑ i : Fin (1 + 1),
        (![f', g'] i x : (a : ℝ × ℝ) → E)
          ((e.symm : (a : Fin (1 + 1) → ℝ) → ℝ × ℝ) (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ ℝ) i 1) :
            ℝ × ℝ)
⊢ Eq.{u + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b)) fun (x : ℝ × ℝ) ↦
      HAdd.hAdd (α := E) (β := E) ((f' x : (a : ℝ × ℝ) → E) (1, 0) : E) ((g' x : (a : ℝ × ℝ) → E) (0, 1) : E))
    (∑ i : Fin 2,
      HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume
            (Set.Icc ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) a ∘ i.succAbove) ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) b ∘ i.succAbove)))
          fun (x : Fin 1 → ℝ) ↦
          ![f, g] i
            ((e.symm : (a : Fin 2 → ℝ) → ℝ × ℝ)
              (i.insertNth (α := fun (a : Fin 2) ↦ ℝ) ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) b i) x)))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume
            (Set.Icc ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) a ∘ i.succAbove) ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) b ∘ i.succAbove)))
          fun (x : Fin 1 → ℝ) ↦
          ![f, g] i
            ((e.symm : (a : Fin 2 → ℝ) → ℝ × ℝ)
              (i.insertNth (α := fun (a : Fin 2) ↦ ℝ) ((e : (a : ℝ × ℝ) → Fin 2 → ℝ) a i) x))))

Tactic:
refine integral_divergence_of_hasFDerivAt_off_countable_of_equiv e ?_ ?_ ![f, g]
        ![f', g'] s hs a b hle ?_ (fun x hx => ?_) _ ?_ Hi

Premises used: MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable_of_equiv, Matrix.vecEmpty, Matrix.vecCons
-- 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 y : ℝ × ℝ),
    LE.le (α := Fin (HAdd.hAdd (α := ℕ) 1 1) → ℝ)
        ((e : (a : ℝ × ℝ) → Fin (1 + 1) → ℝ) x : Fin (HAdd.hAdd (α := ℕ) 1 1) → ℝ)
        ((e : (a : ℝ × ℝ) → Fin (1 + 1) → ℝ) y : Fin (HAdd.hAdd (α := ℕ) 1 1) → ℝ) ↔
      x ≤ y

Tactic:
fun x y => (OrderIso.finTwoArrowIso ℝ).symm.le_iff_le

Premises used: Real, Fin.cons, OrderIso.le_iff_le, OrderIso.symm, OrderIso.finTwoArrowIso, Fin.induction, Fin.cases, Matrix.vecCons
-- 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 y : ℝ × ℝ),
    LE.le (α := Fin (HAdd.hAdd (α := ℕ) 1 1) → ℝ)
        ((e : (a : ℝ × ℝ) → Fin (1 + 1) → ℝ) x : Fin (HAdd.hAdd (α := ℕ) 1 1) → ℝ)
        ((e : (a : ℝ × ℝ) → Fin (1 + 1) → ℝ) y : Fin (HAdd.hAdd (α := ℕ) 1 1) → ℝ) ↔
      x ≤ y

Tactic:
exact fun x y => (OrderIso.finTwoArrowIso ℝ).symm.le_iff_le

Premises used: Real, OrderIso.le_iff_le, OrderIso.symm, OrderIso.finTwoArrowIso
-- 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 ℝ ℝ)
⊢ MeasurePreserving (α := ℝ × ℝ) (β := Fin (HAdd.hAdd (α := ℕ) 1 1) → ℝ) (⇑e : (a : ℝ × ℝ) → Fin (1 + 1) → ℝ) volume
    volume

Tactic:
(volume_preserving_finTwoArrow ℝ).symm _

Premises used: Real, MeasureTheory.MeasurePreserving.symm, Fin.cons, Fin.induction, Matrix.vecEmpty, Fin.cases, MeasureTheory.volume_preserving_finTwoArrow, Matrix.vecCons
-- 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 ℝ ℝ)
⊢ MeasurePreserving (α := ℝ × ℝ) (β := Fin (HAdd.hAdd (α := ℕ) 1 1) → ℝ) (⇑e : (a : ℝ × ℝ) → Fin (1 + 1) → ℝ) volume
    volume

Tactic:
exact (volume_preserving_finTwoArrow ℝ).symm _

Premises used: Real, MeasureTheory.MeasurePreserving.symm, MeasureTheory.volume_preserving_finTwoArrow
-- 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 ℝ ℝ)
⊢ ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), ContinuousOn (![f, g] i) (Set.Icc a b)

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

Premises used: Fin.forall_fin_two, Iff.mpr, 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
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 : ℝ × ℝ
hx : x ∈ interior (Set.Icc a b) \ s
⊢ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s

Tactic:
rw [Icc_prod_eq, interior_prod_eq, interior_Icc, interior_Icc] at hx

Premises used: interior_Icc, interior_prod_eq, Set.Icc_prod_eq
-- 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 : ℝ × ℝ
hx : x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s
⊢ ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), HasFDerivAt (![f, g] i) (![f', g'] i x) x

Tactic:
Fin.forall_fin_two.2 ⟨Hdf x hx, Hdg x hx⟩

Premises used: Fin.forall_fin_two, Iff.mpr, 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
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 : ℝ × ℝ
hx : x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s
⊢ ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), HasFDerivAt (![f, g] i) (![f', g'] i x) x

Tactic:
exact Fin.forall_fin_two.2 ⟨Hdf x hx, Hdg x hx⟩

Premises used: Fin.forall_fin_two, Iff.mpr, 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
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 : ℝ × ℝ
refine_5 :
  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)
⊢ HAdd.hAdd (α := E) (β := E) ((f' x : (a : ℝ × ℝ) → E) (1, 0) : E) ((g' x : (a : ℝ × ℝ) → E) (0, 1) : E) =
    ∑ i : Fin (1 + 1),
      (![f', g'] i x : (a : ℝ × ℝ) → E)
        ((e.symm : (a : Fin (1 + 1) → ℝ) → ℝ × ℝ) (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ ℝ) i 1) :
          ℝ × ℝ)

Tactic:
rw [Fin.sum_univ_two]

Premises used: Fin.sum_univ_two