diff --git a/tests/lean/root.lean b/tests/lean/root.lean
index 24634b275b..7f1536bc20 100644
--- a/tests/lean/root.lean
+++ b/tests/lean/root.lean
@@ -1,22 +1,95 @@
--*- mode: compilation; default-directory: "~/projects/lean4/build/release/" -*-
-Compilation started at Mon Jun 13 13:56:14
+namespace Foo
 
-/home/leodemoura/.elan/bin/lean  /home/leodemoura/projects/lean4/build/release/root.lean
-Bla.f : Nat → Nat
-/home/leodemoura/projects/lean4/build/release/root.lean:21:14: error: protected declarations must be in a namespace
-/home/leodemoura/projects/lean4/build/release/root.lean:29:4: error: invalid declaration name `_root_`, `_root_` is a prefix used to refer to the 'root' namespace
-/home/leodemoura/projects/lean4/build/release/root.lean:31:0: error: invalid namespace '_root_', '_root_' is a reserved namespace
-/home/leodemoura/projects/lean4/build/release/root.lean:33:0: error: invalid namespace 'f._root_', '_root_' is a reserved namespace
-/home/leodemoura/projects/lean4/build/release/root.lean:35:14: error: protected declarations must be in a namespace
-/home/leodemoura/projects/lean4/build/release/root.lean:41:7: error: unknown identifier 'h'
-/home/leodemoura/projects/lean4/build/release/root.lean:43:7: error: unknown identifier 'f'
-f : Nat → Nat
-_private.root.0.prv : Nat -> Nat
-/home/leodemoura/projects/lean4/build/release/root.lean:90:48: error: unsolved goals
-x : Nat
-⊢ isEven (x + 1 + 1) = isEven x
-/home/leodemoura/projects/lean4/build/release/root.lean:95:48: error: unsolved goals
-x : Nat
-⊢ isEven (x + 1 + 1) = isEven x
+def y := 10
 
-Compilation exited abnormally with code 1 at Mon Jun 13 13:56:14
+def _root_.Bla.f (x : Nat) := x + y
+
+#check Bla.f
+
+example : Bla.f 5 = 15 := rfl
+
+def _root_.g (x : Nat) :=
+  match x with
+  | 0 => 1
+  | x+1 => 2*g x
+
+def _root_.Boo.g (x : Nat) :=
+  match x with
+  | 0 => 1
+  | x+1 => 3*g x
+
+protected def _root_.h (x : Nat) := x -- Error
+
+example : g 3 = 8 := rfl
+
+example : Boo.g 2 = 9 := rfl
+
+end Foo
+
+def _root_ (y : Nat) := y + 1 -- Error
+
+def _root_._root_ (y : Nat) := y -- Error
+
+def _root_.f._root_ (y : Nat) := y -- Error
+
+protected def _root_.h (x : Nat) := x -- Error
+
+protected def _root_.Boo.h (x : Nat) := x -- Error
+
+example : Boo.h x = x := rfl
+
+#check h -- Error
+
+#check f -- Error
+
+open Bla
+
+#check f -- Ok
+
+namespace Test
+
+mutual
+
+  def _root_.isEven (x : Nat) :=
+    match x with
+    | 0 => true
+    | x+1 => isOdd x
+
+  def _root_.isOdd (x : Nat) :=
+    match x with
+    | 0 => false
+    | x+1 => isEven x
+
+end
+
+private def _root_.prv (x : Nat) := x + x + x
+
+example : prv 5 = 15 := rfl
+
+end Test
+
+example : isEven 0  = true := by simp! [isOdd, isEven]
+example : isOdd 1   = true := by simp! [isOdd, isEven]
+example : isEven 2  = true := by simp! [isOdd, isEven]
+
+example : prv 5 = 15 := rfl
+
+set_option pp.raw true in
+#check prv
+
+namespace Ex
+
+@[scoped simp] theorem _root_.isEven_of_isOdd (x : Nat) : isEven (x+1) = isOdd x := by simp [isEven]
+
+@[scoped simp] theorem _root_.isOdd_of_isEven (x : Nat) : isOdd (x+1) = isEven x := by simp [isOdd]
+
+example : isEven (x+1+1) = isEven x := by simp -- Ok
+
+end Ex
+
+example : isEven (x+1+1) = isEven x := by simp; done -- Error
+
+open Ex in
+example : isEven (x+1+1) = isEven x := by simp -- Ok
+
+example : isEven (x+1+1) = isEven x := by simp; done -- Error
diff --git a/tests/lean/root.lean.expected.out b/tests/lean/root.lean.expected.out
index 03687c7368..9321a8b14d 100644
--- a/tests/lean/root.lean.expected.out
+++ b/tests/lean/root.lean.expected.out
@@ -1,11 +1,16 @@
-root.lean:1:0: error: expected command
-root.lean:6:80: error: expected 'abbrev', 'axiom', 'builtin_initialize', 'class', 'constant', 'def', 'example', 'inductive', 'initialize', 'instance', 'structure' or 'theorem'
-root.lean:7:0: error: expected identifier
-root.lean:7:125: error: expected ':'
-root.lean:8:0: error: expected identifier
-root.lean:8:90: error: missing end of character literal
-root.lean:9:0: error: expected identifier
-root.lean:9:90: error: missing end of character literal
-root.lean:10:0: error: expected identifier
-root.lean:10:80: error: expected 'abbrev', 'axiom', 'builtin_initialize', 'class', 'constant', 'def', 'example', 'inductive', 'initialize', 'instance', 'structure' or 'theorem'
-root.lean:11:0: error: expected identifier
+Bla.f : Nat → Nat
+root.lean:21:14-21:22: error: protected declarations must be in a namespace
+root.lean:29:4-29:10: error: invalid declaration name `_root_`, `_root_` is a prefix used to refer to the 'root' namespace
+root.lean:31:0-31:32: error: invalid namespace '_root_', '_root_' is a reserved namespace
+root.lean:33:0-33:34: error: invalid namespace 'f._root_', '_root_' is a reserved namespace
+root.lean:35:14-35:22: error: protected declarations must be in a namespace
+root.lean:41:7-41:8: error: unknown identifier 'h'
+root.lean:43:7-43:8: error: unknown identifier 'f'
+f : Nat → Nat
+_private.root.0.prv : Nat -> Nat
+root.lean:90:48-90:52: error: unsolved goals
+x : Nat
+⊢ isEven (x + 1 + 1) = isEven x
+root.lean:95:48-95:52: error: unsolved goals
+x : Nat
+⊢ isEven (x + 1 + 1) = isEven x