Newbie question

Stream: new members

[Jakob Scholbach]

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]

Hey @Jakob Scholbach nice to see you here!

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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

[Jakob Scholbach]

Ok, thanks!

[Alex J. Best]

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 ← add_zero (-a),
rw ← h,
rw neg_add_cancel_left,
end
end my_ring

[Patrick Massot]

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]

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