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

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

State before:
case zero

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

State before:
case zero
a✝ : isEven 0 = true
⊢ (half 0).inl = 0
Tactic:
rfl
State after:
no goals

State before:
case one

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

State before:
case one
a✝ : isEven 1 = true
⊢ (half 1).inl = 1
Tactic:
contradiction
State after:
no goals

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

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

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

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