chore(analysis/normed_space/star/basic): golf a proof (#12420)
chore(analysis/normed_space/star/basic): golf a proof (#12420)

Shorten a proof using ext.





leanprover-community/mathlib,leanprover-community/mathlib