awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
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 (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)
have h : Set.Icc (a 0) (b 0) =
  (⇑(MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ)) : (a : ℝ) → Fin 1 → ℝ) ⁻¹' Set.Icc a b
Tactic: convert!
          (((volume_preserving_funUnique (Fin 1) ℝ).symm _).setIntegral_preimage_emb
              (MeasurableEquiv.measurableEmbedding _) f _).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (hypothesis)
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 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))) =
    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))
have this : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
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) (∫ (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)
have 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)
Tactic: simp only [intervalIntegral.integral_of_le hle.1, intervalIntegral.integral_of_le hle.2,
        setIntegral_congr_set (Ioc_ae_eq_Icc (α := ℝ) (μ := volume))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
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
⊢ ∫ (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)
have inr : ∀
  (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₁),
  ∫ (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: wlog h₁ : a₁ ≤ b₁ generalizing a₁ b₁
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
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)
⊢ ∫ (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)
have 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)
Tactic: simp only [intervalIntegral.integral_symm b₁ a₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
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)
⊢ -∫ (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)
have inr : -((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)) =
  (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)
Tactic: refine (congr_arg Neg.neg (this Hcf Hcg Hdf Hdg Hi (le_of_not_ge h₁))).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a₂ b₂ : ℝ
s : Set (ℝ × ℝ)
hs : s.Countable
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)
have inr : ∀
  (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₂),
  ∫ (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: wlog h₂ : a₂ ≤ b₂ generalizing a₂ b₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a₂ b₂ : ℝ
s : Set (ℝ × ℝ)
hs : s.Countable
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₁
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 a₁..b₁,
        ∫ (y : ℝ) in b₂..a₂,
          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, a₂)) (∫ (x : ℝ) in a₁..b₁, g (x, b₂)) +
          ∫ (y : ℝ) in b₂..a₂, f (b₁, y)) -
        ∫ (y : ℝ) in b₂..a₂, 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)
have inr : -∫ (x : ℝ) in a₁..b₁,
      ∫ (y : ℝ) in b₂..a₂,
        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 b₂..a₂, f (b₁, y)) -
    -∫ (y : ℝ) in b₂..a₂, f (a₁, y)
Tactic: simp only [intervalIntegral.integral_symm b₂ a₂, intervalIntegral.integral_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a₂ b₂ : ℝ
s : Set (ℝ × ℝ)
hs : s.Countable
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₁
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 a₁..b₁,
        ∫ (y : ℝ) in b₂..a₂,
          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, a₂)) (∫ (x : ℝ) in a₁..b₁, g (x, b₂)) +
          ∫ (y : ℝ) in b₂..a₂, f (b₁, y)) -
        ∫ (y : ℝ) in b₂..a₂, f (a₁, y)
⊢ -∫ (x : ℝ) in a₁..b₁,
        ∫ (y : ℝ) in b₂..a₂,
          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 b₂..a₂, f (b₁, y)) -
      -∫ (y : ℝ) in b₂..a₂, f (a₁, y)
have inr : -((HSub.hSub (α := E) (∫ (x : ℝ) in a₁..b₁, g (x, a₂)) (∫ (x : ℝ) in a₁..b₁, g (x, b₂)) +
        ∫ (y : ℝ) in b₂..a₂, f (b₁, y)) -
      ∫ (y : ℝ) in b₂..a₂, f (a₁, y)) =
  (HSub.hSub (α := E) (∫ (x : ℝ) in a₁..b₁, g (x, b₂)) (∫ (x : ℝ) in a₁..b₁, g (x, a₂)) +
      -∫ (y : ℝ) in b₂..a₂, f (b₁, y)) -
    -∫ (y : ℝ) in b₂..a₂, f (a₁, y)
Tactic: refine (congr_arg Neg.neg (this Hcf Hcg Hdf Hdg Hi (le_of_not_ge h₂))).trans ?_