fix: disable auto implicit feature when running tactics

fixes #1569

src/Lean/Elab/SyntheticMVars.lean

@@ -325,7 +325,7 @@ mutual
   /--
   Try to synthesize a term `val` using the tactic code `tacticCode`, and then assign `mvarId := val`.
   -/
-  partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := do
+  partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := withoutAutoBoundImplicit do
     /- Recall, `tacticCode` is the whole `by ...` expression. -/
     let code := tacticCode[1]
     instantiateMVarDeclMVars mvarId

tests/lean/1569.lean

@@ -0,0 +1,2 @@
+def foo (x : Nat) (_ : x = 0) : Nat := x
+example : foo 0 (by simp [typo]; done) = 0 := sorry

tests/lean/1569.lean.expected.out

@@ -0,0 +1 @@
+1569.lean:2:26-2:30: error: unknown identifier 'typo'