diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt
index aace07a93..b742b6b58 100644
--- a/src/frontends/lean/CMakeLists.txt
+++ b/src/frontends/lean/CMakeLists.txt
@@ -5,10 +5,10 @@ server.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp
 inductive_cmd.cpp elaborator.cpp dependencies.cpp parser_bindings.cpp
 begin_end_ext.cpp class.cpp pp_options.cpp tactic_hint.cpp pp.cpp
 theorem_queue.cpp structure_cmd.cpp info_manager.cpp
-info_annotation.cpp choice_iterator.cpp find_cmd.cpp
-placeholder_elaborator.cpp coercion_elaborator.cpp info_tactic.cpp
-proof_qed_elaborator.cpp init_module.cpp elaborator_context.cpp
-calc_proof_elaborator.cpp type_util.cpp elaborator_exception.cpp)
+info_annotation.cpp find_cmd.cpp placeholder_elaborator.cpp
+coercion_elaborator.cpp info_tactic.cpp proof_qed_elaborator.cpp
+init_module.cpp elaborator_context.cpp calc_proof_elaborator.cpp
+type_util.cpp elaborator_exception.cpp)
 
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})
diff --git a/src/frontends/lean/coercion_elaborator.cpp b/src/frontends/lean/coercion_elaborator.cpp
index dd164171f..2810e0fae 100644
--- a/src/frontends/lean/coercion_elaborator.cpp
+++ b/src/frontends/lean/coercion_elaborator.cpp
@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/constraint.h"
 #include "library/coercion.h"
 #include "library/unifier.h"
-#include "frontends/lean/choice_iterator.h"
+#include "library/choice_iterator.h"
 #include "frontends/lean/coercion_elaborator.h"
 
 namespace lean {
diff --git a/src/frontends/lean/coercion_elaborator.h b/src/frontends/lean/coercion_elaborator.h
index 1b20798fa..a3f0d0486 100644
--- a/src/frontends/lean/coercion_elaborator.h
+++ b/src/frontends/lean/coercion_elaborator.h
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "kernel/expr.h"
 #include "kernel/type_checker.h"
-#include "frontends/lean/choice_iterator.h"
+#include "library/choice_iterator.h"
 
 namespace lean {
 /** \brief Abstract class for hiding details of the info_manager from the coercion_elaborator */
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 0c8e2c3b7..1d4023a64 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -33,6 +33,7 @@ Author: Leonardo de Moura
 #include "library/typed_expr.h"
 #include "library/local_context.h"
 #include "library/util.h"
+#include "library/choice_iterator.h"
 #include "library/tactic/expr_to_tactic.h"
 #include "library/error_handling/error_handling.h"
 #include "library/definitional/equations.h"
@@ -41,7 +42,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/tactic_hint.h"
 #include "frontends/lean/info_manager.h"
 #include "frontends/lean/info_annotation.h"
-#include "frontends/lean/choice_iterator.h"
 #include "frontends/lean/elaborator.h"
 #include "frontends/lean/placeholder_elaborator.h"
 #include "frontends/lean/proof_qed_elaborator.h"
diff --git a/src/frontends/lean/placeholder_elaborator.cpp b/src/frontends/lean/placeholder_elaborator.cpp
index 51ebd47d4..f70978bed 100644
--- a/src/frontends/lean/placeholder_elaborator.cpp
+++ b/src/frontends/lean/placeholder_elaborator.cpp
@@ -17,8 +17,8 @@ Author: Leonardo de Moura
 #include "library/error_handling/error_handling.h"
 #include "library/class.h"
 #include "library/local_context.h"
+#include "library/choice_iterator.h"
 #include "frontends/lean/util.h"
-#include "frontends/lean/choice_iterator.h"
 #include "frontends/lean/elaborator_exception.h"
 #include "frontends/lean/pp_options.h"
 
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 77c4aaace..db4e9535a 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -11,6 +11,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   typed_expr.cpp let.cpp type_util.cpp protected.cpp
   metavar_closure.cpp reducible.cpp init_module.cpp
   generic_exception.cpp fingerprint.cpp flycheck.cpp hott_kernel.cpp
-  local_context.cpp)
+  local_context.cpp choice_iterator.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})
diff --git a/src/frontends/lean/choice_iterator.cpp b/src/library/choice_iterator.cpp
similarity index 95%
rename from src/frontends/lean/choice_iterator.cpp
rename to src/library/choice_iterator.cpp
index 1872216b6..ec9558310 100644
--- a/src/frontends/lean/choice_iterator.cpp
+++ b/src/library/choice_iterator.cpp
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "frontends/lean/choice_iterator.h"
+#include "library/choice_iterator.h"
 
 namespace lean {
 lazy_list<constraints> choose(std::shared_ptr<choice_iterator> c, bool ignore_failure) {
diff --git a/src/frontends/lean/choice_iterator.h b/src/library/choice_iterator.h
similarity index 100%
rename from src/frontends/lean/choice_iterator.h
rename to src/library/choice_iterator.h