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

State before:
n : Nat
⊢ n ^^^ 0 = n
Tactic:
apply bitext
State after:
case a
n : Nat
⊢ ∀ (i : Nat), getBit (n ^^^ 0) i = getBit n i

State before:
case a
n : Nat
⊢ ∀ (i : Nat), getBit (n ^^^ 0) i = getBit n i
Tactic:
intro i
State after:
case a
n i : Nat
⊢ getBit (n ^^^ 0) i = getBit n i

State before:
case a
n i : Nat
⊢ getBit (n ^^^ 0) i = getBit n i
Tactic:
conv =>
  change (bitwise bne n 0).getBit i = n.getBit i
  rw [Nat.bitwise_getBit, Nat.zero_getBit]
State after:
case a
n i : Nat
⊢ (getBit n i != false) = getBit n i

State before:
case a
n i : Nat
⊢ (getBit n i != false) = getBit n i
Tactic:
cases n.getBit i <;> decide
State after:
no goals