change

Like show but for hypotheses. Changes a hypothesis or goal to a definitionally equivalent one.

Example

example (a b : ) (H : a + 0 = b + 0) :
a + 3 = b + 3 :=
begin
  -- a + 0 is definitially equivalent to a, and same for b
  change a = b at H,
  rw H
end