diff --git a/tests/lean/mvar1.lean b/tests/lean/mvar1.lean
deleted file mode 100644
index 1d6b1747c1..0000000000
--- a/tests/lean/mvar1.lean
+++ /dev/null
@@ -1,104 +0,0 @@
-import Lean.MetavarContext
-
-open Lean
-
-def check (b : Bool) : IO Unit :=
-unless b do throw $ IO.userError "error"
-
-def f := mkConst `f []
-def g := mkConst `g []
-def a := mkConst `a []
-def b := mkConst `b []
-def c := mkConst `c []
-
-def b0 := mkBVar 0
-def b1 := mkBVar 1
-def b2 := mkBVar 2
-
-def u := mkLevelParam `u
-
-def typeE := mkSort levelOne
-def natE  := mkConst `Nat []
-def boolE := mkConst `Bool []
-def vecE  := mkConst `Vec [levelZero]
-
-instance : Coe Name FVarId where
-  coe n := { name := n }
-
-instance : Coe Name MVarId where
-  coe n := { name := n }
-
-def α := mkFVar `α
-def x := mkFVar `x
-def y := mkFVar `y
-def z := mkFVar `z
-def w := mkFVar `w
-
-def m1 := mkMVar `m1
-def m2 := mkMVar `m2
-def m3 := mkMVar `m3
-def m4 := mkMVar `m4
-def m5 := mkMVar `m5
-def m6 := mkMVar `m6
-
-def bi := BinderInfo.default
-def arrow (d b : Expr) := mkForall `_ bi d b
-def lctx1 : LocalContext := {}
-def lctx2 := lctx1.mkLocalDecl `α `α typeE
-def lctx3 := lctx2.mkLocalDecl `x `x natE
-def lctx4 := lctx3.mkLocalDecl `y `y α
-def lctx5 := lctx4.mkLocalDecl `z `z (mkAppN vecE #[x])
-def lctx6 := lctx5.mkLocalDecl `w `w (arrow natE (mkAppN m6 #[α, x, y]))
-
-def t1 := lctx5.mkLambda #[α, x, y] $ mkAppN f #[α, mkAppN g #[x, y], lctx5.mkLambda #[z] (mkApp f z)]
-#eval check (!t1.hasFVar)
-#eval toString t1
-
-def mctx1 : MetavarContext := {}
-def mctx2  := mctx1.addExprMVarDecl `m1 `m1 lctx3 #[] natE
-def mctx3  := mctx2.addExprMVarDecl `m2 `m2 lctx4 #[] α
-def mctx4  := mctx3.addExprMVarDecl `m3 `m3 lctx4 #[] natE
-def mctx5  := mctx4.addExprMVarDecl `m4 `m4 lctx1 #[] (arrow typeE (arrow natE (arrow α natE)))
-def mctx6  := mctx5.addExprMVarDecl `m5 `m5 lctx5 #[] typeE
-def mctx7  := mctx5.addExprMVarDecl `m6 `m6 lctx5 #[] (arrow typeE (arrow natE (arrow α natE)))
-def mctx8  := mctx7.assignDelayed `m4 #[α, x, y] m3
-def mctx9  := mctx8.assignExpr `m3 (mkAppN g #[x, y])
-def mctx10 := mctx9.assignExpr `m1 a
-
-def t2 := lctx5.mkLambda #[α, x, y] $ mkAppN f #[mkAppN m4 #[α, x, y], x]
-
-#eval t2
-
-#eval check (!t2.hasFVar)
-#eval toString t2
-#eval toString (mctx6.instantiateMVars t2).1
-#eval check (!(mctx9.instantiateMVars t2).1.hasMVar)
-#eval check (!(mctx9.instantiateMVars t2).1.hasFVar)
-#eval toString (mctx9.instantiateMVars t2).1
-
--- t3 is ill-formed since m3's localcontext contains ‵α`, `x` and `y`
-def t3 := lctx5.mkLambda #[α, x, y] $ mkAppN f #[m3, x]
-#eval check (mctx10.instantiateMVars t3).1.hasFVar
-#eval toString (mctx7.instantiateMVars t3).1
-
-partial def mkDiamond : Nat → Expr
-| 0     => m1
-| (n+1) => mkAppN f #[mkDiamond n, mkDiamond n]
-
-#eval toString (mctx7.instantiateMVars (mkDiamond 3)).1
-#eval toString (mctx10.instantiateMVars (mkDiamond 3)).1
-#eval toString (mctx7.instantiateMVars (mkDiamond 100)).1.getAppFn
-#eval toString (mctx10.instantiateMVars (mkDiamond 100)).1.getAppFn
-
-def mctx11 := mctx10.assignDelayed `m6 #[α, x, y] m5
-def mctx12 := mctx11.assignExpr `m5 (arrow α α)
-
-def t4 := lctx6.mkLambda #[α, x, y, w] $ mkAppN f #[mkAppN m4 #[α, x, y], x]
-
-#eval toString t4
-#eval toString (mctx9.instantiateMVars t4).1
-#eval toString (mctx12.instantiateMVars t4).1
-#eval check (mctx9.instantiateMVars t4).1.hasMVar
-#eval check (!((mctx9.instantiateMVars t4).1.hasFVar))
-#eval check (!(mctx12.instantiateMVars t4).1.hasMVar)
-#eval check (!((mctx12.instantiateMVars t4).1.hasFVar))
diff --git a/tests/lean/mvar1.lean.expected.out b/tests/lean/mvar1.lean.expected.out
deleted file mode 100644
index ef2fc3b823..0000000000
--- a/tests/lean/mvar1.lean.expected.out
+++ /dev/null
@@ -1,51 +0,0 @@
-
-"fun (α : Type) (x : Nat) (y : α) => f α (g x y) (fun (z : Vec.{0} x) => f z)"
-Lean.Expr.lam
-  `α
-  (Lean.Expr.sort
-    (Lean.Level.succ (Lean.Level.zero (Level.mkData 2221)) (Level.mkData 1676277521 (depth := 1)))
-    (Expr.mkData 1469443585 (bi := Lean.BinderInfo.default)))
-  (Lean.Expr.lam
-    `x
-    (Lean.Expr.const `Nat [] (Expr.mkData 607656011 (bi := Lean.BinderInfo.default)))
-    (Lean.Expr.lam
-      `y
-      (Lean.Expr.bvar 1 (Expr.mkData 4280418285 (looseBVarRange := 2) (bi := Lean.BinderInfo.default)))
-      (Lean.Expr.app
-        (Lean.Expr.app
-          (Lean.Expr.const `f [] (Expr.mkData 3992371127 (bi := Lean.BinderInfo.default)))
-          (Lean.Expr.app
-            (Lean.Expr.app
-              (Lean.Expr.app
-                (Lean.Expr.mvar `m4 (Expr.mkData 3167598817 (hasExprMVar := true) (bi := Lean.BinderInfo.default)))
-                (Lean.Expr.bvar 2 (Expr.mkData 4281466863 (looseBVarRange := 3) (bi := Lean.BinderInfo.default)))
-                (Expr.mkData 621598011 (looseBVarRange := 3) (approxDepth := 1) (hasExprMVar := true) (bi := Lean.BinderInfo.default)))
-              (Lean.Expr.bvar 1 (Expr.mkData 4280418285 (looseBVarRange := 2) (bi := Lean.BinderInfo.default)))
-              (Expr.mkData 1373601833 (looseBVarRange := 3) (approxDepth := 2) (hasExprMVar := true) (bi := Lean.BinderInfo.default)))
-            (Lean.Expr.bvar 0 (Expr.mkData 4279369707 (looseBVarRange := 1) (bi := Lean.BinderInfo.default)))
-            (Expr.mkData 237469531 (looseBVarRange := 3) (approxDepth := 3) (hasExprMVar := true) (bi := Lean.BinderInfo.default)))
-          (Expr.mkData 1344847761 (looseBVarRange := 3) (approxDepth := 4) (hasExprMVar := true) (bi := Lean.BinderInfo.default)))
-        (Lean.Expr.bvar 1 (Expr.mkData 4280418285 (looseBVarRange := 2) (bi := Lean.BinderInfo.default)))
-        (Expr.mkData 569884967 (looseBVarRange := 3) (approxDepth := 5) (hasExprMVar := true) (bi := Lean.BinderInfo.default)))
-      (Expr.mkData 2023949564 (looseBVarRange := 2) (approxDepth := 6) (hasExprMVar := true) (bi := Lean.BinderInfo.default)))
-    (Expr.mkData 1948877337 (looseBVarRange := 1) (approxDepth := 7) (hasExprMVar := true) (bi := Lean.BinderInfo.default)))
-  (Expr.mkData 2017358918 (approxDepth := 8) (hasExprMVar := true) (bi := Lean.BinderInfo.default))
-
-"fun (α : Type) (x : Nat) (y : α) => f (?m4 α x y) x"
-"fun (α : Type) (x : Nat) (y : α) => f (?m4 α x y) x"
-
-
-"fun (α : Type) (x : Nat) (y : α) => f (g x y) x"
-
-"fun (α : Type) (x : Nat) (y : α) => f ?m3 x"
-"f (f (f ?m1 ?m1) (f ?m1 ?m1)) (f (f ?m1 ?m1) (f ?m1 ?m1))"
-"f (f (f a a) (f a a)) (f (f a a) (f a a))"
-"f"
-"f"
-"fun (α : Type) (x : Nat) (y : α) (w : Nat -> (?m6 α x y)) => f (?m4 α x y) x"
-"fun (α : Type) (x : Nat) (y : α) (w : Nat -> (?m6 α x y)) => f (g x y) x"
-"fun (α : Type) (x : Nat) (y : α) (w : Nat -> α -> α) => f (g x y) x"
-
-
-
-
diff --git a/tests/lean/mvar2.lean b/tests/lean/mvar2.lean
deleted file mode 100644
index 0a95888b24..0000000000
--- a/tests/lean/mvar2.lean
+++ /dev/null
@@ -1,62 +0,0 @@
-import Lean.MetavarContext
-
-open Lean
-
-def check (b : Bool) : IO Unit :=
-unless b do throw $ IO.userError "error"
-
-def f := mkConst `f []
-def g := mkConst `g []
-def a := mkConst `a []
-def b := mkConst `b []
-def c := mkConst `c []
-
-def b0 := mkBVar 0
-def b1 := mkBVar 1
-def b2 := mkBVar 2
-
-def u := mkLevelParam `u
-
-def typeE := mkSort levelOne
-def natE  := mkConst `Nat []
-def boolE := mkConst `Bool []
-def vecE  := mkConst `Vec [levelZero]
-
-instance : Coe Name FVarId where
-  coe n := { name := n }
-
-instance : Coe Name MVarId where
-  coe n := { name := n }
-
-def α := mkFVar `α
-def x := mkFVar `x
-def y := mkFVar `y
-def z := mkFVar `z
-def w := mkFVar `w
-
-def m1 := mkMVar `m1
-def m2 := mkMVar `m2
-def m3 := mkMVar `m3
-
-def bi := BinderInfo.default
-def arrow (d b : Expr) := mkForall `_ bi d b
-
-def lctx1 : LocalContext := {}
-def lctx2 := lctx1.mkLocalDecl `α `α typeE
-def lctx3 := lctx2.mkLocalDecl `x `x m1
-def lctx4 := lctx3.mkLocalDecl `y `y (arrow natE (mkAppN m3 #[α, x]))
-
-def mctx1 : MetavarContext := {}
-def mctx2  := mctx1.addExprMVarDecl `m1 `m1 lctx1 #[] typeE
-def mctx3  := mctx2.addExprMVarDecl `m2 `m2 lctx3 #[] natE
-def mctx4  := mctx3.addExprMVarDecl `m3 `m3 lctx1 #[] (arrow typeE (arrow natE natE))
-def mctx5  := mctx4.assignDelayed `m3 #[α, x] m2
-def mctx6  := mctx5.assignExpr `m2 (arrow α α)
-def mctx7  := mctx6.assignExpr `m1 natE
-
-def t2 := lctx4.mkLambda #[α, x, y] $ mkAppN f #[mkAppN m3 #[α, x], x]
-
-#eval check (!t2.hasFVar)
-#eval toString t2
-#eval toString (mctx6.instantiateMVars t2).1
-#eval toString (mctx7.instantiateMVars t2).1
diff --git a/tests/lean/mvar2.lean.expected.out b/tests/lean/mvar2.lean.expected.out
deleted file mode 100644
index 8d86c66231..0000000000
--- a/tests/lean/mvar2.lean.expected.out
+++ /dev/null
@@ -1,4 +0,0 @@
-
-"fun (α : Type) (x : ?m1) (y : Nat -> (?m3 α x)) => f (?m3 α x) x"
-"fun (α : Type) (x : ?m1) (y : Nat -> α -> α) => f (α -> α) x"
-"fun (α : Type) (x : Nat) (y : Nat -> α -> α) => f (α -> α) x"
diff --git a/tests/lean/mvar3.lean b/tests/lean/mvar3.lean
deleted file mode 100644
index fb8e3427b7..0000000000
--- a/tests/lean/mvar3.lean
+++ /dev/null
@@ -1,103 +0,0 @@
-import Lean.MetavarContext
-
-open Lean
-
-def mkLambdaTest (mctx : MetavarContext) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr)
-    : Except MetavarContext.MkBinding.Exception (MetavarContext × NameGenerator × Expr) :=
-match MetavarContext.mkLambda xs e false true BinderInfo.default { lctx, mainModule := `main } { mctx := mctx, ngen := ngen, nextMacroScope := firstFrontendMacroScope + 1 } with
-| EStateM.Result.ok e s    => Except.ok (s.mctx, s.ngen, e)
-| EStateM.Result.error e s => Except.error e
-
-def check (b : Bool) : IO Unit :=
-unless b do throw $ IO.userError "error"
-
-def f := mkConst `f
-def g := mkConst `g
-def a := mkConst `a
-def b := mkConst `b
-def c := mkConst `c
-
-def b0 := mkBVar 0
-def b1 := mkBVar 1
-def b2 := mkBVar 2
-
-def u := mkLevelParam `u
-
-def typeE := mkSort levelOne
-def natE  := mkConst `Nat
-def boolE := mkConst `Bool
-def vecE  := mkConst `Vec [levelZero]
-
-instance : Coe Name FVarId where
-  coe n := { name := n }
-
-instance : Coe Name MVarId where
-  coe n := { name := n }
-
-def α := mkFVar `α
-def x := mkFVar `x
-def y := mkFVar `y
-def z := mkFVar `z
-def w := mkFVar `w
-
-def m1 := mkMVar `m1
-def m2 := mkMVar `m2
-def m3 := mkMVar `m3
-
-def bi := BinderInfo.default
-def arrow (d b : Expr) := mkForall `_ bi d b
-
-def lctx1 : LocalContext := {}
-def lctx2 := lctx1.mkLocalDecl `α `α typeE
-def lctx3 := lctx2.mkLocalDecl `x `x m1
-def lctx4 := lctx3.mkLocalDecl `y `y (arrow natE m2)
-
-def mctx1 : MetavarContext := {}
-def mctx2  := mctx1.addExprMVarDecl `m1 `m1 lctx2 #[] typeE
-def mctx3  := mctx2.addExprMVarDecl `m2 `m2 lctx3 #[] natE
-def mctx4  := mctx3.addExprMVarDecl `m3 `m3 lctx3 #[] natE
-def mctx4' := mctx3.addExprMVarDecl `m3 `m3 lctx3 #[] natE MetavarKind.syntheticOpaque
-
-def R1 :=
-match mkLambdaTest mctx4 {namePrefix := `n} lctx4 #[α, x, y] $ mkAppN f #[m3, x] with
-| Except.ok s    => s
-| Except.error e => panic! (toString e)
-def e1    := R1.2.2
-def mctx5 := R1.1
-
-def sortNames (xs : List Name) : List Name :=
-(xs.toArray.qsort Name.lt).toList
-
-instance : ToString MVarId where
-  toString m := toString m.name
-
-def sortNamePairs {α} [Inhabited α] (xs : List (MVarId × α)) : List (MVarId × α) :=
-(xs.toArray.qsort (fun a b => Name.lt a.1.name b.1.name)).toList
-
-#eval toString $ sortNames $ mctx5.decls.toList.map (·.1.name)
-#eval toString $ sortNamePairs $ mctx5.eAssignment.toList
-#eval toString e1
-#eval check (!e1.hasFVar)
-
-def R2 :=
-match mkLambdaTest mctx4' {namePrefix := `n} lctx4 #[α, x, y] $ mkAppN f #[m3, y] with
-| Except.ok s    => s
-| Except.error e => panic! (toString e)
-def e2    := R2.2.2
-def mctx6 := R2.1
-
-#eval toString $ sortNames $ mctx6.decls.toList.map (·.1.name)
-#eval toString $ sortNamePairs $ mctx6.eAssignment.toList
--- ?n.2 was delayed assigned because ?m.3 is synthetic
-#eval toString $ sortNames $ mctx6.dAssignment.toList.map (·.1.name)
-#eval toString e2
-
-#print "assigning ?m1 and ?n.1"
-def R3 :=
-let mctx := mctx6.assignExpr `m3 x;
-let mctx := mctx.assignExpr (Name.mkNum `n 1) (mkLambda `_ bi typeE natE);
--- ?n.2 is instantiated because we have the delayed assignment `?n.2 α x := ?m1`
-(mctx.instantiateMVars e2)
-def e3    := R3.1
-def mctx7 := R3.2
-#eval toString e3
diff --git a/tests/lean/mvar3.lean.expected.out b/tests/lean/mvar3.lean.expected.out
deleted file mode 100644
index 8d2bde1ffc..0000000000
--- a/tests/lean/mvar3.lean.expected.out
+++ /dev/null
@@ -1,10 +0,0 @@
-"[n.1, n.2, n.3, m1, m2, m3]"
-"[(m1, ?n α), (m2, ?n α x), (m3, ?n α x)]"
-"fun (α : Type) (x : ?n α) (y : Nat -> (?n α x)) => f (?n α x) x"
-
-"[n.1, n.2, n.3, m1, m2, m3]"
-"[(m1, ?n α), (m2, ?n α x)]"
-"[n.2]"
-"fun (α : Type) (x : ?n α) (y : Nat -> (?n α x)) => f (?n α x) y"
-assigning ?m1 and ?n
-"fun (α : Type) (x : Nat) (y : Nat -> (?n α x)) => f x y"