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

State before:
m n : Nat
⊢ getBit (m + n) 0 = getBit (m ^^^ n) 0
Tactic:
conv =>
  rhs; change (bitwise bne m n).getBit 0
  rw [bitwise_getBit bne (by decide)]
State after:
m n : Nat
⊢ getBit (m + n) 0 = (getBit m 0 != getBit n 0)

State before:
m n : Nat
⊢ getBit (m + n) 0 = (getBit m 0 != getBit n 0)
Tactic:
unfold getBit
State after:
m n : Nat
⊢ decide ((m + n) % 2 = 1) = (decide (m % 2 = 1) != decide (n % 2 = 1))

State before:
m n : Nat
⊢ decide ((m + n) % 2 = 1) = (decide (m % 2 = 1) != decide (n % 2 = 1))
Tactic:
rw [Nat.add_mod m n 2]
State after:
m n : Nat
⊢ decide ((m % 2 + n % 2) % 2 = 1) = (decide (m % 2 = 1) != decide (n % 2 = 1))

State before:
m n : Nat
⊢ decide ((m % 2 + n % 2) % 2 = 1) = (decide (m % 2 = 1) != decide (n % 2 = 1))
Tactic:
apply m.mod_two_eq_zero_or_one.elim
<;> apply n.mod_two_eq_zero_or_one.elim
<;> (intro hn hm; rw [hn, hm]; decide)
State after:
no goals

State before:
m n : Nat
⊢ (false != false) = false
Tactic:
decide
State after:
no goals

State before:
case right.right
m n : Nat
⊢ n % 2 = 1 → m % 2 = 1 → decide ((m % 2 + n % 2) % 2 = 1) = (decide (m % 2 = 1) != decide (n % 2 = 1))
Tactic:
intro hn hm
State after:
case right.right
m n : Nat
hn : n % 2 = 1
hm : m % 2 = 1
⊢ decide ((m % 2 + n % 2) % 2 = 1) = (decide (m % 2 = 1) != decide (n % 2 = 1))

State before:
case right.right
m n : Nat
hn : n % 2 = 1
hm : m % 2 = 1
⊢ decide ((m % 2 + n % 2) % 2 = 1) = (decide (m % 2 = 1) != decide (n % 2 = 1))
Tactic:
rw [hn, hm]
State after:
case right.right
m n : Nat
hn : n % 2 = 1
hm : m % 2 = 1
⊢ decide ((1 + 1) % 2 = 1) = (decide (1 = 1) != decide (1 = 1))

State before:
case right.right
m n : Nat
hn : n % 2 = 1
hm : m % 2 = 1
⊢ decide ((1 + 1) % 2 = 1) = (decide (1 = 1) != decide (1 = 1))
Tactic:
decide
State after:
no goals