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

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

State before:
case zero

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

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

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

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