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