awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.TotallyBounded
Goal:
E : Type u_1
s : Set E
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : Membership.mem (γ := Filter E) (nhds 0) U
W : Set E
hW₁ : Membership.mem (γ := Filter E) (nhds 0) W
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : Membership.mem (γ := Filter E) (nhds 0) V
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
t : Set E
htf : t.Finite
t' : Set E
htf' : t'.Finite
hts : s ⊆ t + V
hts' : (convexHull ℝ : (a : Set E) → Set E) t ⊆ t' + V
calc :
  HAdd.hAdd (α := Set E) (β := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E)
      ((convexHull ℝ : (a : Set E) → Set E) V : Set E) =
    HAdd.hAdd (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E) V
calc₁ : t' + V + V = t' + (V + V)
⊢ (convexHull ℝ : (a : Set E) → Set E) s ⊆ t' + U

Tactic:
calc convexHull ℝ s
    _ ⊆ convexHull ℝ (t + V) := convexHull_mono hts
    _ ⊆ convexHull ℝ t + convexHull ℝ V := convexHull_add_subset
    _ = convexHull ℝ t + V := by rw [hV₂.convexHull_eq]
    _ ⊆ t' + V + V := add_subset_add_right hts'
    _ = t' + (V + V) := by rw [add_assoc]
    _ ⊆ t' + (W + W) := add_subset_add_left (add_subset_add hV₃ hV₃)
    _ ⊆ t' + U := add_subset_add_left (add_subset_iff.mpr hW₂)

Premises used: Iff.mpr, Set.add_subset_add_left, Real, Set.add_subset_iff, convexHull_add_subset, convexHull_mono, convexHull, HAdd.hAdd, Set.add_subset_add, Set.add_subset_add_right, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
hε : 0 < ε
⊢ ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ

Tactic:
UniformConvexSpace.uniform_convex hε

Premises used: UniformConvexSpace.uniform_convex
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
⊢ 0 < ε / 3

Tactic:
have hε' : 0 < ε / 3 := div_pos hε zero_lt_three
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
obtain :
  ∀ (δ : ℝ) (hδ : 0 < δ) (h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ),
    ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
⊢ ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ

Tactic:
obtain ⟨δ, hδ, h⟩ := exists_forall_sphere_dist_add_le_two_sub E hε'

Premises used: exists_forall_sphere_dist_add_le_two_sub
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
⊢ ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ

Tactic:
⟨δ', lt_min one_half_pos <| lt_min hε' (div_pos hδ zero_lt_three), fun x hx y hy hxy => ?_⟩

Premises used: zero_lt_three, lt_min, one_half_pos, And.intro, Exists.intro, div_pos
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
refine : ∀ (x : E) (hx : ‖x‖ ≤ 1) (y : E) (hy : ‖y‖ ≤ 1) (hxy : ε ≤ ‖x - y‖), ‖x + y‖ ≤ 2 - δ'
⊢ ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ

Tactic:
refine ⟨δ', lt_min one_half_pos <| lt_min hε' (div_pos hδ zero_lt_three), fun x hx y hy hxy => ?_⟩
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
inl : ∀ (hx' : ‖x‖ ≤ 1 - δ'), ‖x + y‖ ≤ 2 - δ'
inr : ∀ (hx' : 1 - δ' < ‖x‖), ‖x + y‖ ≤ 2 - δ'
⊢ ‖x + y‖ ≤ 2 - δ'

Tactic:
obtain hx' | hx' := le_or_gt ‖x‖ (1 - δ')

Premises used: Norm.norm, HSub.hSub, le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : ‖x‖ ≤ 1 - δ'
inl : ‖x + y‖ ≤ HAdd.hAdd (α := ℝ) 1 1 - δ'
⊢ ‖x + y‖ ≤ 2 - δ'

Tactic:
rw [← one_add_one_eq_two]

Premises used: one_add_one_eq_two
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : ‖x‖ ≤ 1 - δ'
⊢ ‖x + y‖ ≤ HAdd.hAdd (α := ℝ) 1 1 - δ'

Tactic:
(norm_add_le_of_le hx' hy).trans (sub_add_eq_add_sub _ _ _).le

Premises used: Eq.le, norm_add_le_of_le, LE.le.trans, sub_add_eq_add_sub
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : ‖x‖ ≤ 1 - δ'
⊢ ‖x + y‖ ≤ HAdd.hAdd (α := ℝ) 1 1 - δ'

Tactic:
exact (norm_add_le_of_le hx' hy).trans (sub_add_eq_add_sub _ _ _).le

Premises used: Eq.le, norm_add_le_of_le, LE.le.trans, sub_add_eq_add_sub
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
inr : ∀ (hy' : ‖y‖ ≤ 1 - δ'), ‖x + y‖ ≤ 2 - δ'
inr₁ : ∀ (hy' : 1 - δ' < ‖y‖), ‖x + y‖ ≤ 2 - δ'
⊢ ‖x + y‖ ≤ 2 - δ'

Tactic:
obtain hy' | hy' := le_or_gt ‖y‖ (1 - δ')

Premises used: Norm.norm, HSub.hSub, le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : ‖y‖ ≤ 1 - δ'
inr : ‖x + y‖ ≤ HAdd.hAdd (α := ℝ) 1 1 - δ'
⊢ ‖x + y‖ ≤ 2 - δ'

Tactic:
rw [← one_add_one_eq_two]

Premises used: one_add_one_eq_two
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : ‖y‖ ≤ 1 - δ'
⊢ ‖x + y‖ ≤ HAdd.hAdd (α := ℝ) 1 1 - δ'

Tactic:
(norm_add_le_of_le hx hy').trans (add_sub_assoc _ _ _).ge

Premises used: add_sub_assoc, Eq.ge, norm_add_le_of_le, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : ‖y‖ ≤ 1 - δ'
⊢ ‖x + y‖ ≤ HAdd.hAdd (α := ℝ) 1 1 - δ'

Tactic:
exact (norm_add_le_of_le hx hy').trans (add_sub_assoc _ _ _).ge

Premises used: add_sub_assoc, Eq.ge, norm_add_le_of_le, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
⊢ 0 < 1 - δ'

Tactic:
have hδ' : 0 < 1 - δ' := sub_pos_of_lt (min_lt_of_left_lt one_half_lt_one)
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
z : E
hz : 1 - δ' < ‖z‖
rw : ‖z‖⁻¹ * ‖z‖ = 1
rw₁ rw₂ : Eq (α := ℝ) 1 1
⊢ ‖‖z‖⁻¹ • z‖ = 1

Tactic:
rw [norm_smul_of_nonneg (inv_nonneg.2 <| norm_nonneg _), inv_mul_cancel₀ (hδ'.trans hz).ne']

Premises used: Iff.mpr, norm_smul_of_nonneg, LT.lt.ne', inv_nonneg, LT.lt.trans, inv_mul_cancel₀, norm_nonneg
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
⊢ ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1

Tactic:
have h₁ : ∀ z : E, 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1 := by
    rintro z hz
    rw [norm_smul_of_nonneg (inv_nonneg.2 <| norm_nonneg _), inv_mul_cancel₀ (hδ'.trans hz).ne']
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
z : E
hz : ‖z‖ ≤ 1
hδz : 1 - δ' ≤ ‖z‖
nth_rw : ‖‖z‖⁻¹ • z - HSMul.hSMul (α := ℝ) 1 z‖ ≤ δ'
⊢ ‖‖z‖⁻¹ • z - z‖ ≤ δ'

Tactic:
nth_rw 3 [← one_smul ℝ z]

Premises used: Real, one_smul
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
z : E
hz : ‖z‖ ≤ 1
hδz : 1 - δ' ≤ ‖z‖
rwa : ‖(‖z‖⁻¹ - 1) • z‖ ≤ δ'
rwa₁ : (‖z‖⁻¹ - 1) * ‖z‖ ≤ δ'
rwa₂ : ‖z‖⁻¹ * ‖z‖ - 1 * ‖z‖ ≤ δ'
rwa₃ : 1 - 1 * ‖z‖ ≤ δ'
rwa₄ : 1 - ‖z‖ ≤ δ'
rwa₅ rwa₆ rwa₇ rwa₈ : 1 - δ' ≤ ‖z‖
⊢ ‖‖z‖⁻¹ • z - HSMul.hSMul (α := ℝ) 1 z‖ ≤ δ'

Tactic:
rwa [← sub_smul,
      norm_smul_of_nonneg (sub_nonneg_of_le <| (one_le_inv₀ (hδ'.trans_le hδz)).2 hz),
      sub_mul, inv_mul_cancel₀ (hδ'.trans_le hδz).ne', one_mul, sub_le_comm]

Premises used: Iff.mpr, one_le_inv₀, sub_nonneg_of_le, norm_smul_of_nonneg, sub_smul, LT.lt.ne', sub_mul, sub_le_comm, LT.lt.trans_le, inv_mul_cancel₀, one_mul
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
⊢ ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'

Tactic:
have h₂ : ∀ z : E, ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ' := by
    rintro z hz hδz
    nth_rw 3 [← one_smul ℝ z]
    rwa [← sub_smul,
      norm_smul_of_nonneg (sub_nonneg_of_le <| (one_le_inv₀ (hδ'.trans_le hδz)).2 hz),
      sub_mul, inv_mul_cancel₀ (hδ'.trans_le hδz).ne', one_mul, sub_le_comm]
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
⊢ ε / 3 = ε - (ε / 3 + ε / 3)

Tactic:
ring
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hcd : ‖x' - x‖ ≤ ε / 3
hcd₁ : ‖y' - y‖ ≤ ε / 3
⊢ ε - (ε / 3 + ε / 3) ≤ ‖x - y‖ - (‖x' - x‖ + ‖y' - y‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
⊢ ‖x' - x‖ ≤ ε / 3

Tactic:
(h₂ _ hx hx'.le).trans <| min_le_of_right_le <| min_le_left _ _

Premises used: LT.lt.le, min_le_left, min_le_of_right_le, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
⊢ ‖x' - x‖ ≤ ε / 3

Tactic:
exact (h₂ _ hx hx'.le).trans <| min_le_of_right_le <| min_le_left _ _

Premises used: LT.lt.le, min_le_left, min_le_of_right_le, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
⊢ ‖y' - y‖ ≤ ε / 3

Tactic:
(h₂ _ hy hy'.le).trans <| min_le_of_right_le <| min_le_left _ _

Premises used: LT.lt.le, min_le_left, min_le_of_right_le, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
⊢ ‖y' - y‖ ≤ ε / 3

Tactic:
exact (h₂ _ hy hy'.le).trans <| min_le_of_right_le <| min_le_left _ _

Premises used: LT.lt.le, min_le_left, min_le_of_right_le, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
x_1 x_2 : E
⊢ x - y = x_1 - x_2 + (x - x_1) + (x_2 - y)

Tactic:
abel
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
⊢ ∀ (x' y' : E), x - y = x' - y' + (x - x') + (y' - y)

Tactic:
have : ∀ x' y', x - y = x' - y' + (x - x') + (y' - y) := fun _ _ => by abel
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
this : ∀ (x' y' : E), x - y = x' - y' + (x - x') + (y' - y)
rw : ‖x' - y' + (x - x') + (y' - y)‖ ≤ ‖x' - y'‖ + ‖x - x'‖ + ‖y' - y‖
x'₁ y'₁ : E
⊢ ‖x - y‖ - (‖x' - x‖ + ‖y' - y‖) ≤ ‖x' - y'‖

Tactic:
rw [sub_le_iff_le_add, norm_sub_rev _ x, ← add_assoc, this]

Premises used: add_assoc, sub_le_iff_le_add, norm_sub_rev
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
this : ∀ (x' y' : E), x - y = x' - y' + (x - x') + (y' - y)
⊢ ‖x' - y' + (x - x') + (y' - y)‖ ≤ ‖x' - y'‖ + ‖x - x'‖ + ‖y' - y‖

Tactic:
norm_add₃_le

Premises used: norm_add₃_le
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
⊢ ε / 3 ≤ ‖x' - y'‖

Tactic:
have hxy' : ε / 3 ≤ ‖x' - y'‖ :=
    calc
      ε / 3 = ε - (ε / 3 + ε / 3) := by ring
      _ ≤ ‖x - y‖ - (‖x' - x‖ + ‖y' - y‖) := by
        gcongr
        · exact (h₂ _ hx hx'.le).trans <| min_le_of_right_le <| min_le_left _ _
        · exact (h₂ _ hy hy'.le).trans <| min_le_of_right_le <| min_le_left _ _
      _ ≤ _ := by
        have : ∀ x' y', x - y = x' - y' + (x - x') + (y' - y) := fun _ _ => by abel
        rw [sub_le_iff_le_add, norm_sub_rev _ x, ← add_assoc, this]
        exact norm_add₃_le
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
x_1 x_2 : E
⊢ x + y = x_1 + x_2 + (x - x_1) + (y - x_2)

Tactic:
abel
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ ∀ (x' y' : E), x + y = x' + y' + (x - x') + (y - y')

Tactic:
have : ∀ x' y', x + y = x' + y' + (x - x') + (y - y') := fun _ _ => by abel
-- Module: Mathlib.Analysis.Convex.Uniform
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))
x : E
hx : ‖x‖ ≤ 1
y : E
hy : ‖y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
hx' : 1 - δ' < ‖x‖
hy' : 1 - δ' < ‖y‖
hδ' : 0 < 1 - δ'
h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1
h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'
x' : E := ‖x‖⁻¹ • x
y' : E := ‖y‖⁻¹ • y
hxy' : ε / 3 ≤ ‖x' - y'‖
this : ∀ (x' y' : E), x + y = x' + y' + (x - x') + (y - y')
rw : ‖x' + y' + (x - x') + (y - y')‖ ≤ ‖x' + y'‖ + ‖x - x'‖ + ‖y - y'‖
x'₁ y'₁ : E
⊢ ‖x + y‖ ≤ ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖

Tactic:
rw [norm_sub_rev, norm_sub_rev y', this]

Premises used: norm_sub_rev