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

State before:
m n i : Nat
⊢ getBit (m &&& n) i = (getBit m i && getBit n i)
Tactic:
conv => lhs; change (bitwise and m n).getBit i; rw [bitwise_getBit]
State after:
no goals