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

State before:
x y : Nat
⊢ 2 * x &&& 2 * y = 2 * (x &&& y)
Tactic:
if x = 0 then
  simp [*, and_def]
else if y = 0 then
  simp [*, and_def]
else
  simp [*, and_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 [*, and_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 [*, and_def]
else
simp [*, and_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 [*, and_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 [*, and_def, bit0_bitwise_bit0]
State after:
no goals