chore: Rename Type* to Type _ (#1866)

A bunch of docstrings were still mentioning `Type*`. This changes them to `Type _`.

Mathlib/Algebra/Hom/Group.lean

@@ -81,7 +81,7 @@ section Zero
 /-- `ZeroHom M N` is the type of functions `M → N` that preserve zero.
 
 When possible, instead of parametrizing results over `(f : ZeroHom M N)`,
-you should parametrize over `(F : Type*) [ZeroHomClass F M N] (f : F)`.
+you should parametrize over `(F : Type _) [ZeroHomClass F M N] (f : F)`.
 
 When you extend this structure, make sure to also extend `ZeroHomClass`.
 -/
@@ -128,7 +128,7 @@ section Add
 /-- `AddHom M N` is the type of functions `M → N` that preserve addition.
 
 When possible, instead of parametrizing results over `(f : AddHom M N)`,
-you should parametrize over `(F : Type*) [AddHomClass F M N] (f : F)`.
+you should parametrize over `(F : Type _) [AddHomClass F M N] (f : F)`.
 
 When you extend this structure, make sure to extend `AddHomClass`.
 -/
@@ -158,7 +158,7 @@ section add_zero
 `AddMonoidHom` is also used for group homomorphisms.
 
 When possible, instead of parametrizing results over `(f : M →+ N)`,
-you should parametrize over `(F : Type*) [AddMonoidHomClass F M N] (f : F)`.
+you should parametrize over `(F : Type _) [AddMonoidHomClass F M N] (f : F)`.
 
 When you extend this structure, make sure to extend `AddMonoidHomClass`.
 -/
@@ -191,7 +191,7 @@ variable [One M] [One N]
 /-- `OneHom M N` is the type of functions `M → N` that preserve one.
 
 When possible, instead of parametrizing results over `(f : OneHom M N)`,
-you should parametrize over `(F : Type*) [OneHomClass F M N] (f : F)`.
+you should parametrize over `(F : Type _) [OneHomClass F M N] (f : F)`.
 
 When you extend this structure, make sure to also extend `OneHomClass`.
 -/
@@ -280,7 +280,7 @@ stands for "non-unital" because it is intended to match the notation for `NonUni
 `NonUnitalRingHom`, so a `MulHom` is a non-unital monoid hom.
 
 When possible, instead of parametrizing results over `(f : M →ₙ* N)`,
-you should parametrize over `(F : Type*) [MulHomClass F M N] (f : F)`.
+you should parametrize over `(F : Type _) [MulHomClass F M N] (f : F)`.
 When you extend this structure, make sure to extend `MulHomClass`.
 -/
 @[to_additive]
@@ -354,7 +354,7 @@ variable [MulOneClass M] [MulOneClass N]
 `MonoidHom` is also used for group homomorphisms.
 
 When possible, instead of parametrizing results over `(f : M →+ N)`,
-you should parametrize over `(F : Type*) [MonoidHomClass F M N] (f : F)`.
+you should parametrize over `(F : Type _) [MonoidHomClass F M N] (f : F)`.
 
 When you extend this structure, make sure to extend `MonoidHomClass`.
 -/
@@ -492,7 +492,7 @@ the `MonoidWithZero` structure.
 `MonoidWithZeroHom` is also used for group homomorphisms.
 
 When possible, instead of parametrizing results over `(f : M →*₀ N)`,
-you should parametrize over `(F : Type*) [MonoidWithZeroHomClass F M N] (f : F)`.
+you should parametrize over `(F : Type _) [MonoidWithZeroHomClass F M N] (f : F)`.
 
 When you extend this structure, make sure to extend `MonoidWithZeroHomClass`.
 -/

Mathlib/Algebra/Order/Hom/Monoid.lean

@@ -70,7 +70,7 @@ structure.
 `OrderAddMonoidHom` is also used for ordered group homomorphisms.
 
 When possible, instead of parametrizing results over `(f : α →+o β)`,
-you should parametrize over `(F : Type*) [OrderAddMonoidHomClass F α β] (f : F)`.
+you should parametrize over `(F : Type _) [OrderAddMonoidHomClass F α β] (f : F)`.
 
 When you extend this structure, make sure to extend `OrderAddMonoidHomClass`. -/
 structure OrderAddMonoidHom (α β : Type _) [Preorder α] [Preorder β] [AddZeroClass α]
@@ -105,7 +105,7 @@ section Monoid
 `OrderMonoidHom` is also used for ordered group homomorphisms.
 
 When possible, instead of parametrizing results over `(f : α →*o β)`,
-you should parametrize over `(F : Type*) [OrderMonoidHomClass F α β] (f : F)`.
+you should parametrize over `(F : Type _) [OrderMonoidHomClass F α β] (f : F)`.
 
 When you extend this structure, make sure to extend `OrderMonoidHomClass`. -/
 @[to_additive]
@@ -169,7 +169,7 @@ the `MonoidWithZero` structure.
 `OrderMonoidWithZeroHom` is also used for group homomorphisms.
 
 When possible, instead of parametrizing results over `(f : α →+ β)`,
-you should parametrize over `(F : Type*) [OrderMonoidWithZeroHomClass F α β] (f : F)`.
+you should parametrize over `(F : Type _) [OrderMonoidWithZeroHomClass F α β] (f : F)`.
 
 When you extend this structure, make sure to extend `OrderMonoidWithZeroHomClass`. -/
 structure OrderMonoidWithZeroHom (α β : Type _) [Preorder α] [Preorder β] [MulZeroOneClass α]

Mathlib/Control/Functor.lean

@@ -91,7 +91,7 @@ def Const.mk {α β} (x : α) : Const α β :=
 #align functor.const.mk Functor.Const.mk
 
 /-- `Const.mk'` is `Const.mk` but specialized to map `α` to
-`Const α PUnit`, where `PUnit` is the terminal object in `Type*`. -/
+`Const α PUnit`, where `PUnit` is the terminal object in `Type _`. -/
 def Const.mk' {α} (x : α) : Const α PUnit :=
   x
 #align functor.const.mk' Functor.Const.mk'

Mathlib/Data/Bundle.lean

@@ -15,7 +15,7 @@ import Mathlib.Algebra.Module.Basic
 Basic data structure to implement fiber bundles, vector bundles (maybe fibrations?), etc. This file
 should contain all possible results that do not involve any topology.
 
-We represent a bundle `E` over a base space `B` as a dependent type `E : B → Type*`.
+We represent a bundle `E` over a base space `B` as a dependent type `E : B → Type _`.
 
 We provide a type synonym of `Σ x, E x` as `Bundle.TotalSpace E`, to be able to endow it with
 a topology which is not the disjoint union topology `Sigma.TopologicalSpace`. In general, the

Mathlib/Data/Finite/Defs.lean

@@ -37,7 +37,7 @@ instead.
 ## Implementation notes
 
 The definition of `Finite α` is not just `NonEmpty (Fintype α)` since `Fintype` requires
-that `α : Type*`, and the definition in this module allows for `α : Sort*`. This means
+that `α : Type _`, and the definition in this module allows for `α : Sort*`. This means
 we can write the instance `Finite.prop`.
 
 ## Tags

Mathlib/Data/Finset/Lattice.lean

@@ -1703,7 +1703,7 @@ section Lattice
 variable {ι' : Sort _} [CompleteLattice α]
 
 /-- Supremum of `s i`, `i : ι`, is equal to the supremum over `t : Finset ι` of suprema
-`⨆ i ∈ t, s i`. This version assumes `ι` is a `Type*`. See `supᵢ_eq_supᵢ_finset'` for a version
+`⨆ i ∈ t, s i`. This version assumes `ι` is a `Type _`. See `supᵢ_eq_supᵢ_finset'` for a version
 that works for `ι : Sort*`. -/
 theorem supᵢ_eq_supᵢ_finset (s : ι → α) : (⨆ i, s i) = ⨆ t : Finset ι, ⨆ i ∈ t, s i := by
   classical
@@ -1714,22 +1714,22 @@ theorem supᵢ_eq_supᵢ_finset (s : ι → α) : (⨆ i, s i) = ⨆ t : Finset
 
 /-- Supremum of `s i`, `i : ι`, is equal to the supremum over `t : Finset ι` of suprema
 `⨆ i ∈ t, s i`. This version works for `ι : Sort*`. See `supᵢ_eq_supᵢ_finset` for a version
-that assumes `ι : Type*` but has no `plift`s. -/
+that assumes `ι : Type _` but has no `plift`s. -/
 theorem supᵢ_eq_supᵢ_finset' (s : ι' → α) :
     (⨆ i, s i) = ⨆ t : Finset (PLift ι'), ⨆ i ∈ t, s (PLift.down i) := by
   rw [← supᵢ_eq_supᵢ_finset, ← Equiv.plift.surjective.supᵢ_comp]; rfl
 #align supr_eq_supr_finset' supᵢ_eq_supᵢ_finset'
 
 /-- Infimum of `s i`, `i : ι`, is equal to the infimum over `t : Finset ι` of infima
-`⨅ i ∈ t, s i`. This version assumes `ι` is a `Type*`. See `infᵢ_eq_infᵢ_finset'` for a version
+`⨅ i ∈ t, s i`. This version assumes `ι` is a `Type _`. See `infᵢ_eq_infᵢ_finset'` for a version
 that works for `ι : Sort*`. -/
 theorem infᵢ_eq_infᵢ_finset (s : ι → α) : (⨅ i, s i) = ⨅ (t : Finset ι) (i ∈ t), s i :=
   @supᵢ_eq_supᵢ_finset αᵒᵈ _ _ _
 #align infi_eq_infi_finset infᵢ_eq_infᵢ_finset
 
 /-- Infimum of `s i`, `i : ι`, is equal to the infimum over `t : Finset ι` of infima
 `⨅ i ∈ t, s i`. This version works for `ι : Sort*`. See `infᵢ_eq_infᵢ_finset` for a version
-that assumes `ι : Type*` but has no `plift`s. -/
+that assumes `ι : Type _` but has no `plift`s. -/
 theorem infᵢ_eq_infᵢ_finset' (s : ι' → α) :
     (⨅ i, s i) = ⨅ t : Finset (PLift ι'), ⨅ i ∈ t, s (PLift.down i) :=
   @supᵢ_eq_supᵢ_finset' αᵒᵈ _ _ _
@@ -1742,30 +1742,30 @@ namespace Set
 variable {ι' : Sort _}
 
 /-- Union of an indexed family of sets `s : ι → Set α` is equal to the union of the unions
-of finite subfamilies. This version assumes `ι : Type*`. See also `unionᵢ_eq_unionᵢ_finset'` for
+of finite subfamilies. This version assumes `ι : Type _`. See also `unionᵢ_eq_unionᵢ_finset'` for
 a version that works for `ι : Sort*`. -/
 theorem unionᵢ_eq_unionᵢ_finset (s : ι → Set α) : (⋃ i, s i) = ⋃ t : Finset ι, ⋃ i ∈ t, s i :=
   supᵢ_eq_supᵢ_finset s
 #align set.Union_eq_Union_finset Set.unionᵢ_eq_unionᵢ_finset
 
 /-- Union of an indexed family of sets `s : ι → Set α` is equal to the union of the unions
 of finite subfamilies. This version works for `ι : Sort*`. See also `unionᵢ_eq_unionᵢ_finset` for
-a version that assumes `ι : Type*` but avoids `plift`s in the right hand side. -/
+a version that assumes `ι : Type _` but avoids `plift`s in the right hand side. -/
 theorem unionᵢ_eq_unionᵢ_finset' (s : ι' → Set α) :
     (⋃ i, s i) = ⋃ t : Finset (PLift ι'), ⋃ i ∈ t, s (PLift.down i) :=
   supᵢ_eq_supᵢ_finset' s
 #align set.Union_eq_Union_finset' Set.unionᵢ_eq_unionᵢ_finset'
 
 /-- Intersection of an indexed family of sets `s : ι → Set α` is equal to the intersection of the
-intersections of finite subfamilies. This version assumes `ι : Type*`. See also
+intersections of finite subfamilies. This version assumes `ι : Type _`. See also
 `interᵢ_eq_interᵢ_finset'` for a version that works for `ι : Sort*`. -/
 theorem interᵢ_eq_interᵢ_finset (s : ι → Set α) : (⋂ i, s i) = ⋂ t : Finset ι, ⋂ i ∈ t, s i :=
   infᵢ_eq_infᵢ_finset s
 #align set.Inter_eq_Inter_finset Set.interᵢ_eq_interᵢ_finset
 
 /-- Intersection of an indexed family of sets `s : ι → Set α` is equal to the intersection of the
 intersections of finite subfamilies. This version works for `ι : Sort*`. See also
-`interᵢ_eq_interᵢ_finset` for a version that assumes `ι : Type*` but avoids `plift`s in the right
+`interᵢ_eq_interᵢ_finset` for a version that assumes `ι : Type _` but avoids `plift`s in the right
 hand side. -/
 theorem interᵢ_eq_interᵢ_finset' (s : ι' → Set α) :
     (⋂ i, s i) = ⋂ t : Finset (PLift ι'), ⋂ i ∈ t, s (PLift.down i) :=

Mathlib/Data/Fintype/Card.lean

@@ -400,7 +400,7 @@ noncomputable def Fintype.sumRight {α β} [Fintype (Sum α β)] : Fintype β :=
 /-!
 ### Relation to `Finite`
 
-In this section we prove that `α : Type*` is `Finite` if and only if `Fintype α` is nonempty.
+In this section we prove that `α : Type _` is `Finite` if and only if `Fintype α` is nonempty.
 -/
 
 

Mathlib/Data/FunLike/Basic.lean

@@ -20,13 +20,13 @@ This typeclass is primarily for use by homomorphisms like `MonoidHom` and `Linea
 
 A typical type of morphisms should be declared as:
 ```
-structure MyHom (A B : Type*) [MyClass A] [MyClass B] :=
+structure MyHom (A B : Type _) [MyClass A] [MyClass B] :=
 (toFun : A → B)
 (map_op' : ∀ {x y : A}, toFun (MyClass.op x y) = MyClass.op (toFun x) (toFun y))
 
 namespace MyHom
 
-variables (A B : Type*) [MyClass A] [MyClass B]
+variables (A B : Type _) [MyClass A] [MyClass B]
 
 -- This instance is optional if you follow the "morphism class" design below:
 instance : FunLike (MyHom A B) A (λ _, B) :=
@@ -60,11 +60,11 @@ Continuing the example above:
 ```
 /-- `MyHomClass F A B` states that `F` is a type of `MyClass.op`-preserving morphisms.
 You should extend this class when you extend `MyHom`. -/
-class MyHomClass (F : Type*) (A B : outParam <| Type*) [MyClass A] [MyClass B]
+class MyHomClass (F : Type _) (A B : outParam <| Type _) [MyClass A] [MyClass B]
   extends FunLike F A (λ _, B) :=
 (map_op : ∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y))
 
-@[simp] lemma map_op {F A B : Type*} [MyClass A] [MyClass B] [MyHomClass F A B]
+@[simp] lemma map_op {F A B : Type _} [MyClass A] [MyClass B] [MyHomClass F A B]
   (f : F) (x y : A) : f (MyClass.op x y) = MyClass.op (f x) (f y) :=
 MyHomClass.map_op
 
@@ -81,15 +81,15 @@ The second step is to add instances of your new `MyHomClass` for all types exten
 Typically, you can just declare a new class analogous to `MyHomClass`:
 
 ```
-structure CoolerHom (A B : Type*) [CoolClass A] [CoolClass B]
+structure CoolerHom (A B : Type _) [CoolClass A] [CoolClass B]
   extends MyHom A B :=
 (map_cool' : toFun CoolClass.cool = CoolClass.cool)
 
-class CoolerHomClass (F : Type*) (A B : outParam <| Type*) [CoolClass A] [CoolClass B]
+class CoolerHomClass (F : Type _) (A B : outParam <| Type _) [CoolClass A] [CoolClass B]
   extends MyHomClass F A B :=
 (map_cool : ∀ (f : F), f CoolClass.cool = CoolClass.cool)
 
-@[simp] lemma map_cool {F A B : Type*} [CoolClass A] [CoolClass B] [CoolerHomClass F A B]
+@[simp] lemma map_cool {F A B : Type _} [CoolClass A] [CoolClass B] [CoolerHomClass F A B]
   (f : F) : f CoolClass.cool = CoolClass.cool :=
 MyHomClass.map_op
 
@@ -107,7 +107,7 @@ Then any declaration taking a specific type of morphisms as parameter can instea
 class you just defined:
 ```
 -- Compare with: lemma do_something (f : MyHom A B) : sorry := sorry
-lemma do_something {F : Type*} [MyHomClass F A B] (f : F) : sorry := sorry
+lemma do_something {F : Type _} [MyHomClass F A B] (f : F) : sorry := sorry
 ```
 
 This means anything set up for `MyHom`s will automatically work for `CoolerHomClass`es,

Mathlib/Data/FunLike/Embedding.lean

@@ -19,14 +19,14 @@ This typeclass is primarily for use by embeddings such as `RelEmbedding`.
 
 A typical type of embeddings should be declared as:
 ```
-structure MyEmbedding (A B : Type*) [MyClass A] [MyClass B] :=
+structure MyEmbedding (A B : Type _) [MyClass A] [MyClass B] :=
 (toFun : A → B)
 (injective' : Function.Injective toFun)
 (map_op' : ∀ {x y : A}, toFun (MyClass.op x y) = MyClass.op (toFun x) (toFun y))
 
 namespace MyEmbedding
 
-variables (A B : Type*) [MyClass A] [MyClass B]
+variables (A B : Type _) [MyClass A] [MyClass B]
 
 -- This instance is optional if you follow the "Embedding class" design below:
 instance : EmbeddingLike (MyEmbedding A B) A B :=
@@ -64,13 +64,13 @@ section
 
 /-- `MyEmbeddingClass F A B` states that `F` is a type of `MyClass.op`-preserving embeddings.
 You should extend this class when you extend `MyEmbedding`. -/
-class MyEmbeddingClass (F : Type*) (A B : outParam <| Type*) [MyClass A] [MyClass B]
+class MyEmbeddingClass (F : Type _) (A B : outParam <| Type _) [MyClass A] [MyClass B]
   extends EmbeddingLike F A B :=
 (map_op : ∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y))
 
 end
 
-@[simp] lemma map_op {F A B : Type*} [MyClass A] [MyClass B] [MyEmbeddingClass F A B]
+@[simp] lemma map_op {F A B : Type _} [MyClass A] [MyClass B] [MyEmbeddingClass F A B]
   (f : F) (x y : A) : f (MyClass.op x y) = MyClass.op (f x) (f y) :=
 MyEmbeddingClass.map_op
 
@@ -89,20 +89,20 @@ The second step is to add instances of your new `MyEmbeddingClass` for all types
 Typically, you can just declare a new class analogous to `MyEmbeddingClass`:
 
 ```
-structure CoolerEmbedding (A B : Type*) [CoolClass A] [CoolClass B]
+structure CoolerEmbedding (A B : Type _) [CoolClass A] [CoolClass B]
   extends MyEmbedding A B :=
 (map_cool' : toFun CoolClass.cool = CoolClass.cool)
 
 section
 set_option old_structure_cmd true
 
-class CoolerEmbeddingClass (F : Type*) (A B : outParam <| Type*) [CoolClass A] [CoolClass B]
+class CoolerEmbeddingClass (F : Type _) (A B : outParam <| Type _) [CoolClass A] [CoolClass B]
   extends MyEmbeddingClass F A B :=
 (map_cool : ∀ (f : F), f CoolClass.cool = CoolClass.cool)
 
 end
 
-@[simp] lemma map_cool {F A B : Type*} [CoolClass A] [CoolClass B] [CoolerEmbeddingClass F A B]
+@[simp] lemma map_cool {F A B : Type _} [CoolClass A] [CoolClass B] [CoolerEmbeddingClass F A B]
   (f : F) : f CoolClass.cool = CoolClass.cool :=
 MyEmbeddingClass.map_op
 
@@ -121,7 +121,7 @@ Then any declaration taking a specific type of morphisms as parameter can instea
 class you just defined:
 ```
 -- Compare with: lemma do_something (f : MyEmbedding A B) : sorry := sorry
-lemma do_something {F : Type*} [MyEmbeddingClass F A B] (f : F) : sorry := sorry
+lemma do_something {F : Type _} [MyEmbeddingClass F A B] (f : F) : sorry := sorry
 ```
 
 This means anything set up for `MyEmbedding`s will automatically work for `CoolerEmbeddingClass`es,

Mathlib/Data/FunLike/Equiv.lean

@@ -19,13 +19,13 @@ This typeclass is primarily for use by isomorphisms like `MonoidEquiv` and `Line
 
 A typical type of morphisms should be declared as:
 ```
-structure MyIso (A B : Type*) [MyClass A] [MyClass B]
+structure MyIso (A B : Type _) [MyClass A] [MyClass B]
   extends Equiv A B :=
 (map_op' : ∀ {x y : A}, toFun (MyClass.op x y) = MyClass.op (toFun x) (toFun y))
 
 namespace MyIso
 
-variables (A B : Type*) [MyClass A] [MyClass B]
+variables (A B : Type _) [MyClass A] [MyClass B]
 
 -- This instance is optional if you follow the "Isomorphism class" design below:
 instance : EquivLike (MyIso A B) A (λ _, B) :=
@@ -66,7 +66,7 @@ Continuing the example above:
 
 /-- `MyIsoClass F A B` states that `F` is a type of `MyClass.op`-preserving morphisms.
 You should extend this class when you extend `MyIso`. -/
-class MyIsoClass (F : Type*) (A B : outParam <| Type _) [MyClass A] [MyClass B]
+class MyIsoClass (F : Type _) (A B : outParam <| Type _) [MyClass A] [MyClass B]
   extends EquivLike F A (λ _, B), MyHomClass F A B
 
 end
@@ -87,20 +87,20 @@ The second step is to add instances of your new `MyIsoClass` for all types exten
 Typically, you can just declare a new class analogous to `MyIsoClass`:
 
 ```
-structure CoolerIso (A B : Type*) [CoolClass A] [CoolClass B]
+structure CoolerIso (A B : Type _) [CoolClass A] [CoolClass B]
   extends MyIso A B :=
 (map_cool' : toFun CoolClass.cool = CoolClass.cool)
 
 section
 set_option old_structure_cmd true
 
-class CoolerIsoClass (F : Type*) (A B : outParam <| Type _) [CoolClass A] [CoolClass B]
+class CoolerIsoClass (F : Type _) (A B : outParam <| Type _) [CoolClass A] [CoolClass B]
   extends MyIsoClass F A B :=
 (map_cool : ∀ (f : F), f CoolClass.cool = CoolClass.cool)
 
 end
 
-@[simp] lemma map_cool {F A B : Type*} [CoolClass A] [CoolClass B] [CoolerIsoClass F A B]
+@[simp] lemma map_cool {F A B : Type _} [CoolClass A] [CoolClass B] [CoolerIsoClass F A B]
   (f : F) : f CoolClass.cool = CoolClass.cool :=
 CoolerIsoClass.map_cool
 
@@ -117,7 +117,7 @@ Then any declaration taking a specific type of morphisms as parameter can instea
 class you just defined:
 ```
 -- Compare with: lemma do_something (f : MyIso A B) : sorry := sorry
-lemma do_something {F : Type*} [MyIsoClass F A B] (f : F) : sorry := sorry
+lemma do_something {F : Type _} [MyIsoClass F A B] (f : F) : sorry := sorry
 ```
 
 This means anything set up for `MyIso`s will automatically work for `CoolerIsoClass`es,

Mathlib/Data/List/Sigma.lean

@@ -16,7 +16,7 @@ import Mathlib.Data.List.Perm
 
 This file includes several ways of interacting with `List (Sigma β)`, treated as a key-value store.
 
-If `α : Type*` and `β : α → Type*`, then we regard `s : Sigma β` as having key `s.1 : α` and value
+If `α : Type _` and `β : α → Type _`, then we regard `s : Sigma β` as having key `s.1 : α` and value
 `s.2 : β s.1`. Hence, `list (sigma β)` behaves like a key-value store.
 
 ## Main Definitions
@@ -475,7 +475,7 @@ theorem Perm.kerase {a : α} {l₁ l₂ : List (Sigma β)} (nd : l₁.NodupKeys)
 #align list.perm.kerase List.Perm.kerase
 
 @[simp]
-theorem not_mem_keys_kerase (a) {l : List (Sigma β)} (nd : l.NodupKeys) : 
+theorem not_mem_keys_kerase (a) {l : List (Sigma β)} (nd : l.NodupKeys) :
     a ∉ (kerase a l).keys := by
   induction l
   case nil => simp