diff --git a/src/Lean/Elab/DeclUtil.lean b/src/Lean/Elab/DeclUtil.lean
index b4e6624e72..3d52b625ed 100644
--- a/src/Lean/Elab/DeclUtil.lean
+++ b/src/Lean/Elab/DeclUtil.lean
@@ -75,9 +75,11 @@ def sortDeclLevelParams (scopeParams : List Name) (allUserParams : List Name) (u
   match allUserParams.find? fun u => !usedParams.contains u && !scopeParams.elem u with
   | some u => throw s!"unused universe parameter '{u}'"
   | none   =>
+    -- Recall that `allUserParams` (like `scopeParams`) are in reverse order. That is, the last declared universe is the first element of the list.
+    -- The following `foldl` will reverse the elements and produce a list of universe levels using the user given order.
     let result := allUserParams.foldl (fun result levelName => if usedParams.elem levelName then levelName :: result else result) []
     let remaining := usedParams.filter (fun levelParam => !allUserParams.elem levelParam)
     let remaining := remaining.qsort Name.lt
-    pure $ result ++ remaining.toList
+    return result ++ remaining.toList
 
 end Lean.Elab
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 4bbdb2757e..3122d1e062 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -737,7 +737,8 @@ def mkExplicitBinder (ident : Syntax) (type : Syntax) : Syntax :=
 def levelMVarToParam (e : Expr) (except : LMVarId → Bool := fun _ => false) : TermElabM Expr := do
   let levelNames ← getLevelNames
   let r := (← getMCtx).levelMVarToParam (fun n => levelNames.elem n) except e `u 1
-  setLevelNames (levelNames ++ r.newParamNames.toList)
+  -- Recall that the most recent universe is the first element of the field `levelNames`.
+  setLevelNames (r.newParamNames.reverse.toList ++ levelNames)
   setMCtx r.mctx
   return r.expr
 
diff --git a/tests/lean/run/3965.lean b/tests/lean/run/3965.lean
index 63ad457978..d8ae0101f1 100644
--- a/tests/lean/run/3965.lean
+++ b/tests/lean/run/3965.lean
@@ -198,7 +198,7 @@ theorem principal_nfp_blsub₂' (op : Ordinal → Ordinal → Ordinal) (o : Ordi
   · refine ⟨n+1, ?_⟩
     rw [Function.iterate_succ']
     -- universe 0 also works here
-    exact lt_blsub₂.{0} (@fun a _ b _ => op a b) (lt_of_lt_of_le hm h) hn
+    exact lt_blsub₂.{_, _, 0} (@fun a _ b _ => op a b) (lt_of_lt_of_le hm h) hn
   · sorry
 
 
diff --git a/tests/lean/run/4171.lean b/tests/lean/run/4171.lean
index 4dec00f314..70f4b9998d 100644
--- a/tests/lean/run/4171.lean
+++ b/tests/lean/run/4171.lean
@@ -701,7 +701,7 @@ example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
   mul := { hom := M.X.mul }
   mul_one := by
     ext
-    simp [foo.{v₁ + 1}] -- specifying the universe level explicitly works!
+    simp [foo.{_, v₁ + 1}] -- specifying the universe level explicitly works!
 
 theorem foo' {V} [Quiver V] {X Y x} :
     @Quiver.Hom.unop V _ X Y no_index (Opposite.op (unop := x)) = x := rfl
diff --git a/tests/lean/run/univParamIssue.lean b/tests/lean/run/univParamIssue.lean
new file mode 100644
index 0000000000..1f949e6d29
--- /dev/null
+++ b/tests/lean/run/univParamIssue.lean
@@ -0,0 +1,39 @@
+theorem f1 (a : α) (f : α → β) : f a = f a := by
+  rfl
+
+/--
+info: theorem f1.{u_1, u_2} : ∀ {α : Sort u_1} {β : Sort u_2} (a : α) (f : α → β), f a = f a :=
+fun {α} {β} a f => Eq.refl (f a)
+-/
+#guard_msgs in
+#print f1
+
+theorem f2 {α : Sort u} {β : Sort v} (a : α) (f : α → β) : f a = f a := by
+  rfl
+
+/--
+info: theorem f2.{u, v} : ∀ {α : Sort u} {β : Sort v} (a : α) (f : α → β), f a = f a :=
+fun {α} {β} a f => Eq.refl (f a)
+-/
+#guard_msgs in
+#print f2
+
+theorem f3.{u,v} {α : Sort u} {β : Sort v} (a : α) (f : α → β) : f a = f a := by
+  rfl
+
+/--
+info: theorem f3.{u, v} : ∀ {α : Sort u} {β : Sort v} (a : α) (f : α → β), f a = f a :=
+fun {α} {β} a f => Eq.refl (f a)
+-/
+#guard_msgs in
+#print f3
+
+def g (a : α) (f : α → β) : f a = f a := by
+  rfl
+
+/--
+info: def g.{u_1, u_2} : ∀ {α : Sort u_1} {β : Sort u_2} (a : α) (f : α → β), f a = f a :=
+fun {α} {β} a f => Eq.refl (f a)
+-/
+#guard_msgs in
+#print g