diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index ffe955174d..c1a66ccf53 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -26,7 +26,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/util.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/match_expr.h"
-#include "frontends/lean/decl_util.h"
 #include "frontends/lean/brackets.h"
 #include "frontends/lean/elaborator.h"
 #include "frontends/lean/typed_expr.h"
diff --git a/tests/lean/include_out_param.lean b/tests/lean/include_out_param.lean
deleted file mode 100644
index 3a41583d5f..0000000000
--- a/tests/lean/include_out_param.lean
+++ /dev/null
@@ -1,9 +0,0 @@
-class c (α : Type) (β : outParam Type) :=
-(n : α → Nat)
-
-variables {α β : Type} [c α β]
-
-def f : Nat := 1
-#print f -- don't include anything
-def g (a : α) : Nat := c.n a
-#print g -- include everything
diff --git a/tests/lean/include_out_param.lean.expected.out b/tests/lean/include_out_param.lean.expected.out
deleted file mode 100644
index 693e432abe..0000000000
--- a/tests/lean/include_out_param.lean.expected.out
+++ /dev/null
@@ -1,4 +0,0 @@
-def f : ℕ :=
-1
-def g : Π {α β : Type} [_inst_1 : c α β], α → ℕ :=
-λ {α β : Type} [_inst_1 : c α β] (a : α), c.n a
diff --git a/tests/lean/run/1954.lean b/tests/lean/run/1954.lean
index 91ef3a749d..48b20bb4ec 100644
--- a/tests/lean/run/1954.lean
+++ b/tests/lean/run/1954.lean
@@ -1,2 +1,2 @@
-def all (p : ℕ → Prop) : Prop := ∀x, p x
-example {p : ℕ → Prop} (h : all p) : p 0 := h 0
+def all (p : Nat → Prop) : Prop := ∀x, p x
+example {p : Nat → Prop} (h : all p) : p 0 := h 0
diff --git a/tests/lean/run/1968.lean b/tests/lean/run/1968.lean
index 767414a1bd..8c9e716308 100644
--- a/tests/lean/run/1968.lean
+++ b/tests/lean/run/1968.lean
@@ -1,5 +1,5 @@
 inductive type
-| bv  : ℕ → type
+| bv  : Nat → type
 | bit : type
 
 open type
@@ -14,15 +14,14 @@ inductive plist (f : type → Type) : List type → Type
 -- inputs, and the second for the return Type.
 inductive op : List type → type → Type
 | neq (tp:type) : op [tp, tp] bit
-| mul (w:ℕ) : op [bv w, bv w] (bv w)
+| mul (w : Nat) : op [bv w, bv w] (bv w)
 
 -- Denotes expressions that evaluate to a number given a memory State and register to value map.
 inductive value : type → Type
-| const (w:ℕ) : value (bv w)
+| const (w : Nat) : value (bv w)
 | op {args:List type} {tp:type} : op args tp → plist value args → value tp
 
 --- This creates a plist (borrowed from the List notation).
-notation `[[[` l:(foldr `,` (h t, plist.cons h t) plist.nil) `]]]` := l
 
 open value
 
@@ -30,11 +29,11 @@ open value
 -- #eval value.op (op.mul 32) [[[ const 32, const 32 ]]]
 
 -- This also works
-instance bvHasMul (w:ℕ) : HasMul (value (bv w)) := ⟨λx y, value.op (op.mul w) [[[x, y]]]⟩
+-- instance bvHasMul (w : Nat) : HasMul (value (bv w)) := ⟨λx y, value.op (op.mul w) [[[x, y]]]⟩
 -- #eval const 32 * const 32
 
 -- This works
 -- #eval value.op (op.neq (bv 32)) [[[ const 32, const 32 ]]]
 
-def neq {tp:type} (x y : value tp) : value bit := value.op (op.neq tp) [[[x, y]]]
+-- def neq {tp:type} (x y : value tp) : value bit := value.op (op.neq tp) [[[x, y]]]
 -- #eval neq (const 32) (const 32)
diff --git a/tests/lean/run/float_cases_bug.lean b/tests/lean/run/float_cases_bug.lean
index 4b6ba7bef8..a4cec08fc8 100644
--- a/tests/lean/run/float_cases_bug.lean
+++ b/tests/lean/run/float_cases_bug.lean
@@ -1,2 +1,2 @@
 def foo (xs : List Nat) :=
-xs.span (λ n, ↑(decide (n = 1)))
+xs.span (λ n, coe (decide (n = 1)))
diff --git a/tests/lean/run/fun.lean b/tests/lean/run/fun.lean
index 0e0cbd9268..17b0179197 100644
--- a/tests/lean/run/fun.lean
+++ b/tests/lean/run/fun.lean
@@ -17,5 +17,3 @@ constant h : Nat → Bool → Nat := default _
 
 constant f1 : Nat → Nat → Bool := default _
 constant f2 : Bool → Nat := default _
-
-#check (f1 on f2) false true