Proof of add_left_cancel from Mathematics in Lean

Stream: new members

[Mike]

Hi,

This is a very basic question. I've started reading "Mathematics in Lean" and ran into issues trying to prove

theorem add_left_cancel {a b c : R} (h : a + b = a + c) : b = c :=

I want to rewrite h so that it becomes

-a + (a + b) = -a + (a + c)

and then use neg_add_cancel_left twice for the left and the right side of the equation, but I can't get it to work.

Here's what I've tried:

import algebra.ring
import tactic

variables {R : Type*} [ring R]

theorem neg_add_cancel_left (a b : R) : -a + (a + b) = b :=
by rw [←add_assoc, add_left_neg, zero_add]

theorem add_left_cancel {a b c : R} (h : a + b = a + c) : b = c :=
begin
    have h₁ : -a + (a + b) = -a + (a + c),
    {rw h},
    have h₂ : -a + (a + b) = c,
    {rw neg_add_cancel_left},
    rw neg_add_cancel_left
end

I end up with this error:
/-
solve1 tactic failed, focused goal has not been solved
state:
R : Type u_1,
_inst_1 : ring R,
a b c : R,
h : a + b = a + c,
h₁ : -a + (a + b) = -a + (a + c)
⊢ b = c
-/

So it looks like h₂ isn't established. I'm not able to get it to use neg_add_cancel_left.

I'd appreciate it if someone could show me what I'm doing wrong.
Thanks!

[Alex J. Best]

I think you want to rewrite at your hypotheses rather than making new hypotheses for the next steps (you can do this of course but it gets a bit unwieldy).

theorem add_left_cancel {a b c : R} (h : a + b = a + c) : b = c :=
begin
    have h₁ : -a + (a + b) = -a + (a + c),
    {rw h,},
    rw neg_add_cancel_left at h₁,
    rw neg_add_cancel_left at h₁,
    exact h₁,
end