no goals
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
⊢ ‖↑‖x‖ • coord 𝕜 x h‖ = 1
rw [norm_smul (x := coord 𝕜 x h), IsROrC.norm_coe_norm, coord_norm,
  mul_inv_cancel (mt norm_eq_zero.mp h)]