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

State before:
n : Nat
⊢ succ n = (n ^^^ 1) + (n &&& 1) <<< 1
Tactic:
cases n.mod_two_eq_zero_or_one
State after:
case inl
n : Nat
h✝ : n % 2 = 0
⊢ succ n = (n ^^^ 1) + (n &&& 1) <<< 1

case inr
n : Nat
h✝ : n % 2 = 1
⊢ succ n = (n ^^^ 1) + (n &&& 1) <<< 1

State before:
n : Nat
h : n % 2 = 0
⊢ succ n = (n ^^^ 1) + (n &&& 1) <<< 1
Tactic:
case inl h => simp [Nat.even_xor_one h, h]
State after:
no goals

State before:
n : Nat
h : n % 2 = 1
⊢ succ n = (n ^^^ 1) + (n &&& 1) <<< 1
Tactic:
case inr h =>
  simp [Nat.odd_xor_one h, h]
  cases n
  case zero => cases h
  case succ n => rfl
State after:
no goals

State before:
n : Nat
h : n % 2 = 0
⊢ succ n = (n ^^^ 1) + (n &&& 1) <<< 1
Tactic:
simp [Nat.even_xor_one h, h]
State after:
no goals

State before:
n : Nat
h : n % 2 = 1
⊢ succ n = (n ^^^ 1) + (n &&& 1) <<< 1
Tactic:
simp [Nat.odd_xor_one h, h]
State after:
n : Nat
h : n % 2 = 1
⊢ n = n - 1 + 1

State before:
n : Nat
h : n % 2 = 1
⊢ n = n - 1 + 1
Tactic:
cases n
State after:
case zero
h : zero % 2 = 1
⊢ zero = zero - 1 + 1

case succ
n✝ : Nat
h : succ n✝ % 2 = 1
⊢ succ n✝ = succ n✝ - 1 + 1

State before:
h : zero % 2 = 1
⊢ zero = zero - 1 + 1
Tactic:
case zero => cases h
State after:
no goals

State before:
n : Nat
h : succ n % 2 = 1
⊢ succ n = succ n - 1 + 1
Tactic:
case succ n => rfl
State after:
no goals

State before:
h : zero % 2 = 1
⊢ zero = zero - 1 + 1
Tactic:
cases h
State after:
no goals

State before:
n : Nat
h : succ n % 2 = 1
⊢ succ n = succ n - 1 + 1
Tactic:
rfl
State after:
no goals