le_zero

Stream: new members

[Claus-Peter Becke]

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]

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]

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]

(deleted)

[Kevin Buzzard]

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

[Claus-Peter Becke]

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]

exact add_right_eq_zero ha