How do I easily rewrite nat.succ (nat.succ 0) as 2?

Question

Say my proof goal includes nat.succ (nat.succ 0), and I want to quickly rewrite it to say 2; I can define a whole new theorem:

theorem succ_succ_zero_eq_two : nat.succ (nat.succ 0) = 2 := rfl

then use that theorem with rw, but this seems very clunky. Is there any way to do this in a single line in my proof?

user_617159 · Answer

A simpler solution would use the change tactic:

change 2

user_2852699 · Answer

Use rw (show nat.succ (nat.succ 0) = 2, by refl),