Theorem: Nat.even_xor_one (Algdata/Data/Nat/Bits.lean)

State before:
n : Nat
⊢ n % 2 = 0 → n ^^^ 1 = n + 1
Tactic:
intro heven
State after:
n : Nat
heven : n % 2 = 0
⊢ n ^^^ 1 = n + 1

State before:
n : Nat
heven : n % 2 = 0
⊢ n ^^^ 1 = n + 1
Tactic:
by_cases n = 0
State after:
case pos
n : Nat
heven : n % 2 = 0
h✝ : n = 0
⊢ n ^^^ 1 = n + 1

case neg
n : Nat
heven : n % 2 = 0
h✝ : ¬n = 0
⊢ n ^^^ 1 = n + 1

State before:
n : Nat
heven : n % 2 = 0
h : n = 0
⊢ n ^^^ 1 = n + 1
Tactic:
case pos h => cases h; decide
State after:
no goals

State before:
n : Nat
heven : n % 2 = 0
h : ¬n = 0
⊢ n ^^^ 1 = n + 1
Tactic:
case neg h =>
  conv =>
    lhs; change bitwise bne n 1
    unfold bitwise; simp [h, heven]
    change (n/2 ^^^ 0) + (n/2 ^^^ 0) + 1
    rw [Nat.xor_zero, ←Nat.mul_two, Nat.div_mul_cancel (Nat.dvd_of_mod_eq_zero heven)]
State after:
no goals

State before:
n : Nat
heven : n % 2 = 0
h : n = 0
⊢ n ^^^ 1 = n + 1
Tactic:
cases h
State after:
case refl
heven : 0 % 2 = 0
⊢ 0 ^^^ 1 = 0 + 1

State before:
case refl
heven : 0 % 2 = 0
⊢ 0 ^^^ 1 = 0 + 1
Tactic:
decide
State after:
no goals

State before:
n : Nat
heven : n % 2 = 0
h : ¬n = 0
⊢ n ^^^ 1 = n + 1
Tactic:
conv =>
  lhs; change bitwise bne n 1
  unfold bitwise; simp [h, heven]
  change (n/2 ^^^ 0) + (n/2 ^^^ 0) + 1
  rw [Nat.xor_zero, ←Nat.mul_two, Nat.div_mul_cancel (Nat.dvd_of_mod_eq_zero heven)]
State after:
no goals