refactor(analysis/inner_product_space/basic): do not extend normed_add_comm_group (#18583)

This replaces `[inner_product_space K V]` with `[normed_add_comm_group V] [inner_product_space K V]`.

Before this PR, we had `inner_product_space K V extends normed_add_comm_group V`.
At first glance this is a rather strange arrangement; we certainly don't have `module R V extends add_comm_group V`.
The argument usually goes that `Derived A B extends Base B` is unsafe, because the `Derived.toBase` instance has no way of knowing which `A` to look for.

For `inner_product_space K V` we argued that this problem doesn't apply, as `is_R_or_C K` means that in practice there are only two possible values of `K`. This is indeed enough to stop typeclass search grinding to a halt.

The motivation for the old design is described by @dupuisf [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Dangerous.20instance.20vs.20elaboration.20problems/near/210594971):

> However, when I do (the contents of this PR), I run into some very annoying elaboration issues where I have to constantly spoonfeed it `𝕜` and/or `α` in lemmas that rewrite norms in terms of inner products, even though the relevant instance is directly present in the context.

While it may ease elaboration issues, there are a number of new problems that `inner_product_space K V extends normed_add_comm_group V` causes:
1. It is confusing when compared to all other typeclasses. After being told to write
    ```lean
    variables [add_comm_group U] [module R U]
    variables [normed_add_comm_group V] [normed_space R V]
    ```
    it is natural to assume that the inner product space version would be
    ```lean
    variables [normed_add_comm_group W] [inner_product_space K W]
    ```
    But writing this leads to `W` having two unrelated addition operations!
2. It doesn't allow a space `W` to be an inner product space over both R and C. For a (normed) module, you can write
    ```lean
    variables [add_comm_group U] [module R U] [module C U]
    variables [normed_add_comm_group V] [normed_space R V] [normed_space C V]
    ```
    but writing `[inner_product_space R W] [inner_product_space C W]` again puts two unrelated `+` operators on `V`
3. It doesn't compose with other normed typeclasses. We can talk about a (normed) module with multiplication as
    ```lean
    variables [ring U] [module R U]
    variables [normed_ring V] [normed_space K V]
    ```
    but once again, typing `[normed_ring W] [inner_product_space K W]` gives us two unrelated `+` operators.
    This prevents us generalizing over `real`, `complex`, and `quaternion`.

    We could work around this by defining variants of `inner_product_space` for `normed_ring A`, `normed_comm_ring A`, `normed_division_ring A`, `normed_field A`, but this doesn't scale well. If we do things "the module way" then we only need one new typeclass instead of four,
    ```lean
    class inner_product_algebra (K A) [is_R_or_C K] [normed_ring A]
      extends normed_algebra K A, inner_product_space K A
    ```
5. The "`is_R_or_C` makes it OK" argument stops working if we generalize to [quaternionic inner product spaces](https://link.springer.com/chapter/10.1007/978-94-009-3713-0_13)

The majority of this PR is adding `[normed_add_comm_group _]` to every `variables` line about `inner_product_space`.
The rest is specifying the scalar manually where previously unification would find it for us.

[This Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/inner_product_space.20and.20normed_algebra/near/341848831) has some initial discussion about this change.

Author: eric-wieser

archive/100-theorems-list/57_herons_formula.lean

@@ -23,8 +23,8 @@ open_locale real euclidean_geometry
 
 local notation `√` := real.sqrt
 
-variables {V : Type*} {P : Type*} [inner_product_space ℝ V] [metric_space P]
-  [normed_add_torsor V P]
+variables {V : Type*} {P : Type*}
+  [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P]
 
 include V
 

archive/imo/imo2019_q2.lean

@@ -63,7 +63,8 @@ open_locale affine euclidean_geometry real
 
 local attribute [instance] fact_finite_dimensional_of_finrank_eq_succ
 
-variables (V : Type*) (Pt : Type*) [inner_product_space ℝ V] [metric_space Pt]
+variables (V : Type*) (Pt : Type*)
+variables [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space Pt]
 variables [normed_add_torsor V Pt] [hd2 : fact (finrank ℝ V = 2)]
 include hd2
 

src/analysis/calculus/bump_function_inner.lean

@@ -306,7 +306,7 @@ nonempty.some hb.out
 
 /-- Any inner product space has smooth bump functions. -/
 @[priority 100] instance has_cont_diff_bump_of_inner_product_space
-  (E : Type*) [inner_product_space ℝ E] : has_cont_diff_bump E :=
+  (E : Type*) [normed_add_comm_group E] [inner_product_space ℝ E] : has_cont_diff_bump E :=
 let e : cont_diff_bump_base E :=
 { to_fun := λ R x, real.smooth_transition ((R - ‖x‖) / (R - 1)),
   mem_Icc := λ R x, ⟨real.smooth_transition.nonneg _, real.smooth_transition.le_one _⟩,
@@ -331,7 +331,7 @@ let e : cont_diff_bump_base E :=
       exact cont_diff_at_const.congr_of_eventually_eq this },
     { refine real.smooth_transition.cont_diff_at.comp _ _,
       refine cont_diff_at.div _ _ (sub_pos.2 hR).ne',
-      { exact cont_diff_at_fst.sub (cont_diff_at_snd.norm hx) },
+      { exact cont_diff_at_fst.sub (cont_diff_at_snd.norm ℝ hx) },
       { exact cont_diff_at_fst.sub cont_diff_at_const } }
   end,
   eq_one := λ R hR x hx, real.smooth_transition.one_of_one_le $

src/analysis/calculus/conformal/inner_product.lean

@@ -15,7 +15,9 @@ is conformal at `x` iff the derivative preserves inner products up to a scalar m
 
 noncomputable theory
 
-variables {E F : Type*} [inner_product_space ℝ E] [inner_product_space ℝ F]
+variables {E F : Type*}
+variables [normed_add_comm_group E] [normed_add_comm_group F]
+variables [inner_product_space ℝ E] [inner_product_space ℝ F]
 
 open_locale real_inner_product_space
 

src/analysis/convex/cone/basic.lean

@@ -717,7 +717,7 @@ end
 /-! ### The dual cone -/
 
 section dual
-variables {H : Type*} [inner_product_space ℝ H] (s t : set H)
+variables {H : Type*} [normed_add_comm_group H] [inner_product_space ℝ H] (s t : set H)
 open_locale real_inner_product_space
 
 /-- The dual cone is the cone consisting of all points `y` such that for

src/analysis/fourier/add_circle.lean

@@ -426,7 +426,7 @@ begin
   { exact_mod_cast lp.norm_rpow_eq_tsum _ (fourier_basis.repr f),
     norm_num },
   have H₂ : ‖fourier_basis.repr f‖ ^ 2 = ‖f‖ ^ 2 := by simp,
-  have H₃ := congr_arg is_R_or_C.re (@L2.inner_def (add_circle T) ℂ ℂ _ _ _ _ f f),
+  have H₃ := congr_arg is_R_or_C.re (@L2.inner_def (add_circle T) ℂ ℂ _ _ _ _ _ f f),
   rw ← integral_re at H₃,
   { simp only [← norm_sq_eq_inner] at H₃,
     rw [← H₁, H₂, H₃], },

src/analysis/inner_product_space/adjoint.lean

@@ -44,6 +44,7 @@ open is_R_or_C
 open_locale complex_conjugate
 
 variables {𝕜 E F G : Type*} [is_R_or_C 𝕜]
+variables [normed_add_comm_group E] [normed_add_comm_group F] [normed_add_comm_group G]
 variables [inner_product_space 𝕜 E] [inner_product_space 𝕜 F] [inner_product_space 𝕜 G]
 local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y
 
@@ -206,7 +207,9 @@ end⟩
 
 section real
 
-variables {E' : Type*} {F' : Type*} [inner_product_space ℝ E'] [inner_product_space ℝ F']
+variables {E' : Type*} {F' : Type*}
+variables [normed_add_comm_group E'] [normed_add_comm_group F']
+variables [inner_product_space ℝ E'] [inner_product_space ℝ F']
 variables [complete_space E'] [complete_space F']
 
 -- Todo: Generalize this to `is_R_or_C`.
@@ -402,7 +405,9 @@ by { rw [is_self_adjoint_iff', is_symmetric, ← linear_map.eq_adjoint_iff], exa
 
 section real
 
-variables {E' : Type*} {F' : Type*} [inner_product_space ℝ E'] [inner_product_space ℝ F']
+variables {E' : Type*} {F' : Type*}
+variables [normed_add_comm_group E'] [normed_add_comm_group F']
+variables [inner_product_space ℝ E'] [inner_product_space ℝ F']
 variables [finite_dimensional ℝ E'] [finite_dimensional ℝ F']
 
 -- Todo: Generalize this to `is_R_or_C`.