Theorem: Nat.lor_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 or m n).getBit i; rw [bitwise_getBit]
State after:
no goals