diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 3c933b306f..a4adb7f96b 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1586,7 +1586,7 @@ bool elaborator::try_using_begin_end(substitution & subst, expr const & mvar, pr
                 return false;
             ps = proof_state(ps, tail(gs), subst, ngen);
         } else {
-            expr new_ptac = ptac;
+            expr new_ptac = subst.instantiate_all(ptac);
             if (auto tac = pre_tactic_to_tactic(new_ptac)) {
                 try {
                     proof_state_seq seq = (*tac)(env(), ios(), ps);
@@ -1648,7 +1648,7 @@ void elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set
             return;
         }
 
-        if (auto tac = pre_tactic_to_tactic(*pre_tac)) {
+        if (auto tac = pre_tactic_to_tactic(subst.instantiate_all(*pre_tac))) {
             bool show_failure = true;
             try_using(subst, mvar, ps, *pre_tac, *tac, show_failure);
             return;
diff --git a/tests/lean/hott/457.hlean b/tests/lean/hott/457.hlean
new file mode 100644
index 0000000000..ae03e8d59f
--- /dev/null
+++ b/tests/lean/hott/457.hlean
@@ -0,0 +1,11 @@
+import algebra.group
+
+open eq path_algebra
+
+definition foo {A : Type} (a b c : A) (H₁ : a = c) (H₂ : c = b)  : a = b :=
+begin
+  apply concat,
+  rotate 1,
+  apply H₂,
+  apply H₁
+end