awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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‖ ≤ 2 - δ'
have hxy' : ε / 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
-- 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
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ ‖x + y‖ ≤ ‖x' + y'‖ + ‖x' - x‖ + ‖y' - 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
hxy' : ε / 3 ≤ ‖x' - y'‖
this : ∀ (x' y' : E), x + y = x' + y' + (x - x') + (y - y')
⊢ ‖x + y‖ ≤ ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖
have rw : ‖x' + y' + (x - x') + (y - y')‖ ≤ ‖x' + y'‖ + ‖x - x'‖ + ‖y - y'‖
Tactic: rw [norm_sub_rev, norm_sub_rev y', this]
-- 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
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖ ≤ 2 - δ + δ' + δ'
have h₃ : ‖x' + y'‖ ≤ 2 - δ
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
hxy' : ε / 3 ≤ ‖x' - y'‖
h₃ : ‖x' + y'‖ ≤ 2 - δ
⊢ ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖ ≤ 2 - δ + δ' + δ'
have h₄ : ‖x' - x‖ ≤ δ'
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
hxy' : ε / 3 ≤ ‖x' - y'‖
h₃ : ‖x' + y'‖ ≤ 2 - δ
h₄ : ‖x' - x‖ ≤ δ'
⊢ ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖ ≤ 2 - δ + δ' + δ'
have h₅ : ‖y' - y‖ ≤ δ'
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
hxy' : ε / 3 ≤ ‖x' - y'‖
this : δ' ≤ δ / 3
⊢ 2 - δ + δ' + δ' ≤ 2 - δ'
have linarith : 2 - δ' < 2 - δ + δ' + δ' → 3 / 3 = 1
Tactic: linarith
-- 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
hxy' : ε / 3 ≤ ‖x' - y'‖
this : δ' ≤ δ / 3
linarith : 2 - δ' < 2 - δ + δ' + δ' → 3 / 3 = 1
⊢ 2 - δ + δ' + δ' ≤ 2 - δ'
have linarith₁ : 2 - δ' < 2 - δ + δ' + δ' → HMul.hMul (α := ℝ) 1 3 = 3
Tactic: linarith
-- 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
hxy' : ε / 3 ≤ ‖x' - y'‖
this : δ' ≤ δ / 3
linarith : 2 - δ' < 2 - δ + δ' + δ' → 3 / 3 = 1
linarith₁ : 2 - δ' < 2 - δ + δ' + δ' → HMul.hMul (α := ℝ) 1 3 = 3
⊢ 2 - δ + δ' + δ' ≤ 2 - δ'
have linarith₂ : 2 - δ' < 2 - δ + δ' + δ' → GT.gt (α := ℝ) 3 0
Tactic: linarith
-- 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
hxy' : ε / 3 ≤ ‖x' - y'‖
this : δ' ≤ δ / 3
linarith : 2 - δ' < 2 - δ + δ' + δ' → 3 / 3 = 1
linarith₁ : 2 - δ' < 2 - δ + δ' + δ' → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : 2 - δ' < 2 - δ + δ' + δ' → GT.gt (α := ℝ) 3 0
linarith₃ : 2 - δ' < 2 - δ + δ' + δ' → 3 / 3 = 1
linarith₄ : 2 - δ' < 2 - δ + δ' + δ' → HMul.hMul (α := ℝ) 1 3 = 3
linarith₅ : 2 - δ' < 2 - δ + δ' + δ' → GT.gt (α := ℝ) 3 0
linarith₆ : 2 - δ' < 2 - δ + δ' + δ' → 3 / 3 = 1
linarith₇ : 2 - δ' < 2 - δ + δ' + δ' → HMul.hMul (α := ℝ) 1 3 = 3
linarith₈ : 2 - δ' < 2 - δ + δ' + δ' → GT.gt (α := ℝ) 3 0
⊢ 2 - δ + δ' + δ' ≤ 2 - δ'
have linarith₉ : 2 - δ' < 2 - δ + δ' + δ' → 3 * δ' - 1 * δ + (2 - δ' - (2 - δ + δ' + δ')) = 0
Tactic: linarith
-- 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
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ 2 - δ + δ' + δ' ≤ 2 - δ'
have suffices : δ' ≤ δ / 3
Tactic: suffices δ' ≤ δ / 3 by linarith
-- 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
hxy' : ε / 3 ≤ ‖x' - y'‖
⊢ ‖x + y‖ ≤ 2 - δ'
have have : ‖x + y‖ ≤ ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖
Tactic: calc
    ‖x + y‖ ≤ ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖ := by
      have : ∀ x' y', x + y = x' + y' + (x - x') + (y - y') := fun _ _ => by abel
      rw [norm_sub_rev, norm_sub_rev y', this]
      exact norm_add₃_le
    _ ≤ 2 - δ + δ' + δ' := by
      gcongr
      exacts [h (h₁ _ hx') (h₁ _ hy') hxy', h₂ _ hx hx'.le, h₂ _ hy hy'.le]
    _ ≤ 2 - δ' := by
      suffices δ' ≤ δ / 3 by linarith
      exact min_le_of_right_le <| min_le_right _ _
-- 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
hxy' : ε / 3 ≤ ‖x' - y'‖
have : ‖x + y‖ ≤ ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖
⊢ ‖x + y‖ ≤ 2 - δ'
have have₁ : ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖ ≤ 2 - δ + δ' + δ'
Tactic: calc
    ‖x + y‖ ≤ ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖ := by
      have : ∀ x' y', x + y = x' + y' + (x - x') + (y - y') := fun _ _ => by abel
      rw [norm_sub_rev, norm_sub_rev y', this]
      exact norm_add₃_le
    _ ≤ 2 - δ + δ' + δ' := by
      gcongr
      exacts [h (h₁ _ hx') (h₁ _ hy') hxy', h₂ _ hx hx'.le, h₂ _ hy hy'.le]
    _ ≤ 2 - δ' := by
      suffices δ' ≤ δ / 3 by linarith
      exact min_le_of_right_le <| min_le_right _ _
-- 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
hxy' : ε / 3 ≤ ‖x' - y'‖
have : ‖x + y‖ ≤ ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖
have₁ : ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖ ≤ 2 - δ + δ' + δ'
⊢ ‖x + y‖ ≤ 2 - δ'
have have₂ : 2 - δ + δ' + δ' ≤ 2 - δ'
Tactic: calc
    ‖x + y‖ ≤ ‖x' + y'‖ + ‖x' - x‖ + ‖y' - y‖ := by
      have : ∀ x' y', x + y = x' + y' + (x - x') + (y - y') := fun _ _ => by abel
      rw [norm_sub_rev, norm_sub_rev y', this]
      exact norm_add₃_le
    _ ≤ 2 - δ + δ' + δ' := by
      gcongr
      exacts [h (h₁ _ hx') (h₁ _ hy') hxy', h₂ _ hx hx'.le, h₂ _ hy hy'.le]
    _ ≤ 2 - δ' := by
      suffices δ' ≤ δ / 3 by linarith
      exact min_le_of_right_le <| min_le_right _ _
-- 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 < ε
r : ℝ
⊢ ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ
have inl : ∀ (hr : r ≤ 0), ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ
Tactic: obtain hr | hr := le_or_gt r 0
-- 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 < ε
r : ℝ
inl : ∀ (hr : r ≤ 0), ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ
⊢ ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ
have inr : ∀ (hr : 0 < r), ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ
Tactic: obtain hr | hr := le_or_gt r 0
-- 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 < ε
r : ℝ
hr : 0 < r
⊢ ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ
have inr : ∀ (δ : ℝ) (hδ : 0 < δ) (h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ),
  ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ
Tactic: obtain ⟨δ, hδ, h⟩ := exists_forall_closed_ball_dist_add_le_two_sub E (div_pos hε hr)
-- 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 < ε
r : ℝ
hr : 0 < r
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
⊢ ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ
have inr : ∀ (x : E) (hx : ‖x‖ ≤ r) (y : E) (hy : ‖y‖ ≤ r) (hxy : ε ≤ ‖x - y‖), ‖x + y‖ ≤ 2 * r - δ * r
Tactic: refine ⟨δ * r, mul_pos hδ hr, 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 < ε
r : ℝ
hr : 0 < r
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
x : E
hx : ‖x‖ ≤ r
y : E
hy : ‖y‖ ≤ r
hxy : ε ≤ ‖x - y‖
⊢ ‖x + y‖ ≤ 2 * r - δ * r
have inr : ∀ (hx : ‖r⁻¹ • x‖ ≤ 1) (y : E) (hy : ‖r⁻¹ • y‖ ≤ 1) (hxy : ε ≤ ‖x - y‖), ‖x + y‖ ≤ 2 * r - δ * r
Tactic: rw [← div_le_one hr, div_eq_inv_mul, ← norm_smul_of_nonneg (inv_nonneg.2 hr.le)] at hx hy
Cleared hypotheses: hx, y, hy, hxy
-- 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 < ε
r : ℝ
hr : 0 < r
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
x : E
hx : ‖r⁻¹ • x‖ ≤ 1
y : E
hy : ‖r⁻¹ • y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
⊢ ‖x + y‖ ≤ 2 * r - δ * r
have this : ε / r ≤ ‖r⁻¹ • x - r⁻¹ • y‖ → ‖r⁻¹ • x + r⁻¹ • y‖ ≤ 2 - δ
Tactic: have := h hx hy
-- 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 < ε
r : ℝ
hr : 0 < r
δ : ℝ
hδ : 0 < δ
h : ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε / r ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
x : E
hx : ‖r⁻¹ • x‖ ≤ 1
y : E
hy : ‖r⁻¹ • y‖ ≤ 1
hxy : ε ≤ ‖x - y‖
this : ε / r ≤ ‖r⁻¹ • x - r⁻¹ • y‖ → ‖r⁻¹ • x + r⁻¹ • y‖ ≤ 2 - δ
⊢ ‖x + y‖ ≤ 2 * r - δ * r
have this₁ : ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ * r
Tactic: simp_rw [← smul_add, ← smul_sub, norm_smul_of_nonneg (inv_nonneg.2 hr.le), ← div_eq_inv_mul,
    div_le_div_iff_of_pos_right hr, div_le_iff₀ hr, sub_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
inst_5 : AddTorsor V P
s : Set P
x y : P
hxy : x ≠ y
⊢ IsVisible 𝕜 s x y ↔ ∀ (δ : 𝕜), Membership.mem (γ := Set 𝕜) (Set.Ioo 0 1) δ → ((lineMap x y : (a : 𝕜) → P) δ : P) ∉ s
have simp : (∀ ⦃z : P⦄, z ∈ s → ∀ (x_1 : 𝕜), 0 < x_1 → x_1 < 1 → ¬(lineMap x y : (a : 𝕜) → P) x_1 = z) ↔
  ∀ (δ : 𝕜), 0 < δ → δ < 1 → ((lineMap x y : (a : 𝕜) → P) δ : P) ∉ s
Tactic: simp [IsVisible, sbtw_iff_mem_image_Ioo_and_ne, hxy]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
hw : IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi : 0 < w i
⊢ IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (a i)
have inl : ∀ (hwi : w i = 1), IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (a i)
Tactic: obtain hwi | hwi : w i = 1 ∨ w i < 1 := eq_or_lt_of_le <| (single_le_sum hw₀ hi).trans_eq hw₁
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
hw : IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi : 0 < w i
inl : ∀ (hwi : w i = 1), IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (a i)
⊢ IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (a i)
have inr : ∀ (hwi : w i < 1), IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (a i)
Tactic: obtain hwi | hwi : w i = 1 ∨ w i < 1 := eq_or_lt_of_le <| (single_le_sum hw₀ hi).trans_eq hw₁
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
hw : IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi_1 : 0 < w i
hwi : w i = 1
⊢ IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (a i)
have h : a i = ∑ i ∈ t, w i • a i
Tactic: convert! hw
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
hw : IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi_1 : 0 < w i
hwi : w i = 1
⊢ a i = ∑ i ∈ t, w i • a i
have h : ∑ i ∈ t, w i • a i = w i • a i
Tactic: rw [← one_smul 𝕜 (a i), ← hwi, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (hypothesis)
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
hw : IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi_1 : 0 < w i
hwi : w i = 1
⊢ ∑ i ∈ t, w i • a i = w i • a i
have hw₂ : ∀ i_1 ∈ t.erase i, w i_1 = 0
Tactic: rw [← hwi, ← sub_eq_zero, ← sum_erase_eq_sub hi,
      sum_eq_zero_iff_of_nonneg fun j hj ↦ hw₀ _ <| erase_subset _ _ hj] at hw₁
Cleared hypotheses: hw₁, hi, hwi_1, hwi
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
hw : IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (∑ i ∈ t, w i • a i)
i : ι
hw₁ : ∀ i_1 ∈ t.erase i, w i_1 = 0
hi : i ∈ t
hwi_1 : 0 < w i
hwi : w i = 1
⊢ ∑ i ∈ t, w i • a i = w i • a i
have h : ∀ (j : ι) (hj : j ∈ t) (hji : j ≠ i), w j • a j = 0
Tactic: refine sum_eq_single _ (fun j hj hji ↦ ?_) (by simp [hi])
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
hw : IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (∑ i ∈ t, w i • a i)
i : ι
hw₁ : ∀ i_1 ∈ t.erase i, w i_1 = 0
hi : i ∈ t
hwi_1 : 0 < w i
hwi : w i = 1
j : ι
hj : j ∈ t
hji : j ≠ i
⊢ w j • a j = 0
have h : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 (a j) = 0
Tactic: rw [hw₁ _ <| mem_erase.2 ⟨hji, hj⟩, zero_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
hw : IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (∑ i ∈ t, w i • a i)
i : ι
hw₁ : ∀ i_1 ∈ t.erase i, w i_1 = 0
hi : i ∈ t
hwi_1 : 0 < w i
hwi : w i = 1
j : ι
hj : j ∈ t
hji : j ≠ i
h : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 (a j) = 0
⊢ w j • a j = 0
have h₁ : Eq.{u_2 + 1} (α := V) 0 0
Tactic: rw [hw₁ _ <| mem_erase.2 ⟨hji, hj⟩, zero_smul]