Simple question about online tutorial example

Stream: general

[M. Andrew Moshier]

The following from the online Lean tutorial (Lean 2) doesn't work as is in Lean 3. I figured out that I needed to change underscores in the tutorial into inaccessibles in the mutual theorem. Fine. But I still don't see how to prove not_odd_zero.

mutual inductive even, odd
with even : ℕ → Prop
| even_zero : even 0
| even_succ : ∀ n, odd n → even (n + 1)
with odd : ℕ → Prop
| odd_succ : ∀ n, even n → odd (n + 1)

open even odd

theorem not_odd_zero : ¬ (odd 0).

mutual theorem even_of_odd_succ, odd_of_even_succ
with even_of_odd_succ : ∀ n, odd (n + 1) → even n
| .(n) (odd_succ n h) := h
with odd_of_even_succ : ∀ n, even (n + 1) → odd n
| .(n) (even_succ n h) := h

[Mario Carneiro]

that works for me in 3.4.1

[Mario Carneiro]

There is also no need for the mutual theorem, since the proof is non-recursive. This works too:

theorem even_of_odd_succ : ∀ n, odd (n + 1) → even n
| .(n) (odd_succ n h) := h

theorem odd_of_even_succ : ∀ n, even (n + 1) → odd n
| .(n) (even_succ n h) := h

[M. Andrew Moshier]

I know it doesn't need to be mutual. This is lifted as is (except the change to inaccessibles) from the tutorial. My vscode is using 3.2.x; Emacs is using 3.4.x. I'll fix that. Thanks.