## Stream: new members

### Topic: le_zero

#### Claus-Peter Becke (Aug 21 2020 at 07:36):

I tried to prove the lemma in the Natural Number Game in Inequation World level 7 with the following tactics:

cases h with c ha,
symmetry at ha,
have h2 := add_right_eq_zero ha if ha : a + c = 0,
exact h2,


All goals were closed. But there remained the following error messages:

Messages
20:32: error:
invalid 'begin-end' expression, ',' expected
21:0: error:
sync


I don't know which operations cause the messages and what I can do to avoid them? Does anybody have an explanation and a hint?

#### Shing Tak Lam (Aug 21 2020 at 07:41):

I think the issue is to do with the if there. Notice the "if" in the message on the top is not monospace (ie not code)

#### Claus-Peter Becke (Aug 21 2020 at 07:45):

Thank you for that hint. So I will have a closer look on the if to find the causes for this error message.

(deleted)

#### Kevin Buzzard (Aug 21 2020 at 07:46):

Yeah that definition of h2 doesn't make any sense to Lean

#### Claus-Peter Becke (Aug 21 2020 at 07:52):

At the first attempt I obviously followed too directly the explanations and hints in level 7 in Inequality World. In the meantime I substituted the line containing the have-tactic by the following one:




That works fine.

#### Claus-Peter Becke (Aug 21 2020 at 07:53):

exact add_right_eq_zero ha


Last updated: May 16 2021 at 05:21 UTC