Implementation of the change tactic

def Lean.Elab.Tactic.elabChange (e : Lean.Expr) (p : Lean.Term) : Lean.Elab.Tactic.TacticM Lean.Expr

Elaborates the pattern p and ensures that it is defeq to e. Emulates (show p from ?m : e), returning the type of ?m, but e and p do not need to be types. Unlike (show p from ?m : e), this can assign synthetic opaque metavariables appearing in p.