proving goals with ≠

Stream: new members

[João Felipe]

How do I prove goals with ≠?

[Patrick Massot]

Did you read https://leanprover-community.github.io/mathematics_in_lean/C03_Logic.html#negation already?

[João Felipe]

Yes, just read it. :upside_down:

[Patrick Massot]

So you know x ≠ y means x = y implies False. Hence a direct proof starts with intro hxy and then proves a contradiction.

[João Felipe]

How would I prove a contradiction then?

[Mauricio Collares]

Can you give us an example of a particular goal you'd like to prove?

[João Felipe]

1 ≠ 2 * n

[João Felipe]

AKA 1 is not even

[Riccardo Brasca]

First of all you need to find a pen and paper proof... and "it's obvious" doesn't count

[João Felipe]

I already did induction n and proved the zero case with Nat.one_ne_zero

[Riccardo Brasca]

I don't think it's necessary to use induction, you can just use cases, meaning that n is either 0 or succ k. You already did the cases 0 and 2 * (succ k) = 2 * k + 1 + 1, so if this is equal to 1 you get that 2*k + 1 = 0 that is absurd

[João Felipe]

Yes

[Riccardo Brasca]

Of course I am using other results in mathlib, and it depends on what you want to prove by yourself

[Riccardo Brasca]

If your question is how to prove False in general, the solution is to find a lemma that already contains ≠ (for example 0 ≠ 1) and to apply it.

[Riccardo Brasca]

But which lemma to use of course depends on your math proof