How to choose a case of an inductive in the goal?

Stream: new members

[An Qi Zhang]

Hello! I was wondering if I have an inductive in the goal of a lemma/theorem, is it possible to choose a specific case of the inductive to prove? The constructor tactic just chooses the first case of the inductive, but doesn't let me choose a specific case of the inductive.

Here's an MWE to help illustrate:

import Mathlib

inductive Nat.OddEven (n : Nat) : Prop
| isOdd : n % 2 = 1 → Nat.OddEven n
| isEven : n % 2 = 0 → Nat.OddEven n

lemma Nat.is_odd_or_even (n : Nat) : Nat.OddEven n := by
  cases n
  case zero =>
    -- How do I choose a case of `Nat.OddEvent` such as `isEven`?
    sorry
  case succ n' =>
    sorry

[Ruben Van de Velde]

Try refine .isEven ?_