mathlib3

91b80842 - chore(analysis/normed_space/finite_dimension): extract some lemmas from existentials (#13600)

chore(analysis/normed_space/finite_dimension): extract some lemmas from existentials (#13600) A few proofs in this file prove an existential where a stronger statement in terms of the witness exists. This: * Removes `basis.sup_norm_le_norm` and replaces it with the more general statement `pi.sum_norm_apply_le_norm` * Renames `basis.op_norm_le` to `basis.exists_op_norm_le` * Creates a new `basis.op_norm_le` stated without the existential * Adds the `nnnorm` version of some `norm` lemmas. In some cases it's easier to prove these first, and derive the `norm` versions from them.