[Merged by Bors] - refactor(analysis/normed_space): merge normed_space and semi_normed_space

[eric-wieser]

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

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.

---

• depends on: fix(analysis/normed_space/basic): add some alias instances to fix an inference issue #8221
• depends on: [Merged by Bors] - fix(analysis/calculus/fderiv_symmetric): speed up tactic block from 3.6s to 180ms #11426
• depends on: [Merged by Bors] - feat(analysis/normed_space/linear_isometry): coercion injectivity lemmas and add_monoid_hom_class #11434
• depends on: [Merged by Bors] - chore(analysis/inner_product_space/projection): Speedup linear_isometry_equiv.reflections_generate_dim_aux #11443

[eric-wieser]

For reasons I don't understand, this change breaks:

example (𝕜 ι : Type*) (E : ι → Type*)
  [nondiscrete_normed_field 𝕜] [Π i, normed_group (E i)] [Π i, normed_space 𝕜 (E i)] :
  Π i, module 𝕜 (E i) := by apply_instance

but this works fine

example (𝕜 ι : Type*) (E : ι → Type*)
  [nondiscrete_normed_field 𝕜] [Π i, normed_group (E i)] [Π i, normed_space 𝕜 (E i)] :
  Π i, module 𝕜 (E i) := λ _, by apply_instance

I'm increasingly of the opinion that mixin typeclasses are broken in nasty ways in Lean 3; this is the dfinsupp problem all over again, and has come up multiple times on Zulip.

Edit: I found a workaround which I posted in this Zulip thread, and have committed it. This problem is not a new breakage, it already existed for semi_normed_space.

[riccardobrasca]

LGTM! And it's very nice we can remove some @!

[eric-wieser]

Unfortunately there's a timeout in banach.lean. I'm hoping that I can get away with removing the @s (#8221) before making this refactor, and have an idea to speed up the banach proof using #8220

[leanprover-community-bot-assistant]

This PR/issue depends on:

• fix(analysis/normed_space/basic): add some alias instances to fix an inference issue #8221
• [Merged by Bors] - fix(analysis/calculus/fderiv_symmetric): speed up tactic block from 3.6s to 180ms #11426
• [Merged by Bors] - feat(analysis/normed_space/linear_isometry): coercion injectivity lemmas and add_monoid_hom_class #11434
• [Merged by Bors] - chore(analysis/inner_product_space/projection): Speedup linear_isometry_equiv.reflections_generate_dim_aux #11443
  By Dependent Issues (🤖). Happy coding!

[eric-wieser]

It took 6 months, but all the timeouts are gone!

[eric-wieser]

I introduced function.has_scalar and function.smul_comm_class in another recent PR, and discussed with @madvorak about adding function.has_add etc to fix a similar problem - I'd prefer to leave collecting all those instances together into the right place to a follow-up PR.

[eric-wieser]

I plan to come back to this and check whether those last two commits remove the need for some of the downstream changes

[riccardobrasca]

Looks good to me, and since it compiles it is probably a good idea to merge it soon.

[RemyDegenne]

After all your work to get it to compile, the final diff is rather small in the end :) . It looks good to me!
bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests