simple proof

Stream: new members

[Rohan Joshi]

Hi, I was just getting through the Natural Number Game and I had proven the following a + n = b + n → a = b, and I ended up at a = b → a = b. Is there any way to show that the above statement is true? I tried rfl, symm, everything but it doesnt work

[Damiano Testa]

Does exact id work?

[Kyle Miller]

You can also do intro h followed by exact h or assumption

[Kyle Miller]

(exact id should work, but it's not the sort of thing that NNG teaches)

[Kevin Buzzard]

I always use exact id when speedrunning but it was a conscious choice not to tell the user about this option

[Rohan Joshi]

Thanks for the suggestion!
Originally, I decided to use induction n with c hc, so we can solve the intermediate goal. However (after I solved the first goal), when I'm solving goal 2, it keeps repeating the same assumption and desired goal. How should I proceed from here? I tried using exact h, but it showed up as an error . I tried using simp:
Screenshot-2024-06-25-at-1.07.16PM.png

[Ruben Van de Velde]

Probably rw [hc] at the top of your screenshot does not do what you expect

[Ruben Van de Velde]

I think you want apply hc at that point instead