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) → ℝ) →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
⊢ dist y x ≤ diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)

Tactic:
dist_le_diam_of_mem I.isCompact_Icc.isBounded hy hxI

Premises used: IsCompact.isBounded, BoxIntegral.Box.isCompact_Icc, Metric.dist_le_diam_of_mem
-- 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
⊢ dist y x ≤ diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)

Tactic:
exact dist_le_diam_of_mem I.isCompact_Icc.isBounded hy hxI

Premises used: IsCompact.isBounded, BoxIntegral.Box.isCompact_Icc, Metric.dist_le_diam_of_mem
-- 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 :
  ∀ 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)
⊢ ∀ (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‖ ≤ ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)

Tactic:
replace hε : ∀ y ∈ (Box.Icc I), ‖g y‖ ≤ ε * diam (Box.Icc I) := by
        intro y hy
        refine (hε y hy).trans (mul_le_mul_of_nonneg_left ?_ h0.le)
        rw [← dist_eq_norm]
        exact dist_le_diam_of_mem I.isCompact_Icc.isBounded hy hxI
-- 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
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)
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‖ ≤ ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
convert_2 :
  ‖g (e (I.lower i) y) - g (e (I.upper i) y)‖ ≤
    ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) +
      ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
⊢ ‖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)

Tactic:
rw [two_mul, add_mul]

Premises used: add_mul, two_mul
-- 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
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)
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‖ ≤ ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
⊢ ‖g (e (I.lower i) y) - g (e (I.upper i) y)‖ ≤
    ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) +
      ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)

Tactic:
norm_sub_le_of_le (hε _ (this _ Hl)) (hε _ (this _ Hu))

Premises used: norm_sub_le_of_le
-- 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
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)
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‖ ≤ ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
⊢ ‖g (e (I.lower i) y) - g (e (I.upper i) y)‖ ≤
    ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I) +
      ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)

Tactic:
exact norm_sub_le_of_le (hε _ (this _ Hl)) (hε _ (this _ Hu))

Premises used: norm_sub_le_of_le
-- 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 < ε
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
⊢ ∀ (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)

Tactic:
have : ∀ y ∈ Box.Icc (I.face i),
      ‖f' (Pi.single i (I.upper i - I.lower i)) -
          (f (e (I.upper i) y) - f (e (I.lower i) y))‖ ≤
        2 * ε * diam (Box.Icc I) := fun y hy ↦ by
    set g := fun y => f y - a - f' (y - x) with hg
    change ∀ y ∈ (Box.Icc I), ‖g y‖ ≤ ε * ‖y - x‖ at hε
    clear_value g; obtain rfl : f = fun y => a + f' (y - x) + g y := by simp [hg]
    convert_to ‖g (e (I.lower i) y) - g (e (I.upper i) y)‖ ≤ _
    · congr 1
      have := Fin.insertNth_sub_same (α := fun _ ↦ ℝ) i (I.upper i) (I.lower i) y
      simp only [← this, f'.map_sub]; abel
    · 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
      replace hε : ∀ y ∈ (Box.Icc I), ‖g y‖ ≤ ε * diam (Box.Icc I) := by
        intro y hy
        refine (hε y hy).trans (mul_le_mul_of_nonneg_left ?_ h0.le)
        rw [← dist_eq_norm]
        exact dist_le_diam_of_mem I.isCompact_Icc.isBounded hy hxI
      rw [two_mul, add_mul]
      exact norm_sub_le_of_le (hε _ (this _ Hl)) (hε _ (this _ Hu))
-- 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 < ε
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)
⊢ ‖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:
simp only [(· ∘ ·), Pi.sub_def, ← f'.map_smul, ← Pi.single_smul', smul_eq_mul, mul_one]

Premises used: Function.comp, Pi.sub_def, Pi.single_smul', smul_eq_mul, mul_one, ContinuousLinearMap.map_smul
-- 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 < ε
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))

Tactic:
norm_integral_le_of_le_const (fun y hy => (this y hy).trans ?_) volume

Premises used: MeasureTheory.Measure.real, BoxIntegral.norm_integral_le_of_le_const, MeasureTheory.MeasureSpace.volume, BoxIntegral.BoxAdditiveMap.volume, LE.le.trans
-- 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 < ε
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)
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)
⊢ 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))

Tactic:
refine norm_integral_le_of_le_const (fun y hy => (this y hy).trans ?_) volume

Premises used: BoxIntegral.norm_integral_le_of_le_const, MeasureTheory.MeasureSpace.volume, LE.le.trans