awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
x : Fin (n + 1) → ℝ
hxI :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) x
a : E
ε : ℝ
h0 : 0 < ε
hε :
  ∀ (y : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) y →
      ‖HSub.hSub (β := E) (f y - a) ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ)
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
Hi : ∀ x ∈ Set.Icc (I.lower i) (I.upper i), Integrable (I.face i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
this :
  ∀ (y : Fin n → ℝ),
    Membership.mem (γ := Set (Fin n → ℝ)) ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i) : Set (Fin n → ℝ))
        y →
      ‖HSub.hSub (α := E)
            ((f' : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i (I.upper i - I.lower i)) :
              E)
            (f (e (I.upper i) y) - f (e (I.lower i) y))‖ ≤
        2 * ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
⊢ ‖HSMul.hSMul (α := ℝ) (β := E) (∏ j : Fin (n + 1), (I.upper j - I.lower j))
          ((f' : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : E) -
        (integral (I.face i) ⊥ (f ∘ e (I.upper i)) BoxAdditiveMap.volume -
          integral (I.face i) ⊥ (f ∘ e (I.lower i)) BoxAdditiveMap.volume)‖ =
    norm.{u} (E := E)
      (integral (I.face i) ⊥
        (fun (x : Fin n → ℝ) ↦
          HSub.hSub (α := E)
            ((f' : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i (I.upper i - I.lower i)) :
              E)
            (f (e (I.upper i) x) - f (e (I.lower i) x)))
        BoxAdditiveMap.volume)
have rw : ‖integral (I.face i) ⊥
      ((fun (x : Fin n → ℝ) ↦
          HSMul.hSMul (β := E) (I.upper i - I.lower i)
            ((f' : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : E)) -
        (f ∘ e (I.upper i) - f ∘ e (I.lower i)))
      BoxAdditiveMap.volume‖ =
  norm.{u} (E := E)
    (integral (I.face i) ⊥
      (fun (x : Fin n → ℝ) ↦
        HSub.hSub (α := E)
          ((f' : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i (I.upper i - I.lower i)) : E)
          (f (e (I.upper i) x) - f (e (I.lower i) x)))
      BoxAdditiveMap.volume)
Tactic: rw [← integral_sub (Hi _ Hu) (Hi _ Hl), ← Box.volume_face_mul i, mul_smul, ← Box.volume_apply,
        ← BoxAdditiveMap.toSMul_apply, ← integral_const, ← BoxAdditiveMap.volume,
        ← integral_sub (integrable_const _) ((Hi _ Hu).sub (Hi _ Hl))]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
x : Fin (n + 1) → ℝ
hxI :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) x
a : E
ε : ℝ
h0 : 0 < ε
hε :
  ∀ (y : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) y →
      ‖HSub.hSub (β := E) (f y - a) ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ)
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
Hi : ∀ x ∈ Set.Icc (I.lower i) (I.upper i), Integrable (I.face i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
this :
  ∀ (y : Fin n → ℝ),
    Membership.mem (γ := Set (Fin n → ℝ)) ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i) : Set (Fin n → ℝ))
        y →
      ‖HSub.hSub (α := E)
            ((f' : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i (I.upper i - I.lower i)) :
              E)
            (f (e (I.upper i) y) - f (e (I.lower i) y))‖ ≤
        2 * ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
⊢ norm.{u} (E := E)
      (integral (I.face i) ⊥
        (fun (x : Fin n → ℝ) ↦
          HSub.hSub (α := E)
            ((f' : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i (I.upper i - I.lower i)) :
              E)
            (f (e (I.upper i) x) - f (e (I.lower i) x)))
        BoxAdditiveMap.volume) ≤
    ENNReal.toReal ((volume : (a : Set (Fin n → ℝ)) → ℝ≥0∞) (↑(I.face i) : Set (Fin n → ℝ))) *
      (2 * ε * (↑c : ℝ) * (I.upper i - I.lower i))
have refine : ∀ (y : Fin n → ℝ)
  (hy :
    Membership.mem (γ := Set (Fin n → ℝ)) ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i) : Set (Fin n → ℝ))
      y),
  2 * ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) ≤
    2 * ε * (↑c : ℝ) * (I.upper i - I.lower i)
Tactic: refine norm_integral_le_of_le_const (fun y hy => (this y hy).trans ?_) volume
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
x : Fin (n + 1) → ℝ
hxI :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) x
a : E
ε : ℝ
h0 : 0 < ε
hε :
  ∀ (y : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) y →
      ‖HSub.hSub (β := E) (f y - a) ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ)
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
Hi : ∀ x ∈ Set.Icc (I.lower i) (I.upper i), Integrable (I.face i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
this :
  ∀ (y : Fin n → ℝ),
    Membership.mem (γ := Set (Fin n → ℝ)) ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i) : Set (Fin n → ℝ))
        y →
      ‖HSub.hSub (α := E)
            ((f' : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i (I.upper i - I.lower i)) :
              E)
            (f (e (I.upper i) y) - f (e (I.lower i) y))‖ ≤
        2 * ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
y : Fin n → ℝ
hy :
  Membership.mem (γ := Set (Fin n → ℝ)) ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i) : Set (Fin n → ℝ)) y
⊢ 2 * ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) ≤
    2 * ε * (↑c : ℝ) * (I.upper i - I.lower i)
have rw : 2 * ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) ≤
  2 * ε * ((↑c : ℝ) * (I.upper i - I.lower i))
Tactic: rw [mul_assoc (2 * ε)]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
x : Fin (n + 1) → ℝ
hxI :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) x
a : E
ε : ℝ
h0 : 0 < ε
hε :
  ∀ (y : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) y →
      ‖HSub.hSub (β := E) (f y - a) ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ)
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
Hi : ∀ x ∈ Set.Icc (I.lower i) (I.upper i), Integrable (I.face i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
this :
  ∀ (y : Fin n → ℝ),
    Membership.mem (γ := Set (Fin n → ℝ)) ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i) : Set (Fin n → ℝ))
        y →
      ‖HSub.hSub (α := E)
            ((f' : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i (I.upper i - I.lower i)) :
              E)
            (f (e (I.upper i) y) - f (e (I.lower i) y))‖ ≤
        2 * ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
y : Fin n → ℝ
hy :
  Membership.mem (γ := Set (Fin n → ℝ)) ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i) : Set (Fin n → ℝ)) y
⊢ 2 * ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) ≤
    2 * ε * ((↑c : ℝ) * (I.upper i - I.lower i))
have hbc : diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) ≤
  (↑c : ℝ) * (I.upper i - I.lower i)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
x : Fin (n + 1) → ℝ
hxI :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) x
a : E
ε : ℝ
h0 : 0 < ε
hε :
  ∀ (y : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) y →
      ‖HSub.hSub (β := E) (f y - a) ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ)
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
Hi : ∀ x ∈ Set.Icc (I.lower i) (I.upper i), Integrable (I.face i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
this :
  ∀ (y : Fin n → ℝ),
    Membership.mem (γ := Set (Fin n → ℝ)) ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i) : Set (Fin n → ℝ))
        y →
      ‖HSub.hSub (α := E)
            ((f' : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i (I.upper i - I.lower i)) :
              E)
            (f (e (I.upper i) y) - f (e (I.lower i) y))‖ ≤
        2 * ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
⊢ ENNReal.toReal ((volume : (a : Set (Fin n → ℝ)) → ℝ≥0∞) (↑(I.face i) : Set (Fin n → ℝ))) *
      (2 * ε * (↑c : ℝ) * (I.upper i - I.lower i)) =
    2 * ε * (↑c : ℝ) * ∏ j : Fin (n + 1), (I.upper j - I.lower j)
have rw : (∏ i_1 : Fin n, ((I.face i).upper i_1 - (I.face i).lower i_1)) * (2 * ε * (↑c : ℝ) * (I.upper i - I.lower i)) =
  2 * ε * (↑c : ℝ) * ((∏ j : Fin n, ((I.face i).upper j - (I.face i).lower j)) * (I.upper i - I.lower i))
Tactic: rw [← measureReal_def, ← Measure.toBoxAdditive_apply, Box.volume_apply,
        ← I.volume_face_mul i]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
Hd :
  ∀ (x : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      HasFDerivWithinAt f (f' x) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
i : Fin (n + 1)
x : Fin (n + 1) → ℝ
hx :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) x
⊢ ContinuousWithinAt f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
have pos : ∀ (hxs : x ∈ s), ContinuousWithinAt f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
Tactic: by_cases hxs : x ∈ s
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
Hd :
  ∀ (x : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      HasFDerivWithinAt f (f' x) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
i : Fin (n + 1)
x : Fin (n + 1) → ℝ
hx :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) x
pos : ∀ (hxs : x ∈ s), ContinuousWithinAt f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
⊢ ContinuousWithinAt f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
have neg : ∀ (hxs : x ∉ s), ContinuousWithinAt f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
Tactic: by_cases hxs : x ∈ s
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.DivergenceTheorem (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
Hd :
  ∀ (x : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      HasFDerivWithinAt f (f' x) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
i : Fin (n + 1)
⊢ HasIntegral I GP
    (fun (x : Fin (n + 1) → ℝ) ↦ (f' x : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1))
    BoxAdditiveMap.volume
    (HSub.hSub (α := E)
      (integral (I.face i) GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.upper i) x))
        BoxAdditiveMap.volume)
      (integral (I.face i) GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.lower i) x))
        BoxAdditiveMap.volume))
have Hc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
Tactic: have Hc : ContinuousOn f (Box.Icc I) := fun x hx ↦ by
    by_cases hxs : x ∈ s
    exacts [Hs x hxs, (Hd x ⟨hx, hxs⟩).continuousWithinAt]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
Hd :
  ∀ (x : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      HasFDerivWithinAt f (f' x) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
i : Fin (n + 1)
Hc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
fI : ℝ → Box (Fin n) → E :=
  fun (y : ℝ) (J : Box (Fin n)) ↦
    integral J GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) y x)) BoxAdditiveMap.volume
fb : (↑(Set.Icc (I.lower i) (I.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I.face i) : WithTop (Box (Fin n)))] E :=
  fun (x : (↑(Set.Icc (I.lower i) (I.upper i)) : Type)) ↦
    Integrable.toBoxAdditive (vol := BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) ⋯
F : Fin (n + 1) →ᵇᵃ[(↑I : WithTop (Box (Fin (n + 1))))] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
⊢ HasIntegral I GP
    (fun (x : Fin (n + 1) → ℝ) ↦ (f' x : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1))
    BoxAdditiveMap.volume
    (HSub.hSub (α := E)
      (integral (I.face i) GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.upper i) x))
        BoxAdditiveMap.volume)
      (integral (I.face i) GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) (I.lower i) x))
        BoxAdditiveMap.volume))
have change : HasIntegral (E := E) (F := E) I GP
  (fun (x : Fin (n + 1) → ℝ) ↦
    ((f' x : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : E))
  (BoxAdditiveMap.volume : Fin (n + 1) →ᵇᵃ[⊤] E →L[ℝ] E) ((F : (a : Box (Fin (n + 1))) → E) I : E)
Tactic: change HasIntegral I GP (fun x => f' x (Pi.single i 1)) _ (F I)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
Hd :
  ∀ (x : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      HasFDerivWithinAt f (f' x) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
i : Fin (n + 1)
Hc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
fI : ℝ → Box (Fin n) → E :=
  fun (y : ℝ) (J : Box (Fin n)) ↦
    integral J GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) y x)) BoxAdditiveMap.volume
fb : (↑(Set.Icc (I.lower i) (I.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I.face i) : WithTop (Box (Fin n)))] E :=
  fun (x : (↑(Set.Icc (I.lower i) (I.upper i)) : Type)) ↦
    Integrable.toBoxAdditive (vol := BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) ⋯
F : Fin (n + 1) →ᵇᵃ[(↑I : WithTop (Box (Fin (n + 1))))] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
⊢ HasIntegral (E := E) (F := E) I GP
    (fun (x : Fin (n + 1) → ℝ) ↦
      ((f' x : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : E))
    (BoxAdditiveMap.volume : Fin (n + 1) →ᵇᵃ[⊤] E →L[ℝ] E) ((F : (a : Box (Fin (n + 1))) → E) I : E)
have refine_1 : Fin (n + 1) →ᵇᵃ[(↑I : WithTop (Box (Fin (n + 1))))] ℝ
Tactic: refine HasIntegral.of_le_Henstock_of_forall_isLittleO gp_le ?_ ?_ _ s hs ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.DivergenceTheorem (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
inst_2 : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
Hd :
  ∀ (x : Fin (n + 1) → ℝ),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I \ s : Set (Fin (n + 1) → ℝ)) x →
      HasFDerivWithinAt f (f' x) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) x
i : Fin (n + 1)
Hc : ContinuousOn f ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
fI : ℝ → Box (Fin n) → E :=
  fun (y : ℝ) (J : Box (Fin n)) ↦
    integral J GP (fun (x : Fin n → ℝ) ↦ f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) y x)) BoxAdditiveMap.volume
fb : (↑(Set.Icc (I.lower i) (I.upper i)) : Type) → Fin n →ᵇᵃ[(↑(I.face i) : WithTop (Box (Fin n)))] E :=
  fun (x : (↑(Set.Icc (I.lower i) (I.upper i)) : Type)) ↦
    Integrable.toBoxAdditive (vol := BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) ⋯
F : Fin (n + 1) →ᵇᵃ[(↑I : WithTop (Box (Fin (n + 1))))] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
refine_1 : Fin (n + 1) →ᵇᵃ[(↑I : WithTop (Box (Fin (n + 1))))] ℝ
⊢ HasIntegral (E := E) (F := E) I GP
    (fun (x : Fin (n + 1) → ℝ) ↦
      ((f' x : (a : Fin (n + 1) → ℝ) → E) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : E))
    (BoxAdditiveMap.volume : Fin (n + 1) →ᵇᵃ[⊤] E →L[ℝ] E) ((F : (a : Box (Fin (n + 1))) → E) I : E)
have refine_2 : ∀ (J : Box (Fin (n + 1))),
  LE.le (α := ℝ) (0 : ℝ)
    ((BoxAdditiveMap.restrict (Measure.toBoxAdditive volume) (↑I : WithTop (Box (Fin (n + 1)))) sorry :
          (a : Box (Fin (n + 1))) → ℝ)
        J :
      ℝ)
Tactic: refine HasIntegral.of_le_Henstock_of_forall_isLittleO gp_le ?_ ?_ _ s hs ?_ ?_