diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index aed8889750..a8a95edcb0 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -357,27 +357,6 @@ expr univ_metavars_to_params(environment const & env, local_decls<level> const &
     return univ_metavars_to_params_fn(env, lls, s, ps, new_ps)(e);
 }
 
-expr instantiate_meta(expr const & meta, substitution & subst) {
-    lean_assert(is_meta(meta));
-    buffer<expr> locals;
-    expr mvar = get_app_args(meta, locals);
-    mvar = update_mlocal(mvar, subst.instantiate_all(mlocal_type(mvar)));
-    for (auto & local : locals)
-        local = subst.instantiate_all(local);
-    return mk_app(mvar, locals);
-}
-
-justification mk_failed_to_synthesize_jst(environment const & env, expr const & m) {
-    return mk_justification(m, [=](formatter const & fmt, substitution const & subst) {
-            substitution tmp(subst);
-            expr new_m    = instantiate_meta(m, tmp);
-            expr new_type = type_checker(env).infer(new_m).first;
-            bool relax_main_opaque = true; // this value doesn't really matter for pretty printing
-            proof_state ps = to_proof_state(new_m, new_type, name_generator("dontcare"), relax_main_opaque);
-            return format("failed to synthesize placeholder") + line() + ps.pp(fmt);
-        });
-}
-
 justification mk_type_mismatch_jst(expr const & v, expr const & v_type, expr const & t, expr const & src) {
     return mk_justification(src, [=](formatter const & fmt, substitution const & subst) {
             substitution s(subst);
@@ -393,21 +372,6 @@ justification mk_type_mismatch_jst(expr const & v, expr const & v_type, expr con
         });
 }
 
-pair<expr, justification> update_meta(expr const & meta, substitution s) {
-    buffer<expr> args;
-    expr mvar = get_app_args(meta, args);
-    justification j;
-    auto p = s.instantiate_metavars(mlocal_type(mvar));
-    mvar   = update_mlocal(mvar, p.first);
-    j      = p.second;
-    for (expr & arg : args) {
-        auto p = s.instantiate_metavars(mlocal_type(arg));
-        arg    = update_mlocal(arg, p.first);
-        j      = mk_composite1(j, p.second);
-    }
-    return mk_pair(mk_app(mvar, args), j);
-}
-
 std::tuple<expr, level_param_names> parse_local_expr(parser & p) {
     expr e   = p.parse_expr();
     list<expr> ctx = p.locals_to_context();
diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h
index 1e8273147d..458b1e3844 100644
--- a/src/frontends/lean/util.h
+++ b/src/frontends/lean/util.h
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/expr_sets.h"
 #include "kernel/type_checker.h"
 #include "library/util.h"
+#include "library/tactic/util.h"
 #include "frontends/lean/local_decls.h"
 
 namespace lean {
@@ -80,13 +81,6 @@ bool occurs(level const & u, level const & l);
 expr univ_metavars_to_params(environment const & env, local_decls<level> const & lls, substitution & s,
                              name_set & ps, buffer<name> & new_ps, expr const & e);
 
-/** \brief Instantiate metavariable application \c meta (?M ...) using \c subst  */
-expr instantiate_meta(expr const & meta, substitution & subst);
-
-/** \brief Return a 'failed to synthesize placholder' justification for the given
-    metavariable application \c m of the form (?m l_1 ... l_k) */
-justification mk_failed_to_synthesize_jst(environment const & env, expr const & m);
-
 /** \brief Return a justification for \c v_type being definitionally equal to \c t,
     <tt> v : v_type</tt>, the expressiong \c src is used to extract position information.
 */
@@ -95,12 +89,6 @@ inline justification mk_type_mismatch_jst(expr const & v, expr const & v_type, e
     return mk_type_mismatch_jst(v, v_type, t, v);
 }
 
-/** \brief Given a metavariable application (?m l_1 ... l_n), apply \c s to the types of
-    ?m and local constants l_i
-    Return the updated expression and a justification for all substitutions.
-*/
-pair<expr, justification> update_meta(expr const & meta, substitution s);
-
 /** \brief Auxiliary function for check/eval/find_decl */
 std::tuple<expr, level_param_names> parse_local_expr(parser & p);
 
diff --git a/src/library/tactic/util.cpp b/src/library/tactic/util.cpp
index f1f0583627..d435102e33 100644
--- a/src/library/tactic/util.cpp
+++ b/src/library/tactic/util.cpp
@@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "kernel/type_checker.h"
 #include "library/aliases.h"
 #include "library/tactic/util.h"
+#include "library/tactic/proof_state.h"
 
 namespace lean {
 bool is_tactic_namespace_open(environment const & env) {
@@ -27,4 +29,40 @@ bool is_tactic_namespace_open(environment const & env) {
     }
     return false;
 }
+
+pair<expr, justification> update_meta(expr const & meta, substitution s) {
+    buffer<expr> args;
+    expr mvar = get_app_args(meta, args);
+    justification j;
+    auto p = s.instantiate_metavars(mlocal_type(mvar));
+    mvar   = update_mlocal(mvar, p.first);
+    j      = p.second;
+    for (expr & arg : args) {
+        auto p = s.instantiate_metavars(mlocal_type(arg));
+        arg    = update_mlocal(arg, p.first);
+        j      = mk_composite1(j, p.second);
+    }
+    return mk_pair(mk_app(mvar, args), j);
+}
+
+expr instantiate_meta(expr const & meta, substitution & subst) {
+    lean_assert(is_meta(meta));
+    buffer<expr> locals;
+    expr mvar = get_app_args(meta, locals);
+    mvar = update_mlocal(mvar, subst.instantiate_all(mlocal_type(mvar)));
+    for (auto & local : locals)
+        local = subst.instantiate_all(local);
+    return mk_app(mvar, locals);
+}
+
+justification mk_failed_to_synthesize_jst(environment const & env, expr const & m) {
+    return mk_justification(m, [=](formatter const & fmt, substitution const & subst) {
+            substitution tmp(subst);
+            expr new_m    = instantiate_meta(m, tmp);
+            expr new_type = type_checker(env).infer(new_m).first;
+            bool relax_main_opaque = true; // this value doesn't really matter for pretty printing
+            proof_state ps = to_proof_state(new_m, new_type, name_generator("dontcare"), relax_main_opaque);
+            return format("failed to synthesize placeholder") + line() + ps.pp(fmt);
+        });
+}
 }
diff --git a/src/library/tactic/util.h b/src/library/tactic/util.h
index cfbd9eb506..3c921e0430 100644
--- a/src/library/tactic/util.h
+++ b/src/library/tactic/util.h
@@ -9,4 +9,17 @@ Author: Leonardo de Moura
 namespace lean {
 /** \brief Return true iff the tactic namespace is open in given environment. */
 bool is_tactic_namespace_open(environment const & env);
+
+/** \brief Instantiate metavariable application \c meta (?M ...) using \c subst  */
+expr instantiate_meta(expr const & meta, substitution & subst);
+
+/** \brief Given a metavariable application (?m l_1 ... l_n), apply \c s to the types of
+    ?m and local constants l_i
+    Return the updated expression and a justification for all substitutions.
+*/
+pair<expr, justification> update_meta(expr const & meta, substitution s);
+
+/** \brief Return a 'failed to synthesize placholder' justification for the given
+    metavariable application \c m of the form (?m l_1 ... l_k) */
+justification mk_failed_to_synthesize_jst(environment const & env, expr const & m);
 }