awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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 : 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)) < ε
⊢ u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)

Tactic:
have : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x) :=
    prod_mem_nhds (u_open.mem_nhds au) (ball_mem_nhds _ (sub_pos.2 ht't))
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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)
h :
  ∀ a ∈ u ×ˢ ball x (t - t'),
    ∃ (r' : ℝ),
      (r / 2 < r' ∧ r' ≤ r) ∧
        ∀ (y : E),
          dist y a.2 < r' →
            ∀ (z : E),
              dist z a.2 < r' →
                ‖f a.1 z - f a.1 y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
                  s * r
⊢ {p : α × E |
      ∃ (r' : ℝ),
        (r / 2 < r' ∧ r' ≤ r) ∧
          ∀ (y : E),
            dist y p.2 < r' →
              ∀ (z : E),
                dist z p.2 < r' →
                  ‖f p.1 z - f p.1 y -
                        HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
                    s * r} ∈
    𝓝 (a, x)

Tactic:
filter_upwards [this]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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', x') ∈ u ×ˢ ball x (t - t')
⊢ a' ∈ u ∧ dist x' x < t - t'

Tactic:
simp only [mem_prod, mem_ball] at ha'x'

Premises used: Metric.mem_ball, Set.mem_prod
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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'
⊢ ∃ (r' : ℝ),
    (r / 2 < r' ∧ r' ≤ r) ∧
      ∀ (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

Tactic:
⟨t', ⟨hrt', ht't.le.trans (htr'.le.trans Ir'r)⟩, fun y hy z hz ↦ ?_⟩

Premises used: LT.lt.le, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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'
h :
  ∀ (y : E) (hy : dist y (a', x').2 < t') (z : E) (hz : dist z (a', x').2 < 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
⊢ ∃ (r' : ℝ),
    (r / 2 < r' ∧ r' ≤ r) ∧
      ∀ (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

Tactic:
refine ⟨t', ⟨hrt', ht't.le.trans (htr'.le.trans Ir'r)⟩, fun y hy z hz ↦ ?_⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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'
linarith : t < dist y x → 2 / 2 = 1
linarith₁ : t < dist y x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : t < dist y x → GT.gt (α := ℝ) 2 0
linarith₃ : t < dist y x → 2 / 2 = 1
linarith₄ : t < dist y x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : t < dist y x → GT.gt (α := ℝ) 2 0
linarith₆ : t < dist y x → 2 / 2 = 1
linarith₇ : t < dist y x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : t < dist y x → GT.gt (α := ℝ) 2 0
linarith₉ :
  t < dist y x →
    dist x' x - (t - t') + (dist y (a', x').2 - t') + (t - dist y x) + (dist y x - (dist y x' + dist x' x)) = 0
⊢ dist y x ≤ t

Tactic:
linarith [dist_triangle y x' x]

Premises used: dist_triangle
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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'
⊢ dist y x ≤ t

Tactic:
have dyx : dist y x ≤ t := by linarith [dist_triangle y x' x]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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
linarith : t < dist z x → 2 / 2 = 1
linarith₁ : t < dist z x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : t < dist z x → GT.gt (α := ℝ) 2 0
linarith₃ : t < dist z x → 2 / 2 = 1
linarith₄ : t < dist z x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : t < dist z x → GT.gt (α := ℝ) 2 0
linarith₆ : t < dist z x → 2 / 2 = 1
linarith₇ : t < dist z x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : t < dist z x → GT.gt (α := ℝ) 2 0
linarith₉ :
  t < dist z x →
    dist x' x - (t - t') + (dist z (a', x').2 - t') + (t - dist z x) + (dist z x - (dist z x' + dist x' x)) = 0
⊢ dist z x ≤ t

Tactic:
linarith [dist_triangle z x' x]

Premises used: dist_triangle
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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
⊢ dist z x ≤ t

Tactic:
have dzx : dist z x ≤ t := by linarith [dist_triangle z x' x]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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
e_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' 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:
congr
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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' 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:
abel
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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' 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' 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:
norm_add₃_le

Premises used: norm_add₃_le
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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
h₁ : ‖f a' z - f a z‖ ≤ ε
h₂ : ‖f a y - f a' y‖ ≤ ε
h₃ : ‖f a z - f a y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ ≤ b
⊢ ‖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:
gcongr