## Stream: new members

### Topic: Newbie question

#### Jakob Scholbach (Jan 26 2021 at 20:12):

I am really new to lean, and working through §2 here https://leanprover-community.github.io/mathematics_in_lean/basics.html
I am stuck with this one:

theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b :=
sorry


Of course I would like to say: starting from hypothesis h, add -a on the left and use this lemma sub_self mentioned above in the chapter. What is the syntax to achieve this? Thanks!

#### Johan Commelin (Jan 26 2021 at 20:13):

Hey @Jakob Scholbach nice to see you here!

#### Johan Commelin (Jan 26 2021 at 20:13):

Small tip: you can use #backticks to format your code on Zulip

#### Johan Commelin (Jan 26 2021 at 20:16):

You can go two ways. You can work on the hypothesis h. Or you can work "backward" on the goal.
There is a lemma add_left_cancel that could help with backwards reasoning.

#### Johan Commelin (Jan 26 2021 at 20:18):

For a forward step, you could do something like

example {R : Type} [comm_ring R] {a b : R} (h : a + b = 0) : -a = b :=
begin
have h2 : -a + (a + b) = -a + 0,
{ rw h },
end


#### Johan Commelin (Jan 26 2021 at 20:18):

There are ways of doing this in 1 step. But that's maybe not very enlightening right now.

Ok, thanks!

#### Alex J. Best (Jan 26 2021 at 20:21):

For working backwards from the goal, you can do something like,

import algebra.ring

namespace my_ring

variables {R : Type*} [ring R]

-- BEGIN
theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b :=
begin
rw ← h,
end
end my_ring


#### Patrick Massot (Jan 26 2021 at 20:26):

Beware the exercise asks to do it only with the lemmas discussed before. So we need to know the list of allowed lemmas (that I don't remember).

#### Alex J. Best (Jan 26 2021 at 20:39):

good point, I updated what I wrote to only use lemmas in the tutorial, it got way shorter too :grinning:

Last updated: May 07 2021 at 00:30 UTC