An alternative to this fix -- which just uses the code that was originally intended -- would be to make an explicit reference into the namespaces. Either way the behaviour is complicated enough that it might be worth an additional sentence to say what's going on.
mutual theorem even_of_odd_succ, odd_of_even_succ
with even_of_odd_succ : ∀ n, odd (n + 1) → even n
| _ (odd.odd_succ n h) := h
with odd_of_even_succ : ∀ n, even (n + 1) → odd n
| _ (even.even_succ n h) := h
An alternative to this fix -- which just uses the code that was originally intended -- would be to make an explicit reference into the namespaces. Either way the behaviour is complicated enough that it might be worth an additional sentence to say what's going on.