Theorem: Nat.parityZeroCases (Lib.lean)

State before:
C : ℕ → Sort u
z : C 0
o : (n : ℕ) → C (2 * n + 1)
e : (n : ℕ) → C (2 * n + 2)
⊢ (n : ℕ) → C n
Tactic:
intro n
State after:
C : ℕ → Sort u
z : C 0
o : (n : ℕ) → C (2 * n + 1)
e : (n : ℕ) → C (2 * n + 2)
n : ℕ
⊢ C n

State before:
C : ℕ → Sort u
z : C 0
o : (n : ℕ) → C (2 * n + 1)
e : (n : ℕ) → C (2 * n + 2)
n : ℕ
⊢ C n
Tactic:
cases n using Nat.binaryRec' with
| z => exact z
| f b n hb =>
  cases b with
  | true => simpa [← Nat.two_mul] using o _
  | false =>
    match n with
    | 0 => exact absurd (hb rfl) Bool.noConfusion
    | n+1 => simpa [← Nat.add_assoc, Nat.add_right_comm _ 1, ← Nat.two_mul] using e _
State after:
no goals

State before:
case z
C : ℕ → Sort u
z : C 0
o : (n : ℕ) → C (2 * n + 1)
e : (n : ℕ) → C (2 * n + 2)
⊢ C 0
Tactic:
exact z
State after:
no goals

State before:
case f
C : ℕ → Sort u
z : C 0
o : (n : ℕ) → C (2 * n + 1)
e : (n : ℕ) → C (2 * n + 2)
b : Bool
n : ℕ
hb : n = 0 → b = true
a✝ : bit b n = n → C (bit b n)
⊢ C (bit b n)
Tactic:
cases b with
| true => simpa [← Nat.two_mul] using o _
| false =>
  match n with
  | 0 => exact absurd (hb rfl) Bool.noConfusion
  | n+1 => simpa [← Nat.add_assoc, Nat.add_right_comm _ 1, ← Nat.two_mul] using e _
State after:
no goals

State before:
case f.true
C : ℕ → Sort u
z : C 0
o : (n : ℕ) → C (2 * n + 1)
e : (n : ℕ) → C (2 * n + 2)
n : ℕ
hb : n = 0 → true = true
a✝ : bit true n = n → C (bit true n)
⊢ C (bit true n)
Tactic:
simpa [← Nat.two_mul] using o _
State after:
no goals

State before:
case f.false
C : ℕ → Sort u
z : C 0
o : (n : ℕ) → C (2 * n + 1)
e : (n : ℕ) → C (2 * n + 2)
n : ℕ
hb : n = 0 → false = true
a✝ : bit false n = n → C (bit false n)
⊢ C (bit false n)
Tactic:
match n with
| 0 => exact absurd (hb rfl) Bool.noConfusion
| n+1 => simpa [← Nat.add_assoc, Nat.add_right_comm _ 1, ← Nat.two_mul] using e _
State after:
no goals

State before:
C : ℕ → Sort u
z : C 0
o : (n : ℕ) → C (2 * n + 1)
e : (n : ℕ) → C (2 * n + 2)
n : ℕ
hb : 0 = 0 → false = true
a✝ : bit false 0 = 0 → C (bit false 0)
⊢ C (bit false 0)
Tactic:
exact absurd (hb rfl) Bool.noConfusion
State after:
no goals

State before:
C : ℕ → Sort u
z : C 0
o : (n : ℕ) → C (2 * n + 1)
e : (n : ℕ) → C (2 * n + 2)
n✝ n : ℕ
hb : n + 1 = 0 → false = true
a✝ : bit false (n + 1) = n + 1 → C (bit false (n + 1))
⊢ C (bit false (n + 1))
Tactic:
simpa [← Nat.add_assoc, Nat.add_right_comm _ 1, ← Nat.two_mul] using e _
State after:
no goals