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

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

State before:
case zero

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

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

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