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

State before:
m n : Nat
⊢ (m ^^^ m &&& n) + (n ^^^ m &&& n) = m ^^^ n
Tactic:
rw [add_eq_xor (setminus_land_setminus m n)]
State after:
m n : Nat
⊢ m ^^^ m &&& n ^^^ (n ^^^ m &&& n) = m ^^^ n

State before:
m n : Nat
⊢ m ^^^ m &&& n ^^^ (n ^^^ m &&& n) = m ^^^ n
Tactic:
rw [Nat.xor_assoc, ←Nat.xor_assoc (m &&& n), Nat.xor_comm (m &&& n), Nat.xor_assoc]
State after:
m n : Nat
⊢ m ^^^ (n ^^^ (m &&& n ^^^ m &&& n)) = m ^^^ n

State before:
m n : Nat
⊢ m ^^^ (n ^^^ (m &&& n ^^^ m &&& n)) = m ^^^ n
Tactic:
simp
State after:
no goals