chore(analysis/normed_space): golf some proofs (#5804)
* add `pi_norm_lt_iff`;
* add `has_sum.norm_le_of_bounded`;
* add `multilinear_map.bound_of_shell`;
* rename `continuous_multilinear_map.norm_image_sub_le_of_bound` to
`continuous_multilinear_map.norm_image_sub_le`, same with prime
version;
* golf some proofs.
