Zulip Chat Archive

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:

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

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.

Kevin Buzzard (Aug 21 2020 at 07:45):


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: Dec 20 2023 at 11:08 UTC