`native.rb_map.insert` not working as expected

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Inserting to an rb_map is not working as expected:

import init.meta
import order.basic

-- evaluates to [(4, 5), (2, 3)] as expected
#eval (((native.rb_map.of_list ([] : list (ℕ × ℕ))).insert 2 3).insert 4 5).to_list

-- evaluates to [(tt, 3), (ff, 5)] as expected
#eval (((native.rb_map.of_list ([] : list (bool × ℕ))).insert tt 3).insert ff 5).to_list

-- evaluates to [((ff, 4), 5)] instead of  [((tt, 2), 3), ((ff, 4), 5)]
#eval (((native.rb_map.of_list ([] : list ((bool × ℕ) × ℕ ))).insert (tt,2) 3).insert (ff,4) 5).to_list

Steps to Reproduce

1. This can be easily reproduced in gitpod with the latest mathlib.

Expected behavior: expression evaluates to [((tt, 2), 3), ((ff, 4), 5)]

Actual behavior: expression evaluates to [((ff, 4), 5)]

Reproduces how often: always

Versions

• On gitpod: Lean (version 3.44.1, commit 9d5adc6ab80d, Release) and mathlib 861589f224456f278c61596c0ee8a1ba449a6e8b

• On my PC (Ubuntu 20.04) Lean (version 3.42.1, commit 68455b087d87, Release)

Reproduce the three #eval examples for native.rb_map.of_list, insert, and to_list, confirming that nested tuple keys lose the first entry. Then locate the native.rb_map implementation and trace comparison and insertion for nested keys. Done means the expected two-entry result is produced while the other examples remain correct.