diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt
index d5d6c8045b..f4b24c0287 100644
--- a/src/frontends/lean/CMakeLists.txt
+++ b/src/frontends/lean/CMakeLists.txt
@@ -7,6 +7,5 @@ pp.cpp structure_cmd.cpp structure_instance.cpp
 init_module.cpp type_util.cpp decl_attributes.cpp
 prenum.cpp print_cmd.cpp elaborator.cpp
 match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp
-brackets.cpp tactic_notation.cpp info_manager.cpp json.cpp tactic_evaluator.cpp
-module_parser.cpp
+brackets.cpp tactic_notation.cpp info_manager.cpp json.cpp module_parser.cpp
 equations_validator.cpp parser_state.cpp interactive.cpp completion.cpp)
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index afd7f306a2..e6889065e8 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -48,6 +48,7 @@ Author: Leonardo de Moura
 #include "library/tactic/unfold_tactic.h"
 #include "library/tactic/tactic_state.h"
 #include "library/tactic/elaborate.h"
+#include "library/tactic/tactic_evaluator.h"
 #include "library/equations_compiler/compiler.h"
 #include "library/equations_compiler/util.h"
 #include "library/inductive_compiler/ginductive.h"
@@ -55,7 +56,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/brackets.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/prenum.h"
-#include "frontends/lean/tactic_evaluator.h"
 #include "frontends/lean/structure_cmd.h"
 #include "frontends/lean/structure_instance.h"
 #include "frontends/lean/equations_validator.h"
diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp
index e6e359857d..71b43d6b7d 100644
--- a/src/frontends/lean/tactic_notation.cpp
+++ b/src/frontends/lean/tactic_notation.cpp
@@ -20,11 +20,11 @@ Author: Leonardo de Moura
 #include "library/vm/vm_expr.h"
 #include "library/vm/vm_parser.h"
 #include "library/tactic/elaborate.h"
+#include "library/tactic/tactic_evaluator.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/prenum.h"
 #include "frontends/lean/tactic_notation.h"
-#include "frontends/lean/tactic_evaluator.h"
 #include "frontends/lean/elaborator.h"
 #include "frontends/lean/pp.h"
 #include "frontends/lean/builtin_exprs.h"
diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt
index cea150df79..da3942a236 100644
--- a/src/library/tactic/CMakeLists.txt
+++ b/src/library/tactic/CMakeLists.txt
@@ -9,4 +9,4 @@ add_library(tactic OBJECT occurrences.cpp kabstract.cpp tactic_state.cpp
   simp_result.cpp user_attribute.cpp eval.cpp
   simp_lemmas.cpp eqn_lemmas.cpp dsimplify.cpp simplify.cpp
   vm_monitor.cpp destruct_tactic.cpp norm_num_tactic.cpp
-  elaborator_exception.cpp algebraic_normalizer.cpp)
+  elaborator_exception.cpp algebraic_normalizer.cpp tactic_evaluator.cpp)
diff --git a/src/frontends/lean/tactic_evaluator.cpp b/src/library/tactic/tactic_evaluator.cpp
similarity index 96%
rename from src/frontends/lean/tactic_evaluator.cpp
rename to src/library/tactic/tactic_evaluator.cpp
index 878e287949..961ccb0c7c 100644
--- a/src/frontends/lean/tactic_evaluator.cpp
+++ b/src/library/tactic/tactic_evaluator.cpp
@@ -14,8 +14,7 @@ Author: Leonardo de Moura
 #include "library/compiler/vm_compiler.h"
 #include "library/tactic/smt/smt_state.h"
 #include "library/tactic/elaborator_exception.h"
-#include "frontends/lean/tactic_evaluator.h"
-#include "frontends/lean/tactic_notation.h"
+#include "library/tactic/tactic_evaluator.h"
 
 namespace lean {
 static format mk_tactic_error_msg(tactic_state const & ts, format const & fmt) {
diff --git a/src/frontends/lean/tactic_evaluator.h b/src/library/tactic/tactic_evaluator.h
similarity index 96%
rename from src/frontends/lean/tactic_evaluator.h
rename to src/library/tactic/tactic_evaluator.h
index 71cf781355..4fcbc129d6 100644
--- a/src/frontends/lean/tactic_evaluator.h
+++ b/src/library/tactic/tactic_evaluator.h
@@ -8,7 +8,6 @@ Author: Leonardo de Moura
 #include "library/tactic/tactic_state.h"
 #include "library/tactic/elaborator_exception.h"
 #include "library/vm/interaction_state.h"
-#include "frontends/lean/info_manager.h"
 
 namespace lean {
 elaborator_exception unsolved_tactic_state(tactic_state const & ts, format const & fmt, expr const & ref);