add_right_cancel natural number game

Stream: new members

[Thomas Laraia]

Hi, I am working on add_right_cancel in Advanced Addition World and am not understanding why I cannot apply succ_inj to the h hypothesis. I can see the steps that need to be taken but maybe I need to take a more roundabout way?

intro h,
induction t with d hd,
rw add_zero at h,
rw add_zero at h,
rw h,
refl,
repeat {rw add_succ at h},
apply succ_inj at h,

[Thomas Laraia]

And at the same time, if I just apply succ_inj, the goal changes from a = b to succ a = succ b, which feels like the opposite of what succ_inj is supposed to do.

[Ruben Van de Velde]

You've fallen victim to a common misunderstanding about apply. apply means "I've got a lemma whose conclusion matches the goal, so to prove my goal, it suffices to prove the hypothesis of this lemma"

[Ruben Van de Velde]

In this case, you want to use succ_inj {a b : mynat} : succ(a) = succ(b) → a = b with the hypothesis h : succ (a + d) = succ (b + d) to conclude a + d = b + d; you do that by treating → as a function application: have h2 := succ_inj h,

[Ruben Van de Velde]

Alternatively, you can go backwards from the goal and claim it suffices to prove a + d = b + d by apply hd,

[Thomas Laraia]

Perfect, thank you for the explanation!