no goals
α : Type ?u.9079
β : Type u_1
γ : Type ?u.9085
ι : Type ?u.9088
inst✝² : NormedField α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
x : β
⊢ ‖x‖⁻¹ • x ∈ closedBall 0 1
simp only [mem_closedBall_zero_iff, norm_smul, norm_inv, norm_norm, ← _root_.div_eq_inv_mul,
  div_self_le_one]