cases (even_or_odd n) with
| inl heven =>
 
  exact Even.mul_right heven (n + 1)
| inr hodd =>
  have hsucc : Even (n + 1) := by
   rw [even_add_one, ← odd_iff_not_even]
   exact hodd
  exact Even.mul_left hsucc n
n : ℕ
⊢ Even (n * (n + 1))
no goals