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.

def change? : Lean.ParserDescr

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`

Equations

• One or more equations did not get rendered due to their size.