fix(*): missing universe polymorphism (#18644)

These are all just typo fixes, no proof adaptations.

This deliberately leaves alone things related to category theory and algebraic geometry, as there the lack of polymorphism is likely deliberate.

src/analysis/normed_space/M_structure.lean

@@ -62,7 +62,7 @@ M-summand, M-projection, L-summand, L-projection, M-ideal, M-structure
 -/
 
 variables (X : Type*) [normed_add_comm_group X]
-variables {M : Type} [ring M] [module M X]
+variables {M : Type*} [ring M] [module M X]
 /--
 A projection on a normed space `X` is said to be an L-projection if, for all `x` in `X`,
 $\|x\| = \|P x\| + \|(1 - P) x\|$.

src/data/list/func.lean

@@ -354,15 +354,15 @@ by {apply get_pointwise, apply sub_zero}
   (sub xs ys).length = max xs.length ys.length :=
 @length_pointwise α α α ⟨0⟩ ⟨0⟩ _ _ _
 
-@[simp] lemma nil_sub {α : Type} [add_group α]
+@[simp] lemma nil_sub {α : Type*} [add_group α]
   (as : list α) : sub [] as = neg as :=
 begin
   rw [sub, nil_pointwise],
   congr' with x,
   rw [zero_sub]
 end
 
-@[simp] lemma sub_nil {α : Type} [add_group α]
+@[simp] lemma sub_nil {α : Type*} [add_group α]
   (as : list α) : sub as [] = as :=
 begin
   rw [sub, pointwise_nil],

src/field_theory/separable_degree.lean

@@ -41,7 +41,7 @@ open_locale classical polynomial
 
 section comm_semiring
 
-variables {F : Type} [comm_semiring F] (q : ℕ)
+variables {F : Type*} [comm_semiring F] (q : ℕ)
 
 /-- A separable contraction of a polynomial `f` is a separable polynomial `g` such that
 `g(x^(q^m)) = f(x)` for some `m : ℕ`.-/
@@ -86,7 +86,7 @@ end comm_semiring
 
 section field
 
-variables {F : Type} [field F]
+variables {F : Type*} [field F]
 variables (q : ℕ) {f : F[X]} (hf : has_separable_contraction q f)
 
 /-- Every irreducible polynomial can be contracted to a separable polynomial.

src/linear_algebra/bilinear_form.lean

@@ -405,7 +405,7 @@ end equiv_lin
 
 namespace linear_map
 
-variables {R' : Type} [comm_semiring R'] [algebra R' R] [module R' M] [is_scalar_tower R' R M]
+variables {R' : Type*} [comm_semiring R'] [algebra R' R] [module R' M] [is_scalar_tower R' R M]
 
 /-- Apply a linear map on the output of a bilinear form. -/
 @[simps]

src/logic/equiv/list.lean

@@ -347,7 +347,7 @@ def list_unit_equiv : list unit ≃ ℕ :=
 def list_nat_equiv_nat : list ℕ ≃ ℕ := denumerable.eqv _
 
 /-- If `α` is equivalent to `ℕ`, then `list α` is equivalent to `α`. -/
-def list_equiv_self_of_equiv_nat {α : Type} (e : α ≃ ℕ) : list α ≃ α :=
+def list_equiv_self_of_equiv_nat {α : Type*} (e : α ≃ ℕ) : list α ≃ α :=
 calc list α ≃ list ℕ : list_equiv_of_equiv e
         ... ≃ ℕ      : list_nat_equiv_nat
         ... ≃ α      : e.symm

src/measure_theory/integral/circle_transform.lean

@@ -22,7 +22,7 @@ open_locale interval real
 
 noncomputable theory
 
-variables {E : Type} [normed_add_comm_group E] [normed_space ℂ E] (R : ℝ) (z w : ℂ)
+variables {E : Type*} [normed_add_comm_group E] [normed_space ℂ E] (R : ℝ) (z w : ℂ)
 
 namespace complex
 

src/model_theory/elementary_maps.lean

@@ -59,7 +59,7 @@ instance fun_like : fun_like (M ↪ₑ[L] N) M (λ _, N) :=
 
 instance : has_coe_to_fun (M ↪ₑ[L] N) (λ _, M → N) := fun_like.has_coe_to_fun
 
-@[simp] lemma map_bounded_formula (f : M ↪ₑ[L] N) {α : Type} {n : ℕ}
+@[simp] lemma map_bounded_formula (f : M ↪ₑ[L] N) {α : Type*} {n : ℕ}
   (φ : L.bounded_formula α n) (v : α → M) (xs : fin n → M) :
   φ.realize (f ∘ v) (f ∘ xs) ↔ φ.realize v xs :=
 begin
@@ -80,7 +80,7 @@ begin
     bounded_formula.realize_restrict_free_var set.subset.rfl],
 end
 
-@[simp] lemma map_formula (f : M ↪ₑ[L] N) {α : Type} (φ : L.formula α) (x : α → M) :
+@[simp] lemma map_formula (f : M ↪ₑ[L] N) {α : Type*} (φ : L.formula α) (x : α → M) :
   φ.realize (f ∘ x) ↔ φ.realize x :=
 by rw [formula.realize, formula.realize, ← f.map_bounded_formula, unique.eq_default (f ∘ default)]
 

src/number_theory/legendre_symbol/gauss_sum.lean

@@ -207,7 +207,7 @@ end
 
 /-- When `F` and `F'` are finite fields and `χ : F → F'` is a nontrivial quadratic character,
 then `(χ(-1) * #F)^(#F'/2) = χ(#F')`. -/
-lemma char.card_pow_card {F : Type} [field F] [fintype F] {F' : Type} [field F'] [fintype F']
+lemma char.card_pow_card {F : Type*} [field F] [fintype F] {F' : Type*} [field F'] [fintype F']
   {χ : mul_char F F'} (hχ₁ : is_nontrivial χ) (hχ₂ : is_quadratic χ)
   (hch₁ : ring_char F' ≠ ring_char F) (hch₂ : ring_char F' ≠ 2) :
   (χ (-1) * fintype.card F) ^ (fintype.card F' / 2) = χ (fintype.card F') :=

src/number_theory/legendre_symbol/quadratic_char.lean

@@ -287,7 +287,7 @@ section special_values
 
 open zmod mul_char
 
-variables {F : Type} [field F] [fintype F]
+variables {F : Type*} [field F] [fintype F]
 
 /-- The value of the quadratic character at `-1` -/
 lemma quadratic_char_neg_one [decidable_eq F] (hF : ring_char F ≠ 2) :
@@ -382,7 +382,7 @@ end
 /-- The relation between the values of the quadratic character of one field `F` at the
 cardinality of another field `F'` and of the quadratic character of `F'` at the cardinality
 of `F`. -/
-lemma quadratic_char_card_card [decidable_eq F] (hF : ring_char F ≠ 2) {F' : Type} [field F']
+lemma quadratic_char_card_card [decidable_eq F] (hF : ring_char F ≠ 2) {F' : Type*} [field F']
   [fintype F'] [decidable_eq F'] (hF' : ring_char F' ≠ 2) (h : ring_char F' ≠ ring_char F) :
   quadratic_char F (fintype.card F') = quadratic_char F' (quadratic_char F (-1) * fintype.card F) :=
 begin