Use Sort* and Type* slightly more.

SphereEversion/ToMathlib/Data/Set/Lattice.lean

@@ -9,7 +9,7 @@ theorem const_prod_iUnion {s : ι → Set α} {t : Set β} : (t ×ˢ ⋃ i, s i)
   ext; simp
 
 -- Put next to Union₂_prod_const...
-theorem const_prod_iUnion₂ {κ : ι → Sort _} {s : ∀ i, κ i → Set α} {t : Set β} :
+theorem const_prod_iUnion₂ {κ : ι → Sort*} {s : ∀ i, κ i → Set α} {t : Set β} :
     (t ×ˢ ⋃ (i) (j), s i j) = ⋃ (i) (j), t ×ˢ s i j := by simp_rw [const_prod_iUnion]
 
 -- the next 2 lemmas should be generalized from `Set α` to a `CompleteLattice`

SphereEversion/ToMathlib/Logic/Basic.lean

@@ -1,4 +1,6 @@
+import Mathlib.Tactic.TypeStar
+
 -- `by simp [forall_and]` works in Lean 4
-theorem forall₂_and_distrib {α β : Sort _} {p q : α → β → Prop} :
+theorem forall₂_and_distrib {α β : Sort*} {p q : α → β → Prop} :
     (∀ x y, p x y ∧ q x y) ↔ (∀ x y, p x y) ∧ ∀ x y, q x y :=
   (forall_congr' fun x : α ↦ @forall_and _ (p x) (q x)).trans forall_and

SphereEversion/ToMathlib/Unused/LinearAlgebra/Multilinear.lean

@@ -7,7 +7,7 @@ We no longer intend to use this file in the sphere eversion project.
 -/
 namespace Function
 
-variable {ι : Sort _} [DecidableEq ι] {α β : ι → Type*}
+variable {ι : Sort*} [DecidableEq ι] {α β : ι → Type*}
 
 /-- Special case of `function.apply_update`. Useful for `rw`/`simp`. -/
 theorem update_fst (g : ∀ i, α i × β i) (i : ι) (v : α i × β i) (j : ι) :