diff --git a/tests/lean/1682.lean.expected.out b/tests/lean/1682.lean.expected.out
index cd49d31eeb7a..050d08bc5116 100644
--- a/tests/lean/1682.lean.expected.out
+++ b/tests/lean/1682.lean.expected.out
@@ -1,21 +1,21 @@
 1682.lean:1:25-2:17: error: unsolved goals
 case a
-p : Sort ?u
+p : Sort u_1
 q r : Prop
 ⊢ p → q
 
 case b
-p : Sort ?u
+p : Sort u_1
 q r : Prop
 ⊢ r
 1682.lean:4:25-5:26: error: unsolved goals
 case a
-p : Sort ?u
+p : Sort u_1
 q r : Prop
 h : p
 ⊢ q
 
 case b
-p : Sort ?u
+p : Sort u_1
 q r : Prop
 ⊢ r
diff --git a/tests/lean/813.lean.expected.out b/tests/lean/813.lean.expected.out
index 3ce42e0faa3d..7a1bb87901c4 100644
--- a/tests/lean/813.lean.expected.out
+++ b/tests/lean/813.lean.expected.out
@@ -1,12 +1,12 @@
 p : Nat → Prop
 h : p 1
 ⊢ p 1
-α : Sort ?u
+α : Sort u_1
 a : α
 p : α → Prop
 h : p a
 ⊢ p a
-α : Sort ?u
+α : Sort u_1
 a : α
 f : α → α
 p : α → Prop
diff --git a/tests/lean/autoPPExplicit.lean.expected.out b/tests/lean/autoPPExplicit.lean.expected.out
index 445a458daa16..680b9c24f7b1 100644
--- a/tests/lean/autoPPExplicit.lean.expected.out
+++ b/tests/lean/autoPPExplicit.lean.expected.out
@@ -5,4 +5,4 @@ argument
 has type
   Prop : Type
 but is expected to have type
-  α : Sort ?u
+  α : Sort u_1
diff --git a/tests/lean/interactive/plainGoal.lean.expected.out b/tests/lean/interactive/plainGoal.lean.expected.out
index 91a2fdd633bb..08286c755cc4 100644
--- a/tests/lean/interactive/plainGoal.lean.expected.out
+++ b/tests/lean/interactive/plainGoal.lean.expected.out
@@ -82,9 +82,9 @@
 {"textDocument": {"uri": "file:///plainGoal.lean"},
  "position": {"line": 55, "character": 3}}
 {"rendered":
- "```lean\nα : Sort ?u\np : α → Prop\na b : α\ninst✝ : DecidablePred p\nh : ∀ {p : α → Prop} [inst : DecidablePred p], p a → p b\n⊢ p a\n```",
+ "```lean\nα : Sort u_1\np : α → Prop\na b : α\ninst✝ : DecidablePred p\nh : ∀ {p : α → Prop} [inst : DecidablePred p], p a → p b\n⊢ p a\n```",
  "goals":
- ["α : Sort ?u\np : α → Prop\na b : α\ninst✝ : DecidablePred p\nh : ∀ {p : α → Prop} [inst : DecidablePred p], p a → p b\n⊢ p a"]}
+ ["α : Sort u_1\np : α → Prop\na b : α\ninst✝ : DecidablePred p\nh : ∀ {p : α → Prop} [inst : DecidablePred p], p a → p b\n⊢ p a"]}
 {"textDocument": {"uri": "file:///plainGoal.lean"},
  "position": {"line": 61, "character": 3}}
 {"rendered": "```lean\ncase left\n⊢ True\n```", "goals": ["case left\n⊢ True"]}
@@ -110,15 +110,15 @@
 {"textDocument": {"uri": "file:///plainGoal.lean"},
  "position": {"line": 82, "character": 53}}
 {"rendered":
- "```lean\ncase nil\nα : Type ?u\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)\n```",
+ "```lean\ncase nil\nα : Type u_1\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)\n```",
  "goals":
- ["case nil\nα : Type ?u\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)"]}
+ ["case nil\nα : Type u_1\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)"]}
 {"textDocument": {"uri": "file:///plainGoal.lean"},
  "position": {"line": 82, "character": 54}}
 {"rendered":
- "```lean\ncase nil\nα : Type ?u\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)\n```",
+ "```lean\ncase nil\nα : Type u_1\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)\n```",
  "goals":
- ["case nil\nα : Type ?u\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)"]}
+ ["case nil\nα : Type u_1\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)"]}
 {"textDocument": {"uri": "file:///plainGoal.lean"},
  "position": {"line": 86, "character": 38}}
 {"rendered": "no goals", "goals": []}
diff --git a/tests/lean/ppProofs.lean.expected.out b/tests/lean/ppProofs.lean.expected.out
index 76139fc7d69a..0aad812ed901 100644
--- a/tests/lean/ppProofs.lean.expected.out
+++ b/tests/lean/ppProofs.lean.expected.out
@@ -13,7 +13,7 @@ a : α
 h : α = β
 ⊢ ⋯ ▸ a = b
 ppProofs.lean:10:50-10:98: error: unsolved goals
-α β : Sort ?u
+α β : Sort u_1
 b : β
 a : α
 h : α = β
diff --git a/tests/lean/run/1575.lean b/tests/lean/run/1575.lean
index 47e677127e99..561edb90ce3a 100644
--- a/tests/lean/run/1575.lean
+++ b/tests/lean/run/1575.lean
@@ -1,2 +1,6 @@
-example [Subsingleton α] (p : α → Prop) : Subsingleton (Subtype p) :=
-  ⟨fun ⟨x, _⟩ ⟨y, _⟩ => Subsingleton.elim x y ▸ sorry⟩
+example [Subsingleton α] (p : α → Prop) : Subsingleton (Subtype p) := by
+  constructor
+  intro ⟨x, _⟩ ⟨y, _⟩
+  have := Subsingleton.elim x y
+  subst this
+  rfl
diff --git a/tests/lean/run/multiTargetCasesInductionIssue.lean b/tests/lean/run/multiTargetCasesInductionIssue.lean
index 07e73d21e896..211ccc709c34 100644
--- a/tests/lean/run/multiTargetCasesInductionIssue.lean
+++ b/tests/lean/run/multiTargetCasesInductionIssue.lean
@@ -24,7 +24,7 @@ def Vec.casesOn
   | ⟨as, h⟩ => go n as h
 
 /--
-info: α : Type _
+info: α : Type u_1
 n✝ : Nat
 a✝ : α
 as✝ : Vec α n✝
@@ -43,7 +43,7 @@ example (n : Nat) (a : α) (as : Vec α n) : Vec.cons a (Vec.cons a as) = Vec.co
     constructor
 
 /--
-info: α : Type _
+info: α : Type u_1
 n✝ : Nat
 a✝ : α
 as✝ : Vec α n✝
@@ -62,7 +62,7 @@ example (n : Nat) (a : α) (as : Vec α n) : Vec.cons a (Vec.cons a as) = Vec.co
     constructor
 
 /--
-info: α : Type _
+info: α : Type u_1
 n : Nat
 a : α
 as : Vec α n
diff --git a/tests/lean/rwEqThms.lean.expected.out b/tests/lean/rwEqThms.lean.expected.out
index 166374b659ff..cd30d2e7adad 100644
--- a/tests/lean/rwEqThms.lean.expected.out
+++ b/tests/lean/rwEqThms.lean.expected.out
@@ -1,41 +1,41 @@
-α : Type ?u
+α : Type u_1
 a : α
 as bs : List α
 h : bs = a :: as
 ⊢ (?head :: as).length = bs.length
 
 case head
-α : Type ?u
+α : Type u_1
 a : α
 as bs : List α
 h : bs = a :: as
 ⊢ α
-α : Type ?u
+α : Type u_1
 b a : α
 as bs : List α
 h : as = bs
 ⊢ as.length + 1 + 1 = bs.length + 2
-α : Type ?u
+α : Type u_1
 b a : α
 as bs : List α
 h : as = bs
 ⊢ as.length + 1 + 1 = (b :: bs).length + 1
-α : Type ?u
+α : Type u_1
 b a : α
 as bs : List α
 h : as = bs
 ⊢ as.length + 1 + 1 = bs.length + 1 + 1
-α : Type ?u
+α : Type u_1
 b a : α
 as bs : List α
 h : as = bs
 ⊢ id (a :: b :: as).length = (b :: bs).length + 1
-α : Type ?u
+α : Type u_1
 b a : α
 as bs : List α
 h : as = bs
 ⊢ (a :: b :: as).length = (b :: bs).length + 1
-α : Type ?u
+α : Type u_1
 b a : α
 as bs : List α
 h : as = bs