diff --git a/tests/lean/ppExpr.lean b/tests/lean/ppExpr.lean
index 642569acef..dcb3a8c19c 100644
--- a/tests/lean/ppExpr.lean
+++ b/tests/lean/ppExpr.lean
@@ -16,11 +16,11 @@ def test (e : Expr) : MetaM Unit := do
 
 -- pp annotations
 #eval test $
-  mkAppN (mkConst `id [levelZero]) #[
+  mkAppN (mkConst `id [levelOne]) #[
     mkConst `Nat,
-    mkMData (KVMap.empty.set `pp.explicit true) $ mkAppN (mkConst `id [levelZero]) #[
+    mkMData (KVMap.empty.set `pp.explicit true) $ mkAppN (mkConst `id [levelOne]) #[
       mkConst `Nat,
-      mkAppN (mkConst `id [levelZero]) #[
+      mkAppN (mkConst `id [levelOne]) #[
         mkConst `Nat,
         mkConst `Nat.zero
   ]]]
diff --git a/tests/lean/ppExpr.lean.expected.out b/tests/lean/ppExpr.lean.expected.out
index 7f766cd51f..cf5d43330f 100644
--- a/tests/lean/ppExpr.lean.expected.out
+++ b/tests/lean/ppExpr.lean.expected.out
@@ -1,3 +1,3 @@
 #0
 fun a => a
-id (α := Nat) ((@id Nat (id (α := Nat) Nat.zero : Nat) : Nat) : Nat)
+id (@id Nat (id Nat.zero))