Additions to Lean.Elab.Tactic.Basic

def Lean.Elab.Tactic.getMainTarget'' : TacticM Expr

Return expected type for the main goal, cleaning up annotations, using Lean.MVarId.getType''. Remark: note that MVarId.getType' uses whnf instead of cleanupAnnotations, and MVarId.getType'' also uses cleanupAnnotations