feat: "port" Rbmap and Rbtree files (#5504)

Cf. [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib4.20porting.20meeting.20series/near/369848971). Incorporates #5479.



Co-authored-by: Johan Commelin <johan@commelin.net>

Mathlib.lean

@@ -1637,6 +1637,15 @@ import Mathlib.Data.Rat.NNRat
 import Mathlib.Data.Rat.Order
 import Mathlib.Data.Rat.Sqrt
 import Mathlib.Data.Rat.Star
+import Mathlib.Data.Rbmap.Basic
+import Mathlib.Data.Rbmap.Default
+import Mathlib.Data.Rbtree.Basic
+import Mathlib.Data.Rbtree.DefaultLt
+import Mathlib.Data.Rbtree.Find
+import Mathlib.Data.Rbtree.Init
+import Mathlib.Data.Rbtree.Insert
+import Mathlib.Data.Rbtree.Main
+import Mathlib.Data.Rbtree.MinMax
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Real.Cardinality
 import Mathlib.Data.Real.CauSeq

Mathlib/Data/Rbmap/Basic.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+
+! This file was ported from Lean 3 source module data.rbmap.basic
+! leanprover-community/mathlib commit d13b3a4a392ea7273dfa4727dbd1892e26cfd518
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+
+/-!
+# Porting note: essentially already ported to std4
+
+https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib4.20porting.20meeting.20series/near/369848971
+
+-/

Mathlib/Data/Rbmap/Default.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+
+! This file was ported from Lean 3 source module data.rbmap.default
+! leanprover-community/mathlib commit 70fd9563a21e7b963887c9360bd29b2393e6225a
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+
+/-!
+# Porting note: essentially already ported to std4
+
+https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib4.20porting.20meeting.20series/near/369848971
+
+-/

Mathlib/Data/Rbtree/Basic.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+
+! This file was ported from Lean 3 source module data.rbtree.basic
+! leanprover-community/mathlib commit 5cb17dd1617d2dc55eb17777c3dcded3306fadb5
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+
+/-!
+# Porting note: essentially already ported to std4
+
+https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib4.20porting.20meeting.20series/near/369848971
+
+-/

Mathlib/Data/Rbtree/DefaultLt.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+
+! This file was ported from Lean 3 source module data.rbtree.default_lt
+! leanprover-community/mathlib commit fcc158e986d4896605e97fb3ad17d5cfed49a242
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+
+/-!
+# Porting note: essentially already ported to std4
+
+https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib4.20porting.20meeting.20series/near/369848971
+
+-/

Mathlib/Data/Rbtree/Find.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+
+! This file was ported from Lean 3 source module data.rbtree.find
+! leanprover-community/mathlib commit 8f6fd1b69096c6a587f745d354306c0d46396915
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+
+/-!
+# Porting note: essentially already ported to std4
+
+https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib4.20porting.20meeting.20series/near/369848971
+
+-/

Mathlib/Data/Rbtree/Init.lean

@@ -0,0 +1,76 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+
+! This file was ported from Lean 3 source module data.rbtree.init
+! leanprover-community/mathlib commit fcc158e986d4896605e97fb3ad17d5cfed49a242
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Init.Align
+import Std.Data.RBMap.Basic
+
+/-!
+
+# Align statements for RBTree
+
+Porting note: essentially already ported to std4
+
+https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib4.20porting.20meeting.20series/near/369848971
+
+-/
+
+#align rbnode Std.RBNode
+#align rbnode.color Std.RBColor
+#noalign rbnode.color.decidable_eq
+#align rbnode.depth Std.RBNode.depth
+#align rbnode.min Std.RBNode.min
+#align rbnode.max Std.RBNode.max
+#align rbnode.fold Std.RBNode.fold
+
+#noalign rbnode.rev_fold
+
+#align rbnode.balance1 Std.RBNode.balance1
+
+#noalign rbnode.balance1_node
+
+#align rbnode.balance2 Std.RBNode.balance2
+
+#noalign rbnode.balance2_node
+
+#noalign rbnode.get_color
+
+#align rbnode.ins Std.RBNode.ins
+
+#noalign rbnode.mk_insert_result
+
+#align rbnode.insert Std.RBNode.insert
+#align rbnode.mem Std.RBNode.Mem
+
+#noalign rbnode.mem_exact
+
+#align rbnode.find Std.RBNode.find?
+#align rbnode.well_formed Std.RBNode.WF
+
+#align rbtree Std.RBSet
+#align mk_rbtree Std.mkRBSet
+#align rbtree.mem Std.RBSet.Mem
+
+#noalign rbtree.mem_exact
+#noalign rbtree.depth
+
+#align rbtree.fold Std.RBSet.foldl
+
+#noalign rbtree.rev_fold
+
+#align rbtree.empty Std.RBSet.empty
+#align rbtree.to_list Std.RBSet.toList
+#align rbtree.min Std.RBSet.min
+#align rbtree.max Std.RBSet.max
+#align rbtree.insert Std.RBSet.insert
+#align rbtree.find Std.RBSet.find?
+#align rbtree.contains Std.RBSet.contains
+#align rbtree.from_list Std.RBSet.ofList
+
+#noalign rbtree_of

Mathlib/Data/Rbtree/Insert.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+
+! This file was ported from Lean 3 source module data.rbtree.insert
+! leanprover-community/mathlib commit 4d4167104581a21259f7f448e1972a63a4546be7
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+
+/-!
+# Porting note: essentially already ported to std4
+
+https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib4.20porting.20meeting.20series/near/369848971
+
+-/

Mathlib/Data/Rbtree/Main.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+
+! This file was ported from Lean 3 source module data.rbtree.main
+! leanprover-community/mathlib commit 4d4167104581a21259f7f448e1972a63a4546be7
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+
+/-!
+# Porting note: essentially already ported to std4
+
+https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib4.20porting.20meeting.20series/near/369848971
+
+-/

Mathlib/Data/Rbtree/MinMax.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+
+! This file was ported from Lean 3 source module data.rbtree.min_max
+! leanprover-community/mathlib commit 8f6fd1b69096c6a587f745d354306c0d46396915
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+
+/-!
+# Porting note: essentially already ported to std4
+
+https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib4.20porting.20meeting.20series/near/369848971
+
+-/