show

A tactic which can be used to change a goal to a definitionally equivalent goal. Note also change, which works both with goals and hypotheses.

Example

If n : ℕ then n + 0 is definitionally equivalent to n, so the following proof works:

try it!

example (a b : ℕ) : (a + 0) + b = b + a :=
begin
  change a + b = b + a,
  rw add_comm
end