This tactic is used to suggest a replacement of the goal by a definitionally equal term.
term is intended to contain holes which get unified with the main goal and filled in explicitly
in the suggestion.
term can also be omitted, in which case
change? simply suggests
change with the main goal.
This is helpful after tactics like
dsimp, which can then be deleted.
change? term unifies
term with the current goal, then suggests explicit
that uses the resulting unified term.
term is not present,
change? suggests the current goal itself. This is useful after tactics
which transform the goal while maintaining definitional equality, such as
dsimp; those preceding
tactic calls can then be deleted.