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.

Author: eric-wieser

docs/overview.yaml

@@ -243,7 +243,7 @@ Topology:
 Analysis:
   Normed vector spaces/Banach spaces:
     normed vector space over a normed field: 'normed_space'
-    topology on a normed vector space: 'semi_normed_space.has_bounded_smul'
+    topology on a normed vector space: 'normed_space.has_bounded_smul'
     equivalence of norms in finite dimension: 'linear_equiv.to_continuous_linear_equiv'
     finite dimensional normed spaces over complete normed fields are complete: 'submodule.complete_of_finite_dimensional'
     Heine-Borel theorem (finite dimensional normed spaces are proper): 'finite_dimensional.proper'

docs/undergrad.yaml

@@ -411,7 +411,7 @@ Topology:
     complete metric spaces: 'metric.complete_of_cauchy_seq_tendsto'
     contraction mapping theorem: 'contracting_with.exists_fixed_point'
   Normed vector spaces on $\R$ and $\C$:
-    topology on a normed vector space: 'semi_normed_space.has_bounded_smul'
+    topology on a normed vector space: 'normed_space.has_bounded_smul'
     equivalent norms: ''
     Banach open mapping theorem: 'continuous_linear_map.is_open_map'
     equivalence of norms in finite dimension: 'linear_equiv.to_continuous_linear_equiv'

src/analysis/calculus/deriv.lean

@@ -988,7 +988,8 @@ lemma deriv_within_const_sub (hxs : unique_diff_within_at 𝕜 s x) (c : F) :
 by simp [deriv_within, fderiv_within_const_sub hxs]
 
 lemma deriv_const_sub (c : F) : deriv (λ y, c - f y) x = -deriv f x :=
-by simp only [← deriv_within_univ, deriv_within_const_sub unique_diff_within_at_univ]
+by simp only [← deriv_within_univ,
+  deriv_within_const_sub (unique_diff_within_at_univ : unique_diff_within_at 𝕜 _ _)]
 
 end sub
 

src/analysis/calculus/mean_value.lean

@@ -1301,6 +1301,6 @@ lemma has_strict_deriv_at_of_has_deriv_at_of_continuous_at {f f' : 𝕜 → G} {
   (hder : ∀ᶠ y in 𝓝 x, has_deriv_at f (f' y) y) (hcont : continuous_at f' x) :
   has_strict_deriv_at f (f' x) x :=
 has_strict_fderiv_at_of_has_fderiv_at_of_continuous_at (hder.mono (λ y hy, hy.has_fderiv_at)) $
-  (smul_rightL 𝕜 _ _ 1).continuous.continuous_at.comp hcont
+  (smul_rightL 𝕜 𝕜 G 1).continuous.continuous_at.comp hcont
 
 end is_R_or_C

src/analysis/calculus/times_cont_diff.lean

@@ -164,7 +164,7 @@ local notation `∞` := (⊤ : with_top ℕ)
 universes u v w
 
 local attribute [instance, priority 1001]
-normed_group.to_add_comm_group normed_space.to_module add_comm_group.to_add_comm_monoid
+normed_group.to_add_comm_group normed_space.to_module' add_comm_group.to_add_comm_monoid
 
 open set fin filter
 open_locale topological_space
@@ -2830,7 +2830,9 @@ begin
       by { ext x, simp [deriv_within] },
     simp only [this],
     apply times_cont_diff.comp_times_cont_diff_on _ h,
-    exact (is_bounded_bilinear_map_smul_right.is_bounded_linear_map_right _).times_cont_diff }
+    have : is_bounded_bilinear_map 𝕜 (λ _ : (𝕜 →L[𝕜] 𝕜) × F, _) :=
+      is_bounded_bilinear_map_smul_right,
+    exact (this.is_bounded_linear_map_right _).times_cont_diff }
 end
 
 /-- A function is `C^(n + 1)` on an open domain if and only if it is

src/analysis/normed_space/add_torsor.lean

@@ -273,7 +273,7 @@ end
 
 section normed_space
 
-variables {𝕜 : Type*} [normed_field 𝕜] [semi_normed_space 𝕜 V]
+variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 V]
 
 open affine_map
 
@@ -324,7 +324,7 @@ end
 
 end normed_space
 
-variables [semi_normed_space ℝ V] [normed_space ℝ W]
+variables [normed_space ℝ V] [normed_space ℝ W]
 
 lemma dist_midpoint_midpoint_le (p₁ p₂ p₃ p₄ : V) :
   dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2 :=

src/analysis/normed_space/affine_isometry.lean

@@ -34,8 +34,8 @@ variables (𝕜 : Type*) {V V₁ V₂ V₃ V₄ : Type*} {P₁ : Type*} (P P₂
     [normed_field 𝕜]
   [semi_normed_group V] [normed_group V₁] [semi_normed_group V₂] [semi_normed_group V₃]
     [semi_normed_group V₄]
-  [semi_normed_space 𝕜 V] [normed_space 𝕜 V₁] [semi_normed_space 𝕜 V₂] [semi_normed_space 𝕜 V₃]
-    [semi_normed_space 𝕜 V₄]
+  [normed_space 𝕜 V] [normed_space 𝕜 V₁] [normed_space 𝕜 V₂] [normed_space 𝕜 V₃]
+    [normed_space 𝕜 V₄]
   [pseudo_metric_space P] [metric_space P₁] [pseudo_metric_space P₂] [pseudo_metric_space P₃]
     [pseudo_metric_space P₄]
   [semi_normed_add_torsor V P] [normed_add_torsor V₁ P₁] [semi_normed_add_torsor V₂ P₂]
@@ -519,7 +519,7 @@ lemma point_reflection_fixed_iff [invertible (2:𝕜)] {x y : P} :
   point_reflection 𝕜 x y = y ↔ y = x :=
 affine_equiv.point_reflection_fixed_iff_of_module 𝕜
 
-variables [semi_normed_space ℝ V]
+variables [normed_space ℝ V]
 
 lemma dist_point_reflection_self_real (x y : P) :
   dist (point_reflection ℝ x y) y = 2 * dist x y :=

src/analysis/normed_space/banach_steinhaus.lean

@@ -25,7 +25,7 @@ variables
 {E F 𝕜 𝕜₂ : Type*}
 [semi_normed_group E] [semi_normed_group F]
 [nondiscrete_normed_field 𝕜] [nondiscrete_normed_field 𝕜₂]
-[semi_normed_space 𝕜 E] [semi_normed_space 𝕜₂ F]
+[normed_space 𝕜 E] [normed_space 𝕜₂ F]
 {σ₁₂ : 𝕜 →+* 𝕜₂} [ring_hom_isometric σ₁₂]