Odd and even numbers proof

Stream: new members

[Pehan Amarathunge]

example (h: ∃(n:ℕ), even n ∧ even (n+1)) : ∃(k:ℕ), even (2*k + 1) :=
begin

end

Hi. Can someone please help me with this proof about odd and even numbers?

Thank you

[Heather Macbeth]

@Pehan Amarathunge What have you tried? Where did you learn about this problem? It looks kind of like a homework problem ...

[Heather Macbeth]

Also, please read the page #mwe about how to provide a self-contained example for people to look at. The best approach is to explain in words the mathematics of the idea you're trying to implement, and the code you tried in implementing that idea, together with the error message that you encountered.

[Pehan Amarathunge]

Sure!

begin
  cases h with m n,
  cases n with p q,
  unfold even,

I have tried the following, but I'm a bit stuck on how to proceed.
I would like to know if I am in the right direction and if so a hint on how to proceed would be appreciated.

[Heather Macbeth]

@Pehan Amarathunge You should also tell us the mathematical idea of the solution you want to write in Lean!

[Kevin Buzzard]

Yeah I think the main question here is "what is the maths proof you're trying to formalise". Lean doesn't create mathematics by itself, humans translate already-created mathematics into Lean's language, and Lean checks it.