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

State before:
m n : Nat
⊢ (m + n) / 2 = m / 2 + n / 2 + if getBit (m &&& n) 0 = true then 1 else 0
Tactic:
conv =>
  lhs; rw [←m.div_add_mod 2, ←n.div_add_mod 2]
  rw [←Nat.add_assoc, Nat.add_assoc _ (m%2), Nat.add_comm (m%2), ←Nat.add_assoc]
  rw [←Nat.mul_add 2, Nat.add_assoc, Nat.mul_add_div_left (x:=2) (y:=m/2+n/2) (z:=m%2+n%2) (by decide)]
State after:
m n : Nat
⊢ m / 2 + n / 2 + (m % 2 + n % 2) / 2 = m / 2 + n / 2 + if getBit (m &&& n) 0 = true then 1 else 0

State before:
m n : Nat
⊢ m / 2 + n / 2 + (m % 2 + n % 2) / 2 = m / 2 + n / 2 + if getBit (m &&& n) 0 = true then 1 else 0
Tactic:
apply congrArg
State after:
case h
m n : Nat
⊢ (m % 2 + n % 2) / 2 = if getBit (m &&& n) 0 = true then 1 else 0

State before:
case h
m n : Nat
⊢ (m % 2 + n % 2) / 2 = if getBit (m &&& n) 0 = true then 1 else 0
Tactic:
conv =>
  rhs; change if (bitwise and m n).getBit 0 = true then 1 else 0
  rw [bitwise_getBit and (by decide)]
State after:
case h
m n : Nat
⊢ (m % 2 + n % 2) / 2 = if (getBit m 0 && getBit n 0) = true then 1 else 0

State before:
case h
m n : Nat
⊢ (m % 2 + n % 2) / 2 = if (getBit m 0 && getBit n 0) = true then 1 else 0
Tactic:
unfold getBit
State after:
case h
m n : Nat
⊢ (m % 2 + n % 2) / 2 = if (decide (m % 2 = 1) && decide (n % 2 = 1)) = true then 1 else 0

State before:
case h
m n : Nat
⊢ (m % 2 + n % 2) / 2 = if (decide (m % 2 = 1) && decide (n % 2 = 1)) = true then 1 else 0
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
⊢ 2 > 0
Tactic:
decide
State after:
no goals

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

State before:
case h.right.right
m n : Nat
⊢ n % 2 = 1 → m % 2 = 1 → (m % 2 + n % 2) / 2 = if (decide (m % 2 = 1) && decide (n % 2 = 1)) = true then 1 else 0
Tactic:
intro hn hm
State after:
case h.right.right
m n : Nat
hn : n % 2 = 1
hm : m % 2 = 1
⊢ (m % 2 + n % 2) / 2 = if (decide (m % 2 = 1) && decide (n % 2 = 1)) = true then 1 else 0

State before:
case h.right.right
m n : Nat
hn : n % 2 = 1
hm : m % 2 = 1
⊢ (m % 2 + n % 2) / 2 = if (decide (m % 2 = 1) && decide (n % 2 = 1)) = true then 1 else 0
Tactic:
rw [hn, hm]
State after:
case h.right.right
m n : Nat
hn : n % 2 = 1
hm : m % 2 = 1
⊢ (1 + 1) / 2 = if (decide (1 = 1) && decide (1 = 1)) = true then 1 else 0

State before:
case h.right.right
m n : Nat
hn : n % 2 = 1
hm : m % 2 = 1
⊢ (1 + 1) / 2 = if (decide (1 = 1) && decide (1 = 1)) = true then 1 else 0
Tactic:
decide
State after:
no goals