chore: banish Type _ and Sort _ (#6499)

We remove all possible occurences of `Type _` and `Sort _` in favor of `Type*` and `Sort*`.

This has nice performance benefits.

Mathlib/Algebra/Abs.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Christopher Hoskin
 -/
 import Mathlib.Mathport.Rename
+import Mathlib.Tactic.Basic
 
 #align_import algebra.abs from "leanprover-community/mathlib"@"c4658a649d216f57e99621708b09dcb3dcccbd23"
 /-!
@@ -35,7 +36,7 @@ absolute
 /--
 Absolute value is a unary operator with properties similar to the absolute value of a real number.
 -/
-class Abs (α : Type _) where
+class Abs (α : Type*) where
   /-- The absolute value function. -/
   abs : α → α
 
@@ -45,15 +46,15 @@ export Abs (abs)
 
 /-- The positive part of an element admitting a decomposition into positive and negative parts.
 -/
-class PosPart (α : Type _) where
+class PosPart (α : Type*) where
   /-- The positive part function. -/
   pos : α → α
 
 #align has_pos_part PosPart
 
 /-- The negative part of an element admitting a decomposition into positive and negative parts.
 -/
-class NegPart (α : Type _) where
+class NegPart (α : Type*) where
   /-- The negative part function. -/
   neg : α → α
 

Mathlib/Algebra/AddTorsor.lean

@@ -45,7 +45,7 @@ acted on by an `AddGroup G` with a transitive and free action given
 by the `+ᵥ` operation and a corresponding subtraction given by the
 `-ᵥ` operation. In the case of a vector space, it is an affine
 space. -/
-class AddTorsor (G : outParam (Type _)) (P : Type _) [outParam <| AddGroup G] extends AddAction G P,
+class AddTorsor (G : outParam (Type*)) (P : Type*) [outParam <| AddGroup G] extends AddAction G P,
   VSub G P where
   [Nonempty : Nonempty P]
   /-- Torsor subtraction and addition with the same element cancels out. -/
@@ -61,7 +61,7 @@ attribute [instance 100] AddTorsor.Nonempty -- porting note: removers `nolint in
 
 /-- An `AddGroup G` is a torsor for itself. -/
 --@[nolint instance_priority] Porting note: linter does not exist
-instance addGroupIsAddTorsor (G : Type _) [AddGroup G] : AddTorsor G G
+instance addGroupIsAddTorsor (G : Type*) [AddGroup G] : AddTorsor G G
     where
   vsub := Sub.sub
   vsub_vadd' := sub_add_cancel
@@ -71,13 +71,13 @@ instance addGroupIsAddTorsor (G : Type _) [AddGroup G] : AddTorsor G G
 /-- Simplify subtraction for a torsor for an `AddGroup G` over
 itself. -/
 @[simp]
-theorem vsub_eq_sub {G : Type _} [AddGroup G] (g1 g2 : G) : g1 -ᵥ g2 = g1 - g2 :=
+theorem vsub_eq_sub {G : Type*} [AddGroup G] (g1 g2 : G) : g1 -ᵥ g2 = g1 - g2 :=
   rfl
 #align vsub_eq_sub vsub_eq_sub
 
 section General
 
-variable {G : Type _} {P : Type _} [AddGroup G] [T : AddTorsor G P]
+variable {G : Type*} {P : Type*} [AddGroup G] [T : AddTorsor G P]
 
 /-- Adding the result of subtracting from another point produces that
 point. -/
@@ -244,7 +244,7 @@ end General
 
 section comm
 
-variable {G : Type _} {P : Type _} [AddCommGroup G] [AddTorsor G P]
+variable {G : Type*} {P : Type*} [AddCommGroup G] [AddTorsor G P]
 
 -- Porting note: Removed:
 -- include G
@@ -278,7 +278,7 @@ end comm
 
 namespace Prod
 
-variable {G : Type _} [AddGroup G] [AddGroup G'] [AddTorsor G P] [AddTorsor G' P']
+variable {G : Type*} [AddGroup G] [AddGroup G'] [AddTorsor G P] [AddTorsor G' P']
 
 instance instAddTorsor : AddTorsor (G × G') (P × P') where
   vadd v p := (v.1 +ᵥ p.1, v.2 +ᵥ p.2)
@@ -353,7 +353,7 @@ end Pi
 
 namespace Equiv
 
-variable {G : Type _} {P : Type _} [AddGroup G] [AddTorsor G P]
+variable {G : Type*} {P : Type*} [AddGroup G] [AddTorsor G P]
 
 -- Porting note: Removed:
 -- include G
@@ -488,7 +488,7 @@ theorem pointReflection_fixed_iff_of_injective_bit0 {x y : P} (h : Injective (bi
 -- omit G
 
 -- Porting note: need this to calm down CI
-theorem injective_pointReflection_left_of_injective_bit0 {G P : Type _} [AddCommGroup G]
+theorem injective_pointReflection_left_of_injective_bit0 {G P : Type*} [AddCommGroup G]
     [AddTorsor G P] (h : Injective (bit0 : G → G)) (y : P) :
     Injective fun x : P => pointReflection x y :=
   fun x₁ x₂ (hy : pointReflection x₁ y = pointReflection x₂ y) => by
@@ -499,7 +499,7 @@ theorem injective_pointReflection_left_of_injective_bit0 {G P : Type _} [AddComm
 
 end Equiv
 
-theorem AddTorsor.subsingleton_iff (G P : Type _) [AddGroup G] [AddTorsor G P] :
+theorem AddTorsor.subsingleton_iff (G P : Type*) [AddGroup G] [AddTorsor G P] :
     Subsingleton G ↔ Subsingleton P := by
   inhabit P
   exact (Equiv.vaddConst default).subsingleton_congr

Mathlib/Algebra/Algebra/Basic.lean

@@ -127,19 +127,19 @@ def algebraMap (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra
 #align algebra_map algebraMap
 
 /-- Coercion from a commutative semiring to an algebra over this semiring. -/
-@[coe] def Algebra.cast {R A : Type _} [CommSemiring R] [Semiring A] [Algebra R A] : R → A :=
+@[coe] def Algebra.cast {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] : R → A :=
   algebraMap R A
 
 namespace algebraMap
 
-scoped instance coeHTCT (R A : Type _) [CommSemiring R] [Semiring A] [Algebra R A] :
+scoped instance coeHTCT (R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A] :
     CoeHTCT R A :=
   ⟨Algebra.cast⟩
 #align algebra_map.has_lift_t algebraMap.coeHTCT
 
 section CommSemiringSemiring
 
-variable {R A : Type _} [CommSemiring R] [Semiring A] [Algebra R A]
+variable {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
 
 @[simp, norm_cast]
 theorem coe_zero : (↑(0 : R) : A) = 0 :=
@@ -170,7 +170,7 @@ end CommSemiringSemiring
 
 section CommRingRing
 
-variable {R A : Type _} [CommRing R] [Ring A] [Algebra R A]
+variable {R A : Type*} [CommRing R] [Ring A] [Algebra R A]
 
 @[norm_cast]
 theorem coe_neg (x : R) : (↑(-x : R) : A) = -↑x :=
@@ -181,20 +181,20 @@ end CommRingRing
 
 section CommSemiringCommSemiring
 
-variable {R A : Type _} [CommSemiring R] [CommSemiring A] [Algebra R A]
+variable {R A : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A]
 
 open BigOperators
 
 -- direct to_additive fails because of some mix-up with polynomials
 @[norm_cast]
-theorem coe_prod {ι : Type _} {s : Finset ι} (a : ι → R) :
+theorem coe_prod {ι : Type*} {s : Finset ι} (a : ι → R) :
     (↑(∏ i : ι in s, a i : R) : A) = ∏ i : ι in s, (↑(a i) : A) :=
   map_prod (algebraMap R A) a s
 #align algebra_map.coe_prod algebraMap.coe_prod
 
 -- to_additive fails for some reason
 @[norm_cast]
-theorem coe_sum {ι : Type _} {s : Finset ι} (a : ι → R) :
+theorem coe_sum {ι : Type*} {s : Finset ι} (a : ι → R) :
     ↑(∑ i : ι in s, a i) = ∑ i : ι in s, (↑(a i) : A) :=
   map_sum (algebraMap R A) a s
 #align algebra_map.coe_sum algebraMap.coe_sum
@@ -205,7 +205,7 @@ end CommSemiringCommSemiring
 
 section FieldNontrivial
 
-variable {R A : Type _} [Field R] [CommSemiring A] [Nontrivial A] [Algebra R A]
+variable {R A : Type*} [Field R] [CommSemiring A] [Nontrivial A] [Algebra R A]
 
 @[norm_cast, simp]
 theorem coe_inj {a b : R} : (↑a : A) = ↑b ↔ a = b :=
@@ -221,7 +221,7 @@ end FieldNontrivial
 
 section SemifieldSemidivisionRing
 
-variable {R : Type _} (A : Type _) [Semifield R] [DivisionSemiring A] [Algebra R A]
+variable {R : Type*} (A : Type*) [Semifield R] [DivisionSemiring A] [Algebra R A]
 
 @[norm_cast]
 theorem coe_inv (r : R) : ↑r⁻¹ = ((↑r)⁻¹ : A) :=
@@ -242,7 +242,7 @@ end SemifieldSemidivisionRing
 
 section FieldDivisionRing
 
-variable (R A : Type _) [Field R] [DivisionRing A] [Algebra R A]
+variable (R A : Type*) [Field R] [DivisionRing A] [Algebra R A]
 
 -- porting note: todo: drop implicit args
 @[norm_cast]
@@ -275,7 +275,7 @@ theorem RingHom.algebraMap_toAlgebra {R S} [CommSemiring R] [CommSemiring S] (i
 
 namespace Algebra
 
-variable {R : Type u} {S : Type v} {A : Type w} {B : Type _}
+variable {R : Type u} {S : Type v} {A : Type w} {B : Type*}
 
 /-- Let `R` be a commutative semiring, let `A` be a semiring with a `Module R` structure.
 If `(r • 1) * x = x * (r • 1) = r • x` for all `r : R` and `x : A`, then `A` is an `Algebra`
@@ -319,7 +319,7 @@ variable [Semiring A] [Algebra R A] [Semiring B] [Algebra R B]
 it suffices to check the `algebraMap`s agree.
 -/
 @[ext]
-theorem algebra_ext {R : Type _} [CommSemiring R] {A : Type _} [Semiring A] (P Q : Algebra R A)
+theorem algebra_ext {R : Type*} [CommSemiring R] {A : Type*} [Semiring A] (P Q : Algebra R A)
     (h : ∀ r : R, (haveI := P; algebraMap R A r) = haveI := Q; algebraMap R A r) :
     P = Q := by
   replace h : P.toRingHom = Q.toRingHom := FunLike.ext _ _ h
@@ -396,7 +396,7 @@ protected theorem smul_mul_assoc (r : R) (x y : A) : r • x * y = r • (x * y)
 #align algebra.smul_mul_assoc Algebra.smul_mul_assoc
 
 @[simp]
-theorem _root_.smul_algebraMap {α : Type _} [Monoid α] [MulDistribMulAction α A]
+theorem _root_.smul_algebraMap {α : Type*} [Monoid α] [MulDistribMulAction α A]
     [SMulCommClass α R A] (a : α) (r : R) : a • algebraMap R A r = algebraMap R A r := by
   rw [algebraMap_eq_smul_one, smul_comm a r (1 : A), smul_one]
 #align smul_algebra_map smul_algebraMap
@@ -519,36 +519,36 @@ theorem algebraMap_ofSubsemiring_apply (S : Subsemiring R) (x : S) : algebraMap
 #align algebra.algebra_map_of_subsemiring_apply Algebra.algebraMap_ofSubsemiring_apply
 
 /-- Algebra over a subring. This builds upon `Subring.module`. -/
-instance ofSubring {R A : Type _} [CommRing R] [Ring A] [Algebra R A] (S : Subring R) :
+instance ofSubring {R A : Type*} [CommRing R] [Ring A] [Algebra R A] (S : Subring R) :
     Algebra S A where -- porting note: don't use `toSubsemiring` because of a timeout
   toRingHom := (algebraMap R A).comp S.subtype
   smul := (· • ·)
   commutes' r x := Algebra.commutes (r : R) x
   smul_def' r x := Algebra.smul_def (r : R) x
 #align algebra.of_subring Algebra.ofSubring
 
-theorem algebraMap_ofSubring {R : Type _} [CommRing R] (S : Subring R) :
+theorem algebraMap_ofSubring {R : Type*} [CommRing R] (S : Subring R) :
     (algebraMap S R : S →+* R) = Subring.subtype S :=
   rfl
 #align algebra.algebra_map_of_subring Algebra.algebraMap_ofSubring
 
-theorem coe_algebraMap_ofSubring {R : Type _} [CommRing R] (S : Subring R) :
+theorem coe_algebraMap_ofSubring {R : Type*} [CommRing R] (S : Subring R) :
     (algebraMap S R : S → R) = Subtype.val :=
   rfl
 #align algebra.coe_algebra_map_of_subring Algebra.coe_algebraMap_ofSubring
 
-theorem algebraMap_ofSubring_apply {R : Type _} [CommRing R] (S : Subring R) (x : S) :
+theorem algebraMap_ofSubring_apply {R : Type*} [CommRing R] (S : Subring R) (x : S) :
     algebraMap S R x = x :=
   rfl
 #align algebra.algebra_map_of_subring_apply Algebra.algebraMap_ofSubring_apply
 
 /-- Explicit characterization of the submonoid map in the case of an algebra.
 `S` is made explicit to help with type inference -/
-def algebraMapSubmonoid (S : Type _) [Semiring S] [Algebra R S] (M : Submonoid R) : Submonoid S :=
+def algebraMapSubmonoid (S : Type*) [Semiring S] [Algebra R S] (M : Submonoid R) : Submonoid S :=
   M.map (algebraMap R S)
 #align algebra.algebra_map_submonoid Algebra.algebraMapSubmonoid
 
-theorem mem_algebraMapSubmonoid_of_mem {S : Type _} [Semiring S] [Algebra R S] {M : Submonoid R}
+theorem mem_algebraMapSubmonoid_of_mem {S : Type*} [Semiring S] [Algebra R S] {M : Submonoid R}
     (x : M) : algebraMap R S x ∈ algebraMapSubmonoid S M :=
   Set.mem_image_of_mem (algebraMap R S) x.2
 #align algebra.mem_algebra_map_submonoid_of_mem Algebra.mem_algebraMapSubmonoid_of_mem
@@ -596,7 +596,7 @@ open scoped Algebra
 
 namespace MulOpposite
 
-variable {R A : Type _} [CommSemiring R] [Semiring A] [Algebra R A]
+variable {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
 
 instance instAlgebraMulOpposite : Algebra R Aᵐᵒᵖ where
   toRingHom := (algebraMap R A).toOpposite fun x y => Algebra.commutes _ _
@@ -671,7 +671,7 @@ end Module
 
 namespace LinearMap
 
-variable {R : Type _} {A : Type _} {B : Type _} [CommSemiring R] [Semiring A] [Semiring B]
+variable {R : Type*} {A : Type*} {B : Type*} [CommSemiring R] [Semiring A] [Semiring B]
   [Algebra R A] [Algebra R B]
 
 /-- An alternate statement of `LinearMap.map_smul` for when `algebraMap` is more convenient to
@@ -690,7 +690,7 @@ end LinearMap
 
 section Nat
 
-variable {R : Type _} [Semiring R]
+variable {R : Type*} [Semiring R]
 
 -- Lower the priority so that `Algebra.id` is picked most of the time when working with
 -- `ℕ`-algebras. This is only an issue since `Algebra.id` and `algebraNat` are not yet defeq.
@@ -710,7 +710,7 @@ end Nat
 
 namespace RingHom
 
-variable {R S : Type _}
+variable {R S : Type*}
 
 -- porting note: changed `[Ring R] [Ring S]` to `[Semiring R] [Semiring S]`
 -- otherwise, Lean failed to find a `Subsingleton (ℚ →+* S)` instance
@@ -746,7 +746,7 @@ end Rat
 
 section Int
 
-variable (R : Type _) [Ring R]
+variable (R : Type*) [Ring R]
 
 -- Lower the priority so that `Algebra.id` is picked most of the time when working with
 -- `ℤ`-algebras. This is only an issue since `Algebra.id ℤ` and `algebraInt ℤ` are not yet defeq.
@@ -774,7 +774,7 @@ end Int
 
 namespace NoZeroSMulDivisors
 
-variable {R A : Type _}
+variable {R A : Type*}
 
 open Algebra
 
@@ -841,10 +841,10 @@ end NoZeroSMulDivisors
 
 section IsScalarTower
 
-variable {R : Type _} [CommSemiring R]
-variable (A : Type _) [Semiring A] [Algebra R A]
-variable {M : Type _} [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M]
-variable {N : Type _} [AddCommMonoid N] [Module A N] [Module R N] [IsScalarTower R A N]
+variable {R : Type*} [CommSemiring R]
+variable (A : Type*) [Semiring A] [Algebra R A]
+variable {M : Type*} [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M]
+variable {N : Type*} [AddCommMonoid N] [Module A N] [Module R N] [IsScalarTower R A N]
 
 theorem algebra_compatible_smul (r : R) (m : M) : r • m = (algebraMap R A) r • m := by
   rw [← one_smul A m, ← smul_assoc, Algebra.smul_def, mul_one, one_smul]
@@ -855,12 +855,12 @@ theorem algebraMap_smul (r : R) (m : M) : (algebraMap R A) r • m = r • m :=
   (algebra_compatible_smul A r m).symm
 #align algebra_map_smul algebraMap_smul
 
-theorem intCast_smul {k V : Type _} [CommRing k] [AddCommGroup V] [Module k V] (r : ℤ) (x : V) :
+theorem intCast_smul {k V : Type*} [CommRing k] [AddCommGroup V] [Module k V] (r : ℤ) (x : V) :
     (r : k) • x = r • x :=
   algebraMap_smul k r x
 #align int_cast_smul intCast_smul
 
-theorem NoZeroSMulDivisors.trans (R A M : Type _) [CommRing R] [Ring A] [IsDomain A] [Algebra R A]
+theorem NoZeroSMulDivisors.trans (R A M : Type*) [CommRing R] [Ring A] [IsDomain A] [Algebra R A]
     [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] [NoZeroSMulDivisors R A]
     [NoZeroSMulDivisors A M] : NoZeroSMulDivisors R M := by
   refine' ⟨fun {r m} h => _⟩
@@ -925,7 +925,7 @@ are all defined in `LinearAlgebra/Basic.lean`. -/
 
 section Module
 
-variable (R : Type _) {S M N : Type _} [Semiring R] [Semiring S] [SMul R S]
+variable (R : Type*) {S M N : Type*} [Semiring R] [Semiring S] [SMul R S]
 variable [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M]
 variable [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N]
 

Mathlib/Algebra/Algebra/Bilinear.lean

@@ -25,7 +25,7 @@ namespace LinearMap
 
 section NonUnitalNonAssoc
 
-variable (R A : Type _) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A]
+variable (R A : Type*) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A]
   [SMulCommClass R A A] [IsScalarTower R A A]
 
 /-- The multiplication in a non-unital non-associative algebra is a bilinear map.
@@ -108,7 +108,7 @@ end NonUnitalNonAssoc
 
 section NonUnital
 
-variable (R A : Type _) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A]
+variable (R A : Type*) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A]
   [IsScalarTower R A A]
 
 /-- The multiplication in a non-unital algebra is a bilinear map.
@@ -153,7 +153,7 @@ end NonUnital
 
 section Semiring
 
-variable (R A : Type _) [CommSemiring R] [Semiring A] [Algebra R A]
+variable (R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A]
 
 /-- The multiplication in an algebra is an algebra homomorphism into the endomorphisms on
 the algebra.
@@ -230,7 +230,7 @@ end Semiring
 
 section Ring
 
-variable {R A : Type _} [CommSemiring R] [Ring A] [Algebra R A]
+variable {R A : Type*} [CommSemiring R] [Ring A] [Algebra R A]
 
 theorem mulLeft_injective [NoZeroDivisors A] {x : A} (hx : x ≠ 0) :
     Function.Injective (mulLeft R x) := by