awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.TotallyBounded (goal)
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
hts : s ⊆ ⋃ y ∈ t, y +ᵥ V
⊢ ∃ (t : Set E),
    t.Finite ∧ Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t, y +ᵥ U : Set E)
have obtain : ∀ (t' : Set E) (htf' : t'.Finite)
  (hts' : Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E) (⋃ y ∈ t', y +ᵥ V : Set E)),
  ∃ (t : Set E),
    t.Finite ∧ Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t, y +ᵥ U : Set E)
Tactic: obtain ⟨t', ⟨htf', hts'⟩⟩ := (totallyBounded_iff_subset_finite_iUnion_nhds_zero.mp
    (IsCompact.totallyBounded (Finite.isCompact_convexHull ℝ htf)) _ hV₁)
-- Lean 4 proof step from Mathlib.Analysis.Convex.TotallyBounded (goal)
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
hts : s ⊆ ⋃ y ∈ t, y +ᵥ V
t' : Set E
htf' : t'.Finite
hts' : Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E) (⋃ y ∈ t', y +ᵥ V : Set E)
⊢ ∃ (t : Set E),
    t.Finite ∧ Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t, y +ᵥ U : Set E)
have right : Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t', y +ᵥ U : Set E)
Tactic: use t', htf'
-- Lean 4 proof step from Mathlib.Analysis.Convex.TotallyBounded (goal)
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
hts : s ⊆ ⋃ y ∈ t, y +ᵥ V
t' : Set E
htf' : t'.Finite
hts' : Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E) (⋃ y ∈ t', y +ᵥ V : Set E)
⊢ Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t', y +ᵥ U : Set E)
have right : ∀ (hts : s ⊆ t + V) (hts' : (convexHull ℝ : (a : Set E) → Set E) t ⊆ t' + V),
  (convexHull ℝ : (a : Set E) → Set E) s ⊆ t' + U
Tactic: simp only [iUnion_vadd_set, vadd_eq_add] at hts hts' ⊢
Cleared hypotheses: hts, hts'
-- Lean 4 proof step from Mathlib.Analysis.Convex.TotallyBounded (goal)
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
⊢ 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
have rw : HAdd.hAdd (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E) V =
  HAdd.hAdd (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E) V
Tactic: rw [hV₂.convexHull_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.TotallyBounded (goal)
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
⊢ t' + V + V = t' + (V + V)
have rw : t' + (V + V) = t' + (V + V)
Tactic: rw [add_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Convex.TotallyBounded (goal)
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
⊢ (convexHull ℝ : (a : Set E) → Set E) s ⊆ t' + U
have 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
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₂)
-- Lean 4 proof step from Mathlib.Analysis.Convex.TotallyBounded (goal)
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
⊢ (convexHull ℝ : (a : Set E) → Set E) s ⊆ t' + U
have calc₁ : t' + V + V = t' + (V + V)
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₂)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (hypothesis)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
⊢ ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
have hε' : 0 < ε / 3
Tactic: have hε' : 0 < ε / 3 := div_pos hε zero_lt_three
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : UniformConvexSpace E
ε : ℝ
inst_2 : NormedSpace ℝ E
hε : 0 < ε
hε' : 0 < ε / 3
⊢ ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
have 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 - δ
Tactic: obtain ⟨δ, hδ, h⟩ := exists_forall_sphere_dist_add_le_two_sub E hε'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (goal)
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 - δ
have refine : ∀ (x : E) (hx : ‖x‖ ≤ 1) (y : E) (hy : ‖y‖ ≤ 1) (hxy : ε ≤ ‖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 => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (goal)
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‖
⊢ ‖x + y‖ ≤ 2 - δ'
have inl : ∀ (hx' : ‖x‖ ≤ 1 - δ'), ‖x + y‖ ≤ 2 - δ'
Tactic: obtain hx' | hx' := le_or_gt ‖x‖ (1 - δ')
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (goal)
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 - δ'
⊢ ‖x + y‖ ≤ 2 - δ'
have inr : ∀ (hx' : 1 - δ' < ‖x‖), ‖x + y‖ ≤ 2 - δ'
Tactic: obtain hx' | hx' := le_or_gt ‖x‖ (1 - δ')
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (goal)
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‖ ≤ 2 - δ'
have inl : ‖x + y‖ ≤ HAdd.hAdd (α := ℝ) 1 1 - δ'
Tactic: rw [← one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (goal)
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‖
⊢ ‖x + y‖ ≤ 2 - δ'
have inr : ∀ (hy' : ‖y‖ ≤ 1 - δ'), ‖x + y‖ ≤ 2 - δ'
Tactic: obtain hy' | hy' := le_or_gt ‖y‖ (1 - δ')
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (goal)
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 - δ'
⊢ ‖x + y‖ ≤ 2 - δ'
have inr₁ : ∀ (hy' : 1 - δ' < ‖y‖), ‖x + y‖ ≤ 2 - δ'
Tactic: obtain hy' | hy' := le_or_gt ‖y‖ (1 - δ')
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (goal)
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‖ ≤ 2 - δ'
have inr : ‖x + y‖ ≤ HAdd.hAdd (α := ℝ) 1 1 - δ'
Tactic: rw [← one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (hypothesis)
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‖
⊢ ‖x + y‖ ≤ 2 - δ'
have hδ' : 0 < 1 - δ'
Tactic: have hδ' : 0 < 1 - δ' := sub_pos_of_lt (min_lt_of_left_lt one_half_lt_one)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (goal)
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‖
⊢ ‖‖z‖⁻¹ • z‖ = 1
have rw : ‖z‖⁻¹ * ‖z‖ = 1
Tactic: rw [norm_smul_of_nonneg (inv_nonneg.2 <| norm_nonneg _), inv_mul_cancel₀ (hδ'.trans hz).ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (goal)
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
⊢ ‖‖z‖⁻¹ • z‖ = 1
have rw₁ : Eq (α := ℝ) 1 1
Tactic: rw [norm_smul_of_nonneg (inv_nonneg.2 <| norm_nonneg _), inv_mul_cancel₀ (hδ'.trans hz).ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (hypothesis)
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 - δ'
⊢ ‖x + y‖ ≤ 2 - δ'
have h₁ : ∀ (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']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (goal)
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‖
⊢ ‖‖z‖⁻¹ • z - z‖ ≤ δ'
have nth_rw : ‖‖z‖⁻¹ • z - HSMul.hSMul (α := ℝ) 1 z‖ ≤ δ'
Tactic: nth_rw 3 [← one_smul ℝ z]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (goal)
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‖
⊢ ‖‖z‖⁻¹ • z - HSMul.hSMul (α := ℝ) 1 z‖ ≤ δ'
have rwa : ‖(‖z‖⁻¹ - 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (goal)
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‖ ≤ δ'
⊢ ‖‖z‖⁻¹ • z - HSMul.hSMul (α := ℝ) 1 z‖ ≤ δ'
have rwa₁ : (‖z‖⁻¹ - 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (goal)
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‖ ≤ δ'
⊢ ‖‖z‖⁻¹ • z - HSMul.hSMul (α := ℝ) 1 z‖ ≤ δ'
have rwa₂ : ‖z‖⁻¹ * ‖z‖ - 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (goal)
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‖ ≤ δ'
⊢ ‖‖z‖⁻¹ • z - HSMul.hSMul (α := ℝ) 1 z‖ ≤ δ'
have rwa₃ : 1 - 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (goal)
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‖ ≤ δ'
⊢ ‖‖z‖⁻¹ • z - HSMul.hSMul (α := ℝ) 1 z‖ ≤ δ'
have rwa₄ : 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (hypothesis)
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
⊢ ‖x + y‖ ≤ 2 - δ'
have h₂ : ∀ (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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (goal)
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) ≤ ‖x - y‖ - (‖x' - x‖ + ‖y' - y‖)
have hcd : ‖x' - x‖ ≤ ε / 3
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (goal)
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
⊢ ε - (ε / 3 + ε / 3) ≤ ‖x - y‖ - (‖x' - x‖ + ‖y' - y‖)
have hcd₁ : ‖y' - y‖ ≤ ε / 3
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (hypothesis)
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‖ - (‖x' - x‖ + ‖y' - y‖) ≤ ‖x' - y'‖
have this : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.Convex.Uniform (goal)
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'‖
have rw : ‖x' - y' + (x - x') + (y' - y)‖ ≤ ‖x' - y'‖ + ‖x - x'‖ + ‖y' - y‖
Tactic: rw [sub_le_iff_le_add, norm_sub_rev _ x, ← add_assoc, this]