Theorem: Nat.inl_half_eq_or_inr_half_eq (GMLInit/Data/Nat/Coding/Sum.lean)

State before:
n : Nat
⊢ n.half.inl = n ∨ n.half.inr = n
Tactic:
match isEven_or_isOdd n with
| .inl h => left; exact inl_half_eq_of_isEven h
| .inr h => right; exact inr_half_eq_of_isOdd h
State after:
no goals

State before:
n : Nat
h : n.isEven = true
⊢ n.half.inl = n ∨ n.half.inr = n
Tactic:
left
State after:
case h
n : Nat
h : n.isEven = true
⊢ n.half.inl = n

State before:
case h
n : Nat
h : n.isEven = true
⊢ n.half.inl = n
Tactic:
exact inl_half_eq_of_isEven h
State after:
no goals

State before:
n : Nat
h : n.isOdd = true
⊢ n.half.inl = n ∨ n.half.inr = n
Tactic:
right
State after:
case h
n : Nat
h : n.isOdd = true
⊢ n.half.inr = n

State before:
case h
n : Nat
h : n.isOdd = true
⊢ n.half.inr = n
Tactic:
exact inr_half_eq_of_isOdd h
State after:
no goals