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

State before:
n : Nat
⊢ n.isOdd = true → n.half.inr = n
Tactic:
induction n using Nat.recTwo with
| zero => intro; contradiction
| one => intro; rfl
| step n ih =>
  intro h
  unfold Nat.inr at ih ⊢
  unfold Nat.half
  rw [Nat.mul_succ, Nat.add_succ, Nat.add_succ, ih h]
State after:
no goals

State before:
case zero

⊢ isOdd 0 = true → (half 0).inr = 0
Tactic:
intro
State after:
case zero
a✝ : isOdd 0 = true
⊢ (half 0).inr = 0

State before:
case zero
a✝ : isOdd 0 = true
⊢ (half 0).inr = 0
Tactic:
contradiction
State after:
no goals

State before:
case one

⊢ isOdd 1 = true → (half 1).inr = 1
Tactic:
intro
State after:
case one
a✝ : isOdd 1 = true
⊢ (half 1).inr = 1

State before:
case one
a✝ : isOdd 1 = true
⊢ (half 1).inr = 1
Tactic:
rfl
State after:
no goals

State before:
case step
n : Nat
ih : n.isOdd = true → n.half.inr = n
⊢ (n + 2).isOdd = true → (n + 2).half.inr = n + 2
Tactic:
intro h
State after:
case step
n : Nat
ih : n.isOdd = true → n.half.inr = n
h : (n + 2).isOdd = true
⊢ (n + 2).half.inr = n + 2

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

State before:
case step
n : Nat
ih : n.isOdd = true → 2 * n.half + 1 = n
h : (n + 2).isOdd = true
⊢ 2 * (n + 2).half + 1 = n + 2
Tactic:
unfold Nat.half
State after:
case step
n : Nat
ih : n.isOdd = true → 2 * n.half + 1 = n
h : (n + 2).isOdd = true
⊢ 2 * (n.half + 1) + 1 = n + 2

State before:
case step
n : Nat
ih : n.isOdd = true → 2 * n.half + 1 = n
h : (n + 2).isOdd = true
⊢ 2 * (n.half + 1) + 1 = n + 2
Tactic:
rw [Nat.mul_succ, Nat.add_succ, Nat.add_succ, ih h]
State after:
no goals