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]
m n : Nat
⊢ (m ^^^ m &&& n) + (m &&& n) + ((n ^^^ n &&& m) + (n &&& m)) = (m ^^^ n) + (m &&& n) <<< 1
no goals