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

State before:
n : Nat
⊢ n ^^^ 1 = if n % 2 = 1 then n - 1 else n + 1
Tactic:
cases n.mod_two_eq_zero_or_one
State after:
case inl
n : Nat
h✝ : n % 2 = 0
⊢ n ^^^ 1 = if n % 2 = 1 then n - 1 else n + 1

case inr
n : Nat
h✝ : n % 2 = 1
⊢ n ^^^ 1 = if n % 2 = 1 then n - 1 else n + 1

State before:
n : Nat
h : n % 2 = 0
⊢ n ^^^ 1 = if n % 2 = 1 then n - 1 else n + 1
Tactic:
case inl h => simp [h, n.even_xor_one h]
State after:
no goals

State before:
n : Nat
h : n % 2 = 1
⊢ n ^^^ 1 = if n % 2 = 1 then n - 1 else n + 1
Tactic:
case inr h => simp [h, n.odd_xor_one h]
State after:
no goals

State before:
n : Nat
h : n % 2 = 0
⊢ n ^^^ 1 = if n % 2 = 1 then n - 1 else n + 1
Tactic:
simp [h, n.even_xor_one h]
State after:
no goals

State before:
n : Nat
h : n % 2 = 1
⊢ n ^^^ 1 = if n % 2 = 1 then n - 1 else n + 1
Tactic:
simp [h, n.odd_xor_one h]
State after:
no goals