mathlib

02a4775a - refactor(analysis/normed_space): merge `normed_space` and `semi_normed_space` (#8218)

refactor(analysis/normed_space): merge `normed_space` and `semi_normed_space` (#8218) There are no theorems which are true for `[normed_group M] [normed_space R M]` but not `[normed_group M] [semi_normed_space R M]`; so there is about as much value to the `semi_normed_space` / `normed_space` distinction as there was between `module` / `semimodule`. Since we eliminated `semimodule`, we should eliminte `semi_normed_space` too. This relaxes the typeclass arguments of `normed_space` to make it a drop-in replacement for `semi_normed_space`; or viewed another way, this removes `normed_space` and renames `semi_normed_space` to replace it. This does the same thing to `normed_algebra` and `seminormed_algebra`, but these are hardly used anyway. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/semi_normed_space.20vs.20normed_space/near/245089933) As with any typeclass refactor, this randomly breaks elaboration in a few places; presumably, it was able to unify arguments from one particular typeclass path, but not from another. To fix this, some type ascriptions have to be added where previously none were needed. In a few rare cases, the elaborator gets so confused that we have to enter tactic mode to produce a term. This isn't really a new problem - this PR just makes these issues all visible at once, whereas normally we'd only run into one or two at a time. Optimistically Lean 4 will fix all this, but we won't really know until we try.