Implementation of the change tactic

def Lean.Elab.Tactic.elabChangeDefaultError (p tgt : Expr) : MetaM MessageData

def Lean.Elab.Tactic.elabChange (e : Expr) (p : Term) (mkDefeqError : Expr → Expr → MetaM MessageData := elabChangeDefaultError) : TacticM 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.

def Lean.Elab.Tactic.evalChange : Tactic

change can be used to replace the main goal or its hypotheses with different, yet definitionally equal, goal or hypotheses.

For example, if n : Nat and the current goal is ⊢ n + 2 = 2, then

change _ + 1 = _

changes the goal to ⊢ n + 1 + 1 = 2.

The tactic also applies to hypotheses. If h : n + 2 = 2 and h' : n + 3 = 4 are hypotheses, then

change _ + 1 = _ at h h'

changes their types to be h : n + 1 + 1 = 2 and h' : n + 2 + 1 = 4.

Change is like refine in that every placeholder needs to be solved for by unification, but using named placeholders or ?_ results in change to creating new goals.

The tactic show e is interchangeable with change e, where the pattern e is applied to the main goal.