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

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

State before:
case zero

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

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

State before:
case succ
n : Nat
ih : (2 * n).half = n
⊢ (2 * (n + 1)).half = n + 1
Tactic:
rw [Nat.mul_succ, Nat.half, ih]
State after:
no goals