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) → ℝ) →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)))‖ ≤
    2 * ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
have 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)
Tactic: convert_to ‖g (e (I.lower i) y) - g (e (I.upper i) y)‖ ≤ _
-- 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) → ℝ) →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 (α := 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)‖
have 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)
Tactic: congr 1
-- 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))
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 (α := 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)
have 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)
Tactic: have := Fin.insertNth_sub_same (α := fun _ ↦ ℝ) i (I.upper i) (I.lower i) y
-- 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) → ℝ) →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)
      ((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)
have h : 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: simp only [← this, f'.map_sub]
-- 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))
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)
⊢ ‖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)
have 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)
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
-- 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) → ℝ) →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)
have refine : ‖y - x‖ ≤ 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)
-- 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))
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)
⊢ ‖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)
have 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)
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
Cleared hypotheses: hε
-- 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) → ℝ) →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)‖ ≤
    2 * ε * diam (α := Fin (n + 1) → ℝ) ((Box.Icc : (a : Box (Fin (n + 1))) → Set (Fin (n + 1) → ℝ)) I)
have 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)
Tactic: rw [two_mul, add_mul]
-- 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))
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
⊢ ‖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)‖ ≤
    2 * ε * (↑c : ℝ) * ∏ j : Fin (n + 1), (I.upper j - I.lower j)
have 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)
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))