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

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

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

State before:
case a
n i : Nat
⊢ getBit (n &&& 0) i = getBit 0 i
Tactic:
conv =>
  change (bitwise and n 0).getBit i = getBit 0 i
  rw [bitwise_getBit, zero_getBit, Bool.and_false]
State after:
no goals