awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2
⊢ StrictConvexSpace ℝ E
have fun : ∀ (x y : E) (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) (hne : x ≠ y), ‖(1 / 2) • x + (1 / 2) • y‖ ≠ 1
Tactic: refine
    StrictConvexSpace.of_norm_combo_ne_one fun x y hx hy hne =>
      ⟨1 / 2, 1 / 2, one_half_pos.le, one_half_pos.le, add_halves _, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hne : x ≠ y
⊢ ‖(1 / 2) • x + (1 / 2) • y‖ ≠ 1
have rw : ¬‖x + y‖ = 2
Tactic: rw [← smul_add, norm_smul, Real.norm_of_nonneg one_half_pos.le, one_div, ← div_eq_inv_mul, Ne,
    div_eq_one_iff_eq (two_ne_zero' ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y
⊢ StrictConvexSpace ℝ E
have refine : ∀ (x : E) (hx : Membership.mem (γ := Set E) (sphere 0 1) x) (y : E) (hy : Membership.mem (γ := Set E) (sphere 0 1) y)
  (h₂ : ‖x + y‖ = 2), x = y
Tactic: refine StrictConvexSpace.of_pairwise_sphere_norm_ne_two fun x hx y hy => mt fun h₂ => ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y
x : E
hx : Membership.mem (γ := Set E) (sphere 0 1) x
y : E
hy : Membership.mem (γ := Set E) (sphere 0 1) y
h₂ : ‖x + y‖ = 2
⊢ x = y
have rw : ∀ (hx : ‖x‖ = 1) (y : E) (hy : ‖y‖ = 1) (h₂ : ‖x + y‖ = 2), x = y
Tactic: rw [mem_sphere_zero_iff_norm] at hx hy
Cleared hypotheses: hx, y, hy, h₂
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
hx : x ∈ closedBall z r
hy : y ∈ closedBall z r
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ ball z r
have inl : ∀ (hx : x ∈ closedBall z 0) (hy : y ∈ closedBall z 0), a • x + b • y ∈ ball z 0
Tactic: rcases eq_or_ne r 0 with (rfl | hr)
Cleared hypotheses: r, hx, hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
hx : x ∈ closedBall z r
hy : y ∈ closedBall z r
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
inl : ∀ (hx : x ∈ closedBall z 0) (hy : y ∈ closedBall z 0), a • x + b • y ∈ ball z 0
⊢ a • x + b • y ∈ ball z r
have inr : ∀ (hr : r ≠ 0), a • x + b • y ∈ ball z r
Tactic: rcases eq_or_ne r 0 with (rfl | hr)
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y z : E
a b : ℝ
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : x ∈ closedBall z 0
hy : y ∈ closedBall z 0
⊢ a • x + b • y ∈ ball z 0
have hx₁ : x = z
Tactic: rw [closedBall_zero, mem_singleton_iff] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y z : E
a b : ℝ
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : x ∈ closedBall z 0
hy : y ∈ closedBall z 0
hx₁ : x = z
⊢ a • x + b • y ∈ ball z 0
have hy₁ : y = z
Tactic: rw [closedBall_zero, mem_singleton_iff] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
hx : x ∈ closedBall z r
hy : y ∈ closedBall z r
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hr : r ≠ 0
⊢ a • x + b • y ∈ ball z r
have inr : a • x + b • y ∈ interior (closedBall z r)
Tactic: simp only [← interior_closedBall _ hr] at hx hy ⊢
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
a b r : ℝ
hx : ‖x‖ ≤ r
hy : ‖y‖ ≤ r
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ‖a • x + b • y‖ < r
have simp : ∀ (hx : Membership.mem (γ := Set E) (closedBall 0 r) x) (hy : Membership.mem (γ := Set E) (closedBall 0 r) y),
  Membership.mem (γ := Set E) (ball 0 r) (a • x + b • y)
Tactic: simp only [← mem_ball_zero_iff, ← mem_closedBall_zero_iff] at hx hy ⊢
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : ¬SameRay ℝ x y
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
have h₁ : x ≠ 0 ∧ y ≠ 0 ∧ ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
Tactic: simp only [sameRay_iff_inv_norm_smul_eq, not_or, ← Ne.eq_def] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : x ≠ 0 ∧ y ≠ 0 ∧ ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
have hx : x ≠ 0
Tactic: rcases h with ⟨hx, hy, hne⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : x ≠ 0 ∧ y ≠ 0 ∧ ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hx : x ≠ 0
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
have hy : y ≠ 0
Tactic: rcases h with ⟨hx, hy, hne⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : x ≠ 0 ∧ y ≠ 0 ∧ ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
have hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
Tactic: rcases h with ⟨hx, hy, hne⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
hx : x ≠ 0
hy : y ≠ 0
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
have hx₁ : 0 < ‖x‖
Tactic: rw [← norm_pos_iff] at hx hy
Cleared hypotheses: hx, hy, hne
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
hx : x ≠ 0
hy : y ≠ 0
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hx₁ : 0 < ‖x‖
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
have hy₁ : 0 < ‖y‖
Tactic: rw [← norm_pos_iff] at hx hy
Cleared hypotheses: hx, hy, hne
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
have hxy : 0 < ‖x‖ + ‖y‖
Tactic: have hxy : 0 < ‖x‖ + ‖y‖ := add_pos hx hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
⊢ ‖x‖ / (‖x‖ + ‖y‖) + ‖y‖ / (‖x‖ + ‖y‖) = 1
have rw : (‖x‖ + ‖y‖) / (‖x‖ + ‖y‖) = 1
Tactic: rw [← add_div, div_self hxy.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
rw : (‖x‖ + ‖y‖) / (‖x‖ + ‖y‖) = 1
⊢ ‖x‖ / (‖x‖ + ‖y‖) + ‖y‖ / (‖x‖ + ‖y‖) = 1
have rw₁ : Eq (α := ℝ) 1 1
Tactic: rw [← add_div, div_self hxy.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
have this : Membership.mem (γ := Set E) (ball 0 1) ((‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y)
Tactic: have :=
    combo_mem_ball_of_ne (inv_norm_smul_mem_unitClosedBall x)
      (inv_norm_smul_mem_unitClosedBall y) hne (div_pos hx hxy) (div_pos hy hxy)
      (by rw [← add_div, div_self hxy.ne'])
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
this : Membership.mem (γ := Set E) (ball 0 1) ((‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y)
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
have rwa : ∀ (this : ‖(‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
Tactic: rwa [mem_ball_zero_iff, div_eq_inv_mul, div_eq_inv_mul, mul_smul, mul_smul, smul_inv_smul₀ hx.ne',
    smul_inv_smul₀ hy.ne', ← smul_add, norm_smul, Real.norm_of_nonneg (inv_pos.2 hxy).le, ←
    div_eq_inv_mul, div_lt_one hxy] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
this : Membership.mem (γ := Set E) (ball 0 1) ((‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y)
rwa : ∀ (this : ‖(‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
have rwa₁ : ∀ (this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
Tactic: rwa [mem_ball_zero_iff, div_eq_inv_mul, div_eq_inv_mul, mul_smul, mul_smul, smul_inv_smul₀ hx.ne',
    smul_inv_smul₀ hy.ne', ← smul_add, norm_smul, Real.norm_of_nonneg (inv_pos.2 hxy).le, ←
    div_eq_inv_mul, div_lt_one hxy] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
this : Membership.mem (γ := Set E) (ball 0 1) ((‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y)
rwa : ∀ (this : ‖(‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₁ : ∀ (this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
have rwa₂ : ∀ (this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + ((‖x‖ + ‖y‖)⁻¹ * ‖y‖) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
Tactic: rwa [mem_ball_zero_iff, div_eq_inv_mul, div_eq_inv_mul, mul_smul, mul_smul, smul_inv_smul₀ hx.ne',
    smul_inv_smul₀ hy.ne', ← smul_add, norm_smul, Real.norm_of_nonneg (inv_pos.2 hxy).le, ←
    div_eq_inv_mul, div_lt_one hxy] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
this : Membership.mem (γ := Set E) (ball 0 1) ((‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y)
rwa : ∀ (this : ‖(‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₁ : ∀ (this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₂ : ∀ (this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + ((‖x‖ + ‖y‖)⁻¹ * ‖y‖) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
have rwa₃ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • ‖x‖ • ‖x‖⁻¹ • x + ((‖x‖ + ‖y‖)⁻¹ * ‖y‖) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
Tactic: rwa [mem_ball_zero_iff, div_eq_inv_mul, div_eq_inv_mul, mul_smul, mul_smul, smul_inv_smul₀ hx.ne',
    smul_inv_smul₀ hy.ne', ← smul_add, norm_smul, Real.norm_of_nonneg (inv_pos.2 hxy).le, ←
    div_eq_inv_mul, div_lt_one hxy] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
this : Membership.mem (γ := Set E) (ball 0 1) ((‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y)
rwa : ∀ (this : ‖(‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₁ : ∀ (this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₂ : ∀ (this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + ((‖x‖ + ‖y‖)⁻¹ * ‖y‖) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₃ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • ‖x‖ • ‖x‖⁻¹ • x + ((‖x‖ + ‖y‖)⁻¹ * ‖y‖) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
have rwa₄ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • ‖x‖ • ‖x‖⁻¹ • x + (‖x‖ + ‖y‖)⁻¹ • ‖y‖ • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
Tactic: rwa [mem_ball_zero_iff, div_eq_inv_mul, div_eq_inv_mul, mul_smul, mul_smul, smul_inv_smul₀ hx.ne',
    smul_inv_smul₀ hy.ne', ← smul_add, norm_smul, Real.norm_of_nonneg (inv_pos.2 hxy).le, ←
    div_eq_inv_mul, div_lt_one hxy] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
this : Membership.mem (γ := Set E) (ball 0 1) ((‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y)
rwa : ∀ (this : ‖(‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₁ : ∀ (this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₂ : ∀ (this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + ((‖x‖ + ‖y‖)⁻¹ * ‖y‖) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₃ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • ‖x‖ • ‖x‖⁻¹ • x + ((‖x‖ + ‖y‖)⁻¹ * ‖y‖) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₄ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • ‖x‖ • ‖x‖⁻¹ • x + (‖x‖ + ‖y‖)⁻¹ • ‖y‖ • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
have rwa₅ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • x + (‖x‖ + ‖y‖)⁻¹ • ‖y‖ • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
Tactic: rwa [mem_ball_zero_iff, div_eq_inv_mul, div_eq_inv_mul, mul_smul, mul_smul, smul_inv_smul₀ hx.ne',
    smul_inv_smul₀ hy.ne', ← smul_add, norm_smul, Real.norm_of_nonneg (inv_pos.2 hxy).le, ←
    div_eq_inv_mul, div_lt_one hxy] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
this : Membership.mem (γ := Set E) (ball 0 1) ((‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y)
rwa : ∀ (this : ‖(‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₁ : ∀ (this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₂ : ∀ (this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + ((‖x‖ + ‖y‖)⁻¹ * ‖y‖) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₃ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • ‖x‖ • ‖x‖⁻¹ • x + ((‖x‖ + ‖y‖)⁻¹ * ‖y‖) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₄ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • ‖x‖ • ‖x‖⁻¹ • x + (‖x‖ + ‖y‖)⁻¹ • ‖y‖ • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₅ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • x + (‖x‖ + ‖y‖)⁻¹ • ‖y‖ • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
have rwa₆ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • x + (‖x‖ + ‖y‖)⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
Tactic: rwa [mem_ball_zero_iff, div_eq_inv_mul, div_eq_inv_mul, mul_smul, mul_smul, smul_inv_smul₀ hx.ne',
    smul_inv_smul₀ hy.ne', ← smul_add, norm_smul, Real.norm_of_nonneg (inv_pos.2 hxy).le, ←
    div_eq_inv_mul, div_lt_one hxy] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
this : Membership.mem (γ := Set E) (ball 0 1) ((‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y)
rwa : ∀ (this : ‖(‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₁ : ∀ (this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₂ : ∀ (this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + ((‖x‖ + ‖y‖)⁻¹ * ‖y‖) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₃ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • ‖x‖ • ‖x‖⁻¹ • x + ((‖x‖ + ‖y‖)⁻¹ * ‖y‖) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₄ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • ‖x‖ • ‖x‖⁻¹ • x + (‖x‖ + ‖y‖)⁻¹ • ‖y‖ • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₅ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • x + (‖x‖ + ‖y‖)⁻¹ • ‖y‖ • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₆ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • x + (‖x‖ + ‖y‖)⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
have rwa₇ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • (x + y)‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
Tactic: rwa [mem_ball_zero_iff, div_eq_inv_mul, div_eq_inv_mul, mul_smul, mul_smul, smul_inv_smul₀ hx.ne',
    smul_inv_smul₀ hy.ne', ← smul_add, norm_smul, Real.norm_of_nonneg (inv_pos.2 hxy).le, ←
    div_eq_inv_mul, div_lt_one hxy] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
this : Membership.mem (γ := Set E) (ball 0 1) ((‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y)
rwa : ∀ (this : ‖(‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₁ : ∀ (this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₂ : ∀ (this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + ((‖x‖ + ‖y‖)⁻¹ * ‖y‖) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₃ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • ‖x‖ • ‖x‖⁻¹ • x + ((‖x‖ + ‖y‖)⁻¹ * ‖y‖) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₄ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • ‖x‖ • ‖x‖⁻¹ • x + (‖x‖ + ‖y‖)⁻¹ • ‖y‖ • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₅ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • x + (‖x‖ + ‖y‖)⁻¹ • ‖y‖ • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₆ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • x + (‖x‖ + ‖y‖)⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₇ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • (x + y)‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
have rwa₈ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹‖ * ‖x + y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
Tactic: rwa [mem_ball_zero_iff, div_eq_inv_mul, div_eq_inv_mul, mul_smul, mul_smul, smul_inv_smul₀ hx.ne',
    smul_inv_smul₀ hy.ne', ← smul_add, norm_smul, Real.norm_of_nonneg (inv_pos.2 hxy).le, ←
    div_eq_inv_mul, div_lt_one hxy] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
this : Membership.mem (γ := Set E) (ball 0 1) ((‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y)
rwa : ∀ (this : ‖(‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₁ : ∀ (this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₂ : ∀ (this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + ((‖x‖ + ‖y‖)⁻¹ * ‖y‖) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₃ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • ‖x‖ • ‖x‖⁻¹ • x + ((‖x‖ + ‖y‖)⁻¹ * ‖y‖) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₄ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • ‖x‖ • ‖x‖⁻¹ • x + (‖x‖ + ‖y‖)⁻¹ • ‖y‖ • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₅ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • x + (‖x‖ + ‖y‖)⁻¹ • ‖y‖ • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₆ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • x + (‖x‖ + ‖y‖)⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₇ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • (x + y)‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₈ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹‖ * ‖x + y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
have rwa₉ : ∀ (this : (‖x‖ + ‖y‖)⁻¹ * ‖x + y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
Tactic: rwa [mem_ball_zero_iff, div_eq_inv_mul, div_eq_inv_mul, mul_smul, mul_smul, smul_inv_smul₀ hx.ne',
    smul_inv_smul₀ hy.ne', ← smul_add, norm_smul, Real.norm_of_nonneg (inv_pos.2 hxy).le, ←
    div_eq_inv_mul, div_lt_one hxy] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
this : Membership.mem (γ := Set E) (ball 0 1) ((‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y)
rwa : ∀ (this : ‖(‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₁ : ∀ (this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₂ : ∀ (this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + ((‖x‖ + ‖y‖)⁻¹ * ‖y‖) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₃ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • ‖x‖ • ‖x‖⁻¹ • x + ((‖x‖ + ‖y‖)⁻¹ * ‖y‖) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₄ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • ‖x‖ • ‖x‖⁻¹ • x + (‖x‖ + ‖y‖)⁻¹ • ‖y‖ • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₅ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • x + (‖x‖ + ‖y‖)⁻¹ • ‖y‖ • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₆ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • x + (‖x‖ + ‖y‖)⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₇ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • (x + y)‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₈ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹‖ * ‖x + y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₉ : ∀ (this : (‖x‖ + ‖y‖)⁻¹ * ‖x + y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
have rwa₁₀ : ∀ (this : ‖x + y‖ / (‖x‖ + ‖y‖) < 1), ‖x + y‖ < ‖x‖ + ‖y‖
Tactic: rwa [mem_ball_zero_iff, div_eq_inv_mul, div_eq_inv_mul, mul_smul, mul_smul, smul_inv_smul₀ hx.ne',
    smul_inv_smul₀ hy.ne', ← smul_add, norm_smul, Real.norm_of_nonneg (inv_pos.2 hxy).le, ←
    div_eq_inv_mul, div_lt_one hxy] at this
Cleared hypotheses: this