Tactic change? term #

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 change syntax that uses the resulting unified term.

If 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.

example : (fun x : Nat => x) 0 = 1 := by
  change? 0 = _  -- `Try this: change 0 = 1`
Instances For