diff --git a/library/data/rbtree/default.lean b/library/data/rbtree/default.lean
new file mode 100644
index 0000000000..bcc7359af8
--- /dev/null
+++ b/library/data/rbtree/default.lean
@@ -0,0 +1,6 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import data.rbtree.lemmas
diff --git a/library/init/data/rbtree/lemmas.lean b/library/data/rbtree/lemmas.lean
similarity index 99%
rename from library/init/data/rbtree/lemmas.lean
rename to library/data/rbtree/lemmas.lean
index 69d5af986c..a67303dec7 100644
--- a/library/init/data/rbtree/lemmas.lean
+++ b/library/data/rbtree/lemmas.lean
@@ -1,11 +1,8 @@
 /-
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Mario Carneiro
+Authors: Leonardo de Moura
 -/
-prelude
-import init.data.rbtree.basic init.meta init.data.nat
-
 universes u v
 
 /- TODO(Leo): remove after we cleanup stdlib simp lemmas -/
diff --git a/library/init/data/rbtree/basic.lean b/library/init/data/rbtree/basic.lean
index 457e430193..ca3616b183 100644
--- a/library/init/data/rbtree/basic.lean
+++ b/library/init/data/rbtree/basic.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Mario Carneiro
+Authors: Leonardo de Moura
 -/
 prelude
 import init.data.ordering
diff --git a/library/init/data/rbtree/default.lean b/library/init/data/rbtree/default.lean
index c09428e0a8..28812c78c3 100644
--- a/library/init/data/rbtree/default.lean
+++ b/library/init/data/rbtree/default.lean
@@ -1,10 +1,10 @@
 /-
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Mario Carneiro
+Authors: Leonardo de Moura
 -/
 prelude
-import init.data.rbtree.basic init.data.rbtree.lemmas
+import init.data.rbtree.basic
 
 meta def rbtree.default_lt : tactic unit :=
 `[apply has_lt.lt]