diff --git a/tests/lean/fold.lean.expected.out b/tests/lean/fold.lean.expected.out
index be434df08..02bd2af80 100644
--- a/tests/lean/fold.lean.expected.out
+++ b/tests/lean/fold.lean.expected.out
@@ -1,8 +1,8 @@
-(a, false, b, true, c) : prod num (prod Prop (prod num (prod Prop num)))
+(a, false, b, true, c) : num × (Prop × (num × (Prop × num)))
 prod.mk a (prod.mk false (prod.mk b (prod.mk true c))) : prod num (prod Prop (prod num (prod Prop num)))
-(a, false, b, true, c) : prod (prod (prod (prod num Prop) num) Prop) num
+(a, false, b, true, c) : num × Prop × num × Prop × num
 prod.mk (prod.mk (prod.mk (prod.mk c true) b) false) a : prod (prod (prod (prod num Prop) num) Prop) num
-(a, false, b, true, c) : prod (prod (prod (prod num Prop) num) Prop) num
+(a, false, b, true, c) : num × Prop × num × Prop × num
 prod.mk (prod.mk (prod.mk (prod.mk a false) b) true) c : prod (prod (prod (prod num Prop) num) Prop) num
-(a, false, b, true, c) : prod num (prod Prop (prod num (prod Prop num)))
+(a, false, b, true, c) : num × (Prop × (num × (Prop × num)))
 prod.mk c (prod.mk true (prod.mk b (prod.mk false a))) : prod num (prod Prop (prod num (prod Prop num)))
diff --git a/tests/lean/nonexhaustive.lean.expected.out b/tests/lean/nonexhaustive.lean.expected.out
index 336f8a50c..4d32e00b1 100644
--- a/tests/lean/nonexhaustive.lean.expected.out
+++ b/tests/lean/nonexhaustive.lean.expected.out
@@ -1,3 +1,4 @@
+nonexhaustive.lean:2:0: warning: imported file uses 'sorry'
 nonexhaustive.lean:6:11: error: invalid non-exhaustive set of recursive equations, left-hand-side(s) after elaboration:
   @foo 0 (@nil A)
 
diff --git a/tests/lean/run/fun.lean b/tests/lean/run/fun.lean
index a602b6cd0..626a928f3 100644
--- a/tests/lean/run/fun.lean
+++ b/tests/lean/run/fun.lean
@@ -8,7 +8,6 @@ constant g : num → num
 check f ∘ g ∘ g
 
 check typeof id : num → num
-check num → num ⟨is_typeof⟩ id
 
 constant h : num → bool → num
 
diff --git a/tests/lean/unzip_error.lean.expected.out b/tests/lean/unzip_error.lean.expected.out
index a5d708bb4..d33d12844 100644
--- a/tests/lean/unzip_error.lean.expected.out
+++ b/tests/lean/unzip_error.lean.expected.out
@@ -1,2 +1,3 @@
+unzip_error.lean:2:0: warning: imported file uses 'sorry'
 unzip_error.lean:9:2: error: invalid recursive equation, left-hand-side contains meta-variable (possible solution: provide implicit parameters occurring in left-hand-side explicitly)
   match (@mk (vector A ?M_1) (vector B ?M_1) va vb)