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

State before:
m n : Nat
⊢ m + n = (m ^^^ n) + (m &&& n) <<< 1
Tactic:
conv =>
  lhs; congr
  . rw [bitdivide m n]
  . rw [bitdivide n m]
State after:
m n : Nat
⊢ (m ^^^ m &&& n) + (m &&& n) + ((n ^^^ n &&& m) + (n &&& m)) = (m ^^^ n) + (m &&& n) <<< 1

State before:
m n : Nat
⊢ (m ^^^ m &&& n) + (m &&& n) + ((n ^^^ n &&& m) + (n &&& m)) = (m ^^^ n) + (m &&& n) <<< 1
Tactic:
conv =>
  lhs; rw [Nat.land_comm n m]
  rw [Nat.add_assoc, ←Nat.add_assoc (m &&& n), Nat.add_comm (m &&& n), Nat.add_assoc]
  rw [←Nat.two_mul, ←Nat.add_assoc]
  change (m ^^^ (m &&& n)) + (n ^^^ (m &&& n)) + ((m &&& n) <<< 1)
  rw [setminus_add_setminus]
State after:
no goals