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

State before:
n : Nat
⊢ n.inl.isEven = true
Tactic:
induction n with
| zero => rfl
| succ n ih =>
  unfold Nat.inl at ih ⊢
  rw [Nat.mul_succ]
  exact ih
State after:
no goals

State before:
case zero

⊢ (Nat.inl 0).isEven = true
Tactic:
rfl
State after:
no goals

State before:
case succ
n : Nat
ih : n.inl.isEven = true
⊢ (n + 1).inl.isEven = true
Tactic:
unfold Nat.inl at ih ⊢
State after:
case succ
n : Nat
ih : (2 * n).isEven = true
⊢ (2 * (n + 1)).isEven = true

State before:
case succ
n : Nat
ih : (2 * n).isEven = true
⊢ (2 * (n + 1)).isEven = true
Tactic:
rw [Nat.mul_succ]
State after:
case succ
n : Nat
ih : (2 * n).isEven = true
⊢ (2 * n + 2).isEven = true

State before:
case succ
n : Nat
ih : (2 * n).isEven = true
⊢ (2 * n + 2).isEven = true
Tactic:
exact ih
State after:
no goals