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

State before:
x y : Nat
⊢ 2 * x ^^^ 2 * y = 2 * (x ^^^ y)
Tactic:
if x = 0 then
  simp [*, xor_def]
else if y = 0 then
  simp [*, xor_def]
else
  simp [*, xor_def, bit0_bitwise_bit0]
State after:
no goals

State before:
x y : Nat
h✝ : x = 0
⊢ 2 * x ^^^ 2 * y = 2 * (x ^^^ y)
Tactic:
simp [*, xor_def]
State after:
no goals

State before:
x y : Nat
h✝ : ¬x = 0
⊢ 2 * x ^^^ 2 * y = 2 * (x ^^^ y)
Tactic:
if y = 0 then
simp [*, xor_def]
else
simp [*, xor_def, bit0_bitwise_bit0]
State after:
no goals

State before:
x y : Nat
h✝¹ : ¬x = 0
h✝ : y = 0
⊢ 2 * x ^^^ 2 * y = 2 * (x ^^^ y)
Tactic:
simp [*, xor_def]
State after:
no goals

State before:
x y : Nat
h✝¹ : ¬x = 0
h✝ : ¬y = 0
⊢ 2 * x ^^^ 2 * y = 2 * (x ^^^ y)
Tactic:
simp [*, xor_def, bit0_bitwise_bit0]
State after:
no goals