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

State before:
⊢ isEven = Nat.isEvenImpl
Tactic:
funext n
State after:
case h
n : Nat
⊢ n.isEven = Nat.isEvenImpl n

State before:
case h
n : Nat
⊢ n.isEven = Nat.isEvenImpl n
Tactic:
induction n using Nat.recTwo with
| zero => rfl
| one => rfl
| step n ih =>
  unfold Nat.isEven
  rw [isEvenImpl, Nat.add_mod_right, ih]
State after:
no goals

State before:
case h.zero

⊢ isEven 0 = Nat.isEvenImpl 0
Tactic:
rfl
State after:
no goals

State before:
case h.one

⊢ isEven 1 = Nat.isEvenImpl 1
Tactic:
rfl
State after:
no goals

State before:
case h.step
n : Nat
ih : n.isEven = Nat.isEvenImpl n
⊢ (n + 2).isEven = Nat.isEvenImpl (n + 2)
Tactic:
unfold Nat.isEven
State after:
case h.step
n : Nat
ih : n.isEven = Nat.isEvenImpl n
⊢ n.isEven = Nat.isEvenImpl (n + 2)

State before:
case h.step
n : Nat
ih : n.isEven = Nat.isEvenImpl n
⊢ n.isEven = Nat.isEvenImpl (n + 2)
Tactic:
rw [isEvenImpl, Nat.add_mod_right, ih]
State after:
no goals