no goals
𝕜 : Type ?u.79698
E : Type u_1
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
h : ‖x‖ = ‖y‖
⊢ ‖(1 / 2) • (x + y)‖ < ‖x‖ ↔ x ≠ y
rw [norm_smul, Real.norm_of_nonneg (one_div_nonneg.2 zero_le_two), ← inv_eq_one_div, ←
  div_eq_inv_mul, div_lt_iff (zero_lt_two' ℝ), mul_two, ← not_sameRay_iff_of_norm_eq h,
  not_sameRay_iff_norm_add_lt, h]