def Lean.Elab.runTactic (mvarId : MVarId) (tacticCode : Syntax) (ctx : Term.Context := { }) (s : Term.State := { }) : MetaM (List MVarId × Term.State)

Apply the give tactic code to mvarId in MetaM.