awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this_1 : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' →
      ∀ (z : E),
        dist z (a, x).2 < r' →
          ‖f (a, x).1 z - f (a, x).1 y -
                HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
            s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b : ℝ
b_lt : b < s * r
hb :
  ∀ y ∈ closedBall x t,
    ∀ z ∈ closedBall x t,
      ‖f a z - f a y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ ≤ b
ε : ℝ
εpos : 0 < ε
hε : b + 2 * ε < s * r
u : Set α
u_open : IsOpen[inst_6] u
au : a ∈ u
hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)
a' : α
x' : E
ha'x' : a' ∈ u ∧ dist x' x < t - t'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
⊢ dist (f a' z) (f a z) ≤ ε
have h₁ : dist (Function.uncurry f (a', z)) (Function.uncurry f (a, z)) ≤ ε
Tactic: change dist (f.uncurry (a', z)) (f.uncurry (a, z)) ≤ ε
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this_1 : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' →
      ∀ (z : E),
        dist z (a, x).2 < r' →
          ‖f (a, x).1 z - f (a, x).1 y -
                HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
            s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b : ℝ
b_lt : b < s * r
hb :
  ∀ y ∈ closedBall x t,
    ∀ z ∈ closedBall x t,
      ‖f a z - f a y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ ≤ b
ε : ℝ
εpos : 0 < ε
hε : b + 2 * ε < s * r
u : Set α
u_open : IsOpen[inst_6] u
au : a ∈ u
hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)
a' : α
x' : E
ha'x' : a' ∈ u ∧ dist x' x < t - t'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
⊢ dist (Function.uncurry f (a', z)) (Function.uncurry f (a, z)) ≤ ε
have apply : (a', z).1 ∈ u
Tactic: apply (hu _ _ _).le
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this_1 : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' →
      ∀ (z : E),
        dist z (a, x).2 < r' →
          ‖f (a, x).1 z - f (a, x).1 y -
                HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
            s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b : ℝ
b_lt : b < s * r
hb :
  ∀ y ∈ closedBall x t,
    ∀ z ∈ closedBall x t,
      ‖f a z - f a y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ ≤ b
ε : ℝ
εpos : 0 < ε
hε : b + 2 * ε < s * r
u : Set α
u_open : IsOpen[inst_6] u
au : a ∈ u
hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)
a' : α
x' : E
ha'x' : a' ∈ u ∧ dist x' x < t - t'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
apply : (a', z).1 ∈ u
⊢ dist (Function.uncurry f (a', z)) (Function.uncurry f (a, z)) ≤ ε
have apply₁ : (a', z).2 ∈ closedBall x t
Tactic: apply (hu _ _ _).le
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this_1 : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' →
      ∀ (z : E),
        dist z (a, x).2 < r' →
          ‖f (a, x).1 z - f (a, x).1 y -
                HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
            s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b : ℝ
b_lt : b < s * r
hb :
  ∀ y ∈ closedBall x t,
    ∀ z ∈ closedBall x t,
      ‖f a z - f a y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ ≤ b
ε : ℝ
εpos : 0 < ε
hε : b + 2 * ε < s * r
u : Set α
u_open : IsOpen[inst_6] u
au : a ∈ u
hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)
a' : α
x' : E
ha'x' : a' ∈ u ∧ dist x' x < t - t'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
⊢ ‖f a y - f a' y‖ ≤ ε
have h₁ : dist (f a' y) (f a y) ≤ ε
Tactic: rw [← dist_eq_norm']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this_1 : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' →
      ∀ (z : E),
        dist z (a, x).2 < r' →
          ‖f (a, x).1 z - f (a, x).1 y -
                HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
            s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b : ℝ
b_lt : b < s * r
hb :
  ∀ y ∈ closedBall x t,
    ∀ z ∈ closedBall x t,
      ‖f a z - f a y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ ≤ b
ε : ℝ
εpos : 0 < ε
hε : b + 2 * ε < s * r
u : Set α
u_open : IsOpen[inst_6] u
au : a ∈ u
hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)
a' : α
x' : E
ha'x' : a' ∈ u ∧ dist x' x < t - t'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
⊢ dist (f a' y) (f a y) ≤ ε
have h₁ : dist (Function.uncurry f (a', y)) (Function.uncurry f (a, y)) ≤ ε
Tactic: change dist (f.uncurry (a', y)) (f.uncurry (a, y)) ≤ ε
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this_1 : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' →
      ∀ (z : E),
        dist z (a, x).2 < r' →
          ‖f (a, x).1 z - f (a, x).1 y -
                HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
            s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b : ℝ
b_lt : b < s * r
hb :
  ∀ y ∈ closedBall x t,
    ∀ z ∈ closedBall x t,
      ‖f a z - f a y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ ≤ b
ε : ℝ
εpos : 0 < ε
hε : b + 2 * ε < s * r
u : Set α
u_open : IsOpen[inst_6] u
au : a ∈ u
hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)
a' : α
x' : E
ha'x' : a' ∈ u ∧ dist x' x < t - t'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
⊢ dist (Function.uncurry f (a', y)) (Function.uncurry f (a, y)) ≤ ε
have apply : (a', y).1 ∈ u
Tactic: apply (hu _ _ _).le
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this_1 : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' →
      ∀ (z : E),
        dist z (a, x).2 < r' →
          ‖f (a, x).1 z - f (a, x).1 y -
                HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
            s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b : ℝ
b_lt : b < s * r
hb :
  ∀ y ∈ closedBall x t,
    ∀ z ∈ closedBall x t,
      ‖f a z - f a y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ ≤ b
ε : ℝ
εpos : 0 < ε
hε : b + 2 * ε < s * r
u : Set α
u_open : IsOpen[inst_6] u
au : a ∈ u
hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)
a' : α
x' : E
ha'x' : a' ∈ u ∧ dist x' x < t - t'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
apply : (a', y).1 ∈ u
⊢ dist (Function.uncurry f (a', y)) (Function.uncurry f (a, y)) ≤ ε
have apply₁ : (a', y).2 ∈ closedBall x t
Tactic: apply (hu _ _ _).le
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this_1 : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' →
      ∀ (z : E),
        dist z (a, x).2 < r' →
          ‖f (a, x).1 z - f (a, x).1 y -
                HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
            s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b : ℝ
b_lt : b < s * r
hb :
  ∀ y ∈ closedBall x t,
    ∀ z ∈ closedBall x t,
      ‖f a z - f a y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ ≤ b
ε : ℝ
εpos : 0 < ε
hε : b + 2 * ε < s * r
u : Set α
u_open : IsOpen[inst_6] u
au : a ∈ u
hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)
a' : α
x' : E
ha'x' : a' ∈ u ∧ dist x' x < t - t'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
⊢ ε + ε + b < s * r
have linarith : s * r ≤ ε + ε + b → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this_1 : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' →
      ∀ (z : E),
        dist z (a, x).2 < r' →
          ‖f (a, x).1 z - f (a, x).1 y -
                HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
            s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b : ℝ
b_lt : b < s * r
hb :
  ∀ y ∈ closedBall x t,
    ∀ z ∈ closedBall x t,
      ‖f a z - f a y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ ≤ b
ε : ℝ
εpos : 0 < ε
hε : b + 2 * ε < s * r
u : Set α
u_open : IsOpen[inst_6] u
au : a ∈ u
hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)
a' : α
x' : E
ha'x' : a' ∈ u ∧ dist x' x < t - t'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
linarith : s * r ≤ ε + ε + b → 2 / 2 = 1
⊢ ε + ε + b < s * r
have linarith₁ : s * r ≤ ε + ε + b → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this_1 : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' →
      ∀ (z : E),
        dist z (a, x).2 < r' →
          ‖f (a, x).1 z - f (a, x).1 y -
                HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
            s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b : ℝ
b_lt : b < s * r
hb :
  ∀ y ∈ closedBall x t,
    ∀ z ∈ closedBall x t,
      ‖f a z - f a y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ ≤ b
ε : ℝ
εpos : 0 < ε
hε : b + 2 * ε < s * r
u : Set α
u_open : IsOpen[inst_6] u
au : a ∈ u
hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)
a' : α
x' : E
ha'x' : a' ∈ u ∧ dist x' x < t - t'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
linarith : s * r ≤ ε + ε + b → 2 / 2 = 1
linarith₁ : s * r ≤ ε + ε + b → HMul.hMul (α := ℝ) 1 2 = 2
⊢ ε + ε + b < s * r
have linarith₂ : s * r ≤ ε + ε + b → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this_1 : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' →
      ∀ (z : E),
        dist z (a, x).2 < r' →
          ‖f (a, x).1 z - f (a, x).1 y -
                HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
            s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b : ℝ
b_lt : b < s * r
hb :
  ∀ y ∈ closedBall x t,
    ∀ z ∈ closedBall x t,
      ‖f a z - f a y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ ≤ b
ε : ℝ
εpos : 0 < ε
hε : b + 2 * ε < s * r
u : Set α
u_open : IsOpen[inst_6] u
au : a ∈ u
hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)
a' : α
x' : E
ha'x' : a' ∈ u ∧ dist x' x < t - t'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
linarith : s * r ≤ ε + ε + b → 2 / 2 = 1
linarith₁ : s * r ≤ ε + ε + b → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : s * r ≤ ε + ε + b → GT.gt (α := ℝ) 2 0
linarith₃ : s * r ≤ ε + ε + b → 2 / 2 = 1
linarith₄ : s * r ≤ ε + ε + b → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : s * r ≤ ε + ε + b → GT.gt (α := ℝ) 2 0
linarith₆ : s * r ≤ ε + ε + b → 2 / 2 = 1
linarith₇ : s * r ≤ ε + ε + b → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : s * r ≤ ε + ε + b → GT.gt (α := ℝ) 2 0
⊢ ε + ε + b < s * r
have linarith₉ : s * r ≤ ε + ε + b → b + 2 * ε - s * r + (s * r - (ε + ε + b)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this_1 : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' →
      ∀ (z : E),
        dist z (a, x).2 < r' →
          ‖f (a, x).1 z - f (a, x).1 y -
                HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
            s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b : ℝ
b_lt : b < s * r
hb :
  ∀ y ∈ closedBall x t,
    ∀ z ∈ closedBall x t,
      ‖f a z - f a y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ ≤ b
ε : ℝ
εpos : 0 < ε
hε : b + 2 * ε < s * r
u : Set α
u_open : IsOpen[inst_6] u
au : a ∈ u
hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)
a' : α
x' : E
ha'x' : a' ∈ u ∧ dist x' x < t - t'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
⊢ ‖f (a', x').1 z - f (a', x').1 y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
    s * r
have a'₁ : ‖f a' z - f a' y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ =
  ‖f a' z - f a z + (f a y - f a' y) +
      (f a z - f a y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F))‖
Tactic: calc
  ‖f a' z - f a' y - (L z - L y)‖ =
    ‖(f a' z - f a z) + (f a y - f a' y) + (f a z - f a y - (L z - L y))‖ := by congr; abel
  _ ≤ ‖f a' z - f a z‖ + ‖f a y - f a' y‖ + ‖f a z - f a y - (L z - L y)‖ := norm_add₃_le
  _ ≤ ε + ε + b := by
      gcongr
      · rw [← dist_eq_norm]
        change dist (f.uncurry (a', z)) (f.uncurry (a, z)) ≤ ε
        apply (hu _ _ _).le
        · exact ha'x'.1
        · simp [dzx]
      · rw [← dist_eq_norm']
        change dist (f.uncurry (a', y)) (f.uncurry (a, y)) ≤ ε
        apply (hu _ _ _).le
        · exact ha'x'.1
        · simp [dyx]
      · simp [hb, dyx, dzx]
  _ < s * r := by linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this_1 : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' →
      ∀ (z : E),
        dist z (a, x).2 < r' →
          ‖f (a, x).1 z - f (a, x).1 y -
                HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
            s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b : ℝ
b_lt : b < s * r
hb :
  ∀ y ∈ closedBall x t,
    ∀ z ∈ closedBall x t,
      ‖f a z - f a y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ ≤ b
ε : ℝ
εpos : 0 < ε
hε : b + 2 * ε < s * r
u : Set α
u_open : IsOpen[inst_6] u
au : a ∈ u
hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)
a' : α
x' : E
ha'x' : a' ∈ u ∧ dist x' x < t - t'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
a'₁ :
  ‖f a' z - f a' y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ =
    ‖f a' z - f a z + (f a y - f a' y) +
        (f a z - f a y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F))‖
⊢ ‖f (a', x').1 z - f (a', x').1 y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
    s * r
have a'₂ : ‖f a' z - f a z‖ + ‖f a y - f a' y‖ +
    ‖f a z - f a y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ ≤
  ε + ε + b
Tactic: calc
  ‖f a' z - f a' y - (L z - L y)‖ =
    ‖(f a' z - f a z) + (f a y - f a' y) + (f a z - f a y - (L z - L y))‖ := by congr; abel
  _ ≤ ‖f a' z - f a z‖ + ‖f a y - f a' y‖ + ‖f a z - f a y - (L z - L y)‖ := norm_add₃_le
  _ ≤ ε + ε + b := by
      gcongr
      · rw [← dist_eq_norm]
        change dist (f.uncurry (a', z)) (f.uncurry (a, z)) ≤ ε
        apply (hu _ _ _).le
        · exact ha'x'.1
        · simp [dzx]
      · rw [← dist_eq_norm']
        change dist (f.uncurry (a', y)) (f.uncurry (a, y)) ≤ ε
        apply (hu _ _ _).le
        · exact ha'x'.1
        · simp [dyx]
      · simp [hb, dyx, dzx]
  _ < s * r := by linarith