Theorem: Nat.bit0_xor_bit1 (Extra/Nat/Bitwise.lean)

State before:
x y : Nat
⊢ 2 * x ^^^ 2 * y + 1 = 2 * (x ^^^ y) + 1
Tactic:
simp [xor_def, bit0_bitwise_bit1]
State after:
no goals