awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
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 < ε
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
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
g : (y : Fin (n + 1) → ℝ) → E :=
  fun (y : Fin (n + 1) → ℝ) ↦ HSub.hSub (β := E) (f y - a) ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)
hg : g = fun (y : Fin (n + 1) → ℝ) ↦ HSub.hSub (β := E) (f y - a) ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)
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 →
      ‖g y‖ ≤ ε * ‖y - x‖
clear_value :
  ∀ (g : (y : Fin (n + 1) → ℝ) → E)
    (hg : g = fun (y : Fin (n + 1) → ℝ) ↦ HSub.hSub (β := E) (f y - a) ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E))
    (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 →
          ‖g y‖ ≤ ε * ‖y - x‖),
    ‖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)
⊢ ‖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)

Tactic:
clear_value g
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
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 < ε
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
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
g : (y : Fin (n + 1) → ℝ) → E
hg : g = fun (y : Fin (n + 1) → ℝ) ↦ HSub.hSub (β := E) (f y - a) ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)
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 →
      ‖g y‖ ≤ ε * ‖y - x‖
⊢ f = fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y

Tactic:
simp [hg]
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
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 < ε
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
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
g : (y : Fin (n + 1) → ℝ) → E
hg : g = fun (y : Fin (n + 1) → ℝ) ↦ HSub.hSub (β := E) (f y - a) ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)
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 →
      ‖g y‖ ≤ ε * ‖y - x‖
obtain :
  ∀
    (hfc :
      ContinuousOn.{0, u} (Y := E)
        (fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y)
        ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I))
    (Hi :
      ∀ x_1 ∈ Set.Icc (I.lower i) (I.upper i),
        Integrable.{0, u, u} (E := E) (I.face i) ⊥
          ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y) ∘
            e x_1)
          BoxAdditiveMap.volume)
    (hg :
      g = fun (y : Fin (n + 1) → ℝ) ↦
        HSub.hSub (β := E)
          ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y) y -
            a)
          ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)),
    ‖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)
          (HSub.hSub (α := E)
            ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y)
              (e (I.upper i) y))
            ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y)
              (e (I.lower i) y)))‖ ≤
      2 * ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
⊢ ‖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)

Tactic:
obtain rfl : f = fun y => a + f' (y - x) + g y := by simp [hg]

Premises used: HSub.hSub, HAdd.hAdd, DFunLike.coe, rfl
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
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) → ℝ) →L[ℝ] E
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 < ε
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)
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
g : (y : Fin (n + 1) → ℝ) → E
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 →
      ‖g y‖ ≤ ε * ‖y - x‖
hfc :
  ContinuousOn.{0, u} (Y := E)
    (fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y)
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
Hi :
  ∀ x_1 ∈ Set.Icc (I.lower i) (I.upper i),
    Integrable.{0, u, u} (E := E) (I.face i) ⊥
      ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y) ∘ e x_1)
      BoxAdditiveMap.volume
hg :
  g = fun (y : Fin (n + 1) → ℝ) ↦
    HSub.hSub (β := E)
      ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y) y - a)
      ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)
h :
  ‖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)
        (HSub.hSub (α := E)
          ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y)
            (e (I.upper i) y))
          ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y)
            (e (I.lower i) y)))‖ =
    ‖g (e (I.lower i) y) - g (e (I.upper i) y)‖
convert_2 :
  ‖g (e (I.lower i) y) - g (e (I.upper i) y)‖ ≤
    2 * ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
⊢ ‖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)
        (HSub.hSub (α := E)
          ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y)
            (e (I.upper i) y))
          ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y)
            (e (I.lower i) y)))‖ ≤
    2 * ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)

Tactic:
convert_to ‖g (e (I.lower i) y) - g (e (I.upper i) y)‖ ≤ _

Premises used: BoxIntegral.Box.upper, BoxIntegral.Box.lower
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
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) → ℝ) →L[ℝ] E
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 < ε
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)
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
g : (y : Fin (n + 1) → ℝ) → E
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 →
      ‖g y‖ ≤ ε * ‖y - x‖
hfc :
  ContinuousOn.{0, u} (Y := E)
    (fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y)
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
Hi :
  ∀ x_1 ∈ Set.Icc (I.lower i) (I.upper i),
    Integrable.{0, u, u} (E := E) (I.face i) ⊥
      ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y) ∘ e x_1)
      BoxAdditiveMap.volume
hg :
  g = fun (y : Fin (n + 1) → ℝ) ↦
    HSub.hSub (β := E)
      ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y) y - a)
      ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)
h :
  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)
      (HSub.hSub (α := E)
        ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y)
          (e (I.upper i) y))
        ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y)
          (e (I.lower i) y))) =
    g (e (I.lower i) y) - g (e (I.upper i) 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)
        (HSub.hSub (α := E)
          ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y)
            (e (I.upper i) y))
          ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y)
            (e (I.lower i) y)))‖ =
    ‖g (e (I.lower i) y) - g (e (I.upper i) y)‖

Tactic:
congr 1
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
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) → ℝ) →L[ℝ] E
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 < ε
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)
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
g : (y : Fin (n + 1) → ℝ) → E
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 →
      ‖g y‖ ≤ ε * ‖y - x‖
hfc :
  ContinuousOn.{0, u} (Y := E)
    (fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y)
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
Hi :
  ∀ x_1 ∈ Set.Icc (I.lower i) (I.upper i),
    Integrable.{0, u, u} (E := E) (I.face i) ⊥
      ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y) ∘ e x_1)
      BoxAdditiveMap.volume
hg :
  g = fun (y : Fin (n + 1) → ℝ) ↦
    HSub.hSub (β := E)
      ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y) y - a)
      ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)
⊢ HSub.hSub (α := (j : Fin (n + 1)) → ℝ) (i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ) (I.upper i) y)
      (i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ) (I.lower i) y) =
    Pi.single (M := fun (x : Fin (n + 1)) ↦ ℝ) i (I.upper i - I.lower i)

Tactic:
have := Fin.insertNth_sub_same (α := fun _ ↦ ℝ) i (I.upper i) (I.lower i) y
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
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) → ℝ) →L[ℝ] E
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 < ε
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)
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
g : (y : Fin (n + 1) → ℝ) → E
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 →
      ‖g y‖ ≤ ε * ‖y - x‖
hfc :
  ContinuousOn.{0, u} (Y := E)
    (fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y)
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
Hi :
  ∀ x_1 ∈ Set.Icc (I.lower i) (I.upper i),
    Integrable.{0, u, u} (E := E) (I.face i) ⊥
      ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y) ∘ e x_1)
      BoxAdditiveMap.volume
hg :
  g = fun (y : Fin (n + 1) → ℝ) ↦
    HSub.hSub (β := E)
      ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y) y - a)
      ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)
this :
  HSub.hSub (α := (j : Fin (n + 1)) → ℝ) (i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ) (I.upper i) y)
      (i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ) (I.lower i) y) =
    Pi.single (M := fun (x : Fin (n + 1)) ↦ ℝ) i (I.upper i - I.lower i)
⊢ HSub.hSub (α := E) (β := E)
        ((f' : (a : Fin (n + 1) → ℝ) → E) (i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ) (I.upper i) y) : E)
        ((f' : (a : Fin (n + 1) → ℝ) → E) (i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ) (I.lower i) y) : E) -
      (a +
            HSub.hSub (α := E) (β := E) ((f' : (a : Fin (n + 1) → ℝ) → E) (e (I.upper i) y) : E)
              ((f' : (a : Fin (n + 1) → ℝ) → E) x : E) +
          g (e (I.upper i) y) -
        (a +
            HSub.hSub (α := E) (β := E) ((f' : (a : Fin (n + 1) → ℝ) → E) (e (I.lower i) y) : E)
              ((f' : (a : Fin (n + 1) → ℝ) → E) x : E) +
          g (e (I.lower i) y))) =
    g (e (I.lower i) y) - g (e (I.upper i) y)

Tactic:
abel
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
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) → ℝ) →L[ℝ] E
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 < ε
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)
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
g : (y : Fin (n + 1) → ℝ) → E
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 →
      ‖g y‖ ≤ ε * ‖y - x‖
hfc :
  ContinuousOn.{0, u} (Y := E)
    (fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y)
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
Hi :
  ∀ x_1 ∈ Set.Icc (I.lower i) (I.upper i),
    Integrable.{0, u, u} (E := E) (I.face i) ⊥
      ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y) ∘ e x_1)
      BoxAdditiveMap.volume
hg :
  g = fun (y : Fin (n + 1) → ℝ) ↦
    HSub.hSub (β := E)
      ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y) y - a)
      ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)
⊢ ∀ z ∈ Set.Icc (I.lower i) (I.upper i),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
      ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) (e z y)

Tactic:
have : ∀ z ∈ Icc (I.lower i) (I.upper i), e z y ∈ (Box.Icc I) := fun z hz =>
        I.mapsTo_insertNth_face_Icc hz hy
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
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) → ℝ) →L[ℝ] E
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 < ε
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)
y_1 : Fin n → ℝ
hy_1 :
  Membership.mem (γ := Set (Fin n → ℝ)) ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i) : Set (Fin n → ℝ))
    y_1
g : (y : Fin (n + 1) → ℝ) → E
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 →
      ‖g y‖ ≤ ε * ‖y - x‖
hfc :
  ContinuousOn.{0, u} (Y := E)
    (fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y)
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
Hi :
  ∀ x_1 ∈ Set.Icc (I.lower i) (I.upper i),
    Integrable.{0, u, u} (E := E) (I.face i) ⊥
      ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y) ∘ e x_1)
      BoxAdditiveMap.volume
hg :
  g = fun (y : Fin (n + 1) → ℝ) ↦
    HSub.hSub (β := E)
      ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y) y - a)
      ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)
this :
  ∀ z ∈ Set.Icc (I.lower i) (I.upper i),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
      ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) (e z y_1)
y : Fin (n + 1) → ℝ
hy :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) y
⊢ ‖g y‖ ≤ ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)

Tactic:
(hε y hy).trans (mul_le_mul_of_nonneg_left ?_ h0.le)

Premises used: LT.lt.le, LE.le.trans, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem
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) → ℝ) →L[ℝ] E
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 < ε
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)
y_1 : Fin n → ℝ
hy_1 :
  Membership.mem (γ := Set (Fin n → ℝ)) ((Box.Icc : (a : Box (Fin n)) → Set (Fin n → ℝ)) (I.face i) : Set (Fin n → ℝ))
    y_1
g : (y : Fin (n + 1) → ℝ) → E
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 →
      ‖g y‖ ≤ ε * ‖y - x‖
hfc :
  ContinuousOn.{0, u} (Y := E)
    (fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y)
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
Hi :
  ∀ x_1 ∈ Set.Icc (I.lower i) (I.upper i),
    Integrable.{0, u, u} (E := E) (I.face i) ⊥
      ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y) ∘ e x_1)
      BoxAdditiveMap.volume
hg :
  g = fun (y : Fin (n + 1) → ℝ) ↦
    HSub.hSub (β := E)
      ((fun (y : Fin (n + 1) → ℝ) ↦ HAdd.hAdd (β := E) a ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E) + g y) y - a)
      ((f' : (a : Fin (n + 1) → ℝ) → E) (y - x) : E)
this :
  ∀ z ∈ Set.Icc (I.lower i) (I.upper i),
    Membership.mem (γ := Set (Fin (n + 1) → ℝ))
      ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) (e z y_1)
y : Fin (n + 1) → ℝ
hy :
  Membership.mem (γ := Set (Fin (n + 1) → ℝ))
    ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I : Set (Fin (n + 1) → ℝ)) y
refine : ‖y - x‖ ≤ diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
⊢ ‖g y‖ ≤ ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)

Tactic:
refine (hε y hy).trans (mul_le_mul_of_nonneg_left ?_ h0.le)

Premises used: LT.lt.le, LE.le.trans, mul_le_mul_of_nonneg_left