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

State before:
n : Nat
⊢ n % 2 = 1 → n ^^^ 1 = n - 1
Tactic:
intro hodd
State after:
n : Nat
hodd : n % 2 = 1
⊢ n ^^^ 1 = n - 1

State before:
n : Nat
hodd : n % 2 = 1
⊢ n ^^^ 1 = n - 1
Tactic:
have : n ≠ 0 := λ h => by cases h; cases hodd
State after:
n : Nat
hodd : n % 2 = 1
this : n ≠ 0
⊢ n ^^^ 1 = n - 1

State before:
n : Nat
hodd : n % 2 = 1
this : n ≠ 0
⊢ n ^^^ 1 = n - 1
Tactic:
conv =>
  lhs; change bitwise bne n 1
  unfold bitwise; simp [this, hodd]
  change (n/2 ^^^ 0) + (n/2 ^^^ 0)
  rw [Nat.xor_zero, ←Nat.mul_two]
State after:
n : Nat
hodd : n % 2 = 1
this : n ≠ 0
⊢ n / 2 * 2 = n - 1

State before:
n : Nat
hodd : n % 2 = 1
this : n ≠ 0
⊢ n / 2 * 2 = n - 1
Tactic:
conv =>
  rhs; rw [←Nat.div_add_mod n 2, hodd, Nat.add_sub_cancel, Nat.mul_comm]
State after:
no goals

State before:
n : Nat
hodd : n % 2 = 1
h : n = 0
⊢ False
Tactic:
cases h
State after:
case refl
hodd : 0 % 2 = 1
⊢ False

State before:
case refl
hodd : 0 % 2 = 1
⊢ False
Tactic:
cases hodd
State after:
no goals