fix(frontends/lean/parser): bug when applying tactics to synthesize remaining meta-variables

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/parser_tactic.cpp

@@ -254,7 +254,11 @@ expr parser_imp::apply_tactics(expr const & val, metavar_env & menv) {
     buffer<expr> mvars;
     for_each(val, [&](expr const & e, unsigned) {
             if (is_metavar(e)) {
-                mvars.push_back(e);
+                expr m = e;
+                if (has_local_context(m))
+                    m = mk_metavar(metavar_name(m));
+                if (std::find(mvars.begin(), mvars.end(), m) == mvars.end())
+                    mvars.push_back(m);
             }
             return true;
         });

tests/lean/apply_tac_bug.lean

@@ -0,0 +1,10 @@
+import heq
+import macros
+import tactic
+
+theorem my_proof_irrel {a b : Bool} (H1 : a) (H2 : b) : H1 == H2
+:= let H1b       : b                     := cast (by simp) H1,
+       H1_eq_H1b : H1 == H1b             := hsymm (cast_heq (by simp) H1),
+       H1b_eq_H2 : H1b == H2             := to_heq (proof_irrel H1b H2)
+   in  htrans H1_eq_H1b H1b_eq_H2
+

tests/lean/apply_tac_bug.lean.expected.out

@@ -0,0 +1,6 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Imported 'heq'
+  Imported 'macros'
+  Imported 'tactic'
+  Proved: my_proof_irrel