# Zulip Chat Archive

## Stream: new members

### Topic: Proof of self_sub for Mathematics in Lean

#### Mike (Aug 27 2020 at 15:39):

Hi,

I'm hoping someone can help me with my attempted proof of

```
theorem self_sub (a : R) : a - a = 0 :=
```

Here's what I have:

```
import algebra.ring
import tactic
variables {R : Type*} [ring R]
theorem eq_neg_of_add_eq_zero {a b : R} (h : a + b = 0) : a = -b :=
...
theorem sub_eq_add_neg (a b : R) : a - b = a + -b :=
by reflexivity
theorem neg_neg (a : R) : -(-a) = a :=
...
theorem self_sub (a : R) : a - a = 0 :=
begin
have h₁ : a = -(-a),
{rw neg_neg},
have h₂ : a + (-a) = 0,
{rw ←eq_neg_of_add_eq_zero at h₁},
have h₂ := sub_eq_add_neg h₂,
exact h₂,
end
```

The justification of h₂ doesn't work:

/-

rewrite tactic failed, lemma lhs is a metavariable

state:

R : Type u_1,

_inst_1 : ring R,

a : R,

h₁ : a = - -a

⊢ a + -a = 0

-/

Could someone explain what caused this error and what it means please.

Thanks!

#### Yakov Pechersky (Aug 27 2020 at 15:47):

With minimal changes from what you have:

```
import algebra.ring
import tactic
variables {R : Type*} [ring R]
theorem eq_neg_of_add_eq_zero' {a b : R} : a + b = 0 ↔ a = -b := sorry
theorem sub_eq_add_neg' (a b : R) : a - b = a + -b :=
by reflexivity
theorem neg_neg' (a : R) : -(-a) = a := sorry
theorem self_sub (a : R) : a - a = 0 :=
begin
have h₁ : a = -(-a),
{ rw neg_neg' },
have h₂ : a + (-a) = 0,
{ rw ←eq_neg_of_add_eq_zero' at h₁,
exact h₁ },
rw ←sub_eq_add_neg' at h₂,
exact h₂,
end
```

#### Yakov Pechersky (Aug 27 2020 at 15:48):

I named them all "prime" to avoid clashes with names in mathlib

#### Yakov Pechersky (Aug 27 2020 at 15:49):

I changed the first lemma to `\iff`

format, so that it can be used for rewrites.

#### Yakov Pechersky (Aug 27 2020 at 15:50):

Before, having the hypothesis on the left as an explicit argument makes it not possible to use it as a rewrite how you wanted to, that was the metavariable issue.

#### Yakov Pechersky (Aug 27 2020 at 15:50):

Because how you had it originally, `eq_neg_of_add_eq_zero`

needed an explicit argument. And that explicit argument was exactly what you were trying to prove in the goal.

#### Johan Commelin (Aug 27 2020 at 15:51):

@Mike In particular, what went wrong with your first attempt is that you tried to treat `eq_neg_of_add_eq_zero`

as an iff statement, but it is only one direction of the iff that you are looking for. (And the wrong direction unfortunately.)

#### Yakov Pechersky (Aug 27 2020 at 15:51):

Additionally, I changed the `have h2 := ...`

to `rw ... at h2`

#### Yakov Pechersky (Aug 27 2020 at 15:52):

Because you can't just apply an equality of the form `a = b`

to a hypothesis of `h2 := a`

to get `h2 := b`

. That's exactly what the rewrite tactic does instead.

Last updated: May 13 2021 at 06:15 UTC