(u : Fin 2) → (Even u ↔ Even u.val)

Stream: general

[Iván Renison]

Hello, I'm trying to prove this:

theorem aux28 (u : Fin 2) : Even u ↔ Even u.val := sorry

Witch I think should also be valid for Fin n, but I'm not being able to prove it.
I was able to reduce it to having to prove this:

theorem aux33 : ¬Even (1 : Fin 2) := sorry

But i'm not able to prove that neither
How could I do?

[Ruben Van de Velde]

Not for odd $n$:

example : ¬∀ (u : Fin 5), Even u ↔ Even u.val := by
  simp
  use 3
  simp
  use 4
  simp

[Thomas Murrills]

theorem aux33 : ¬Even (1 : Fin 2) := by unfold Even; decide works. (I feel like decide should work without the unfold; presumably we just could do with another instance somewhere?)

[Iván Renison]

Thank you

[Yury G. Kudryashov]

I'm working on

lemma Fin.even_iff {n : ℕ} {k : Fin n} : Even k ↔ Odd n ∨ Even k.val := by