feat: RBMap lemmas cont'd: find?_erase

Std/Data/RBMap/Basic.lean

@@ -689,14 +689,7 @@ are not of this form as long as they are suitably monotonic.)
 @[inline] def eraseP (t : RBSet α cmp) (cut : α → Ordering) : RBSet α cmp :=
   ⟨t.1.erase cut, t.2.erase⟩
 
-/--
-`O(log n)`. Remove an element from the tree using a cut function.
-The `cut` function is used to locate an element in the tree:
-it returns `.gt` if we go too high and `.lt` if we go too low;
-if it returns `.eq` we will remove the element.
-(The function `cmp k` for some key `k` is a valid cut function, but we can also use cuts that
-are not of this form as long as they are suitably monotonic.)
--/
+/-- `O(log n)`. Remove element `x` from the tree, if present. -/
 @[inline] def erase (t : RBSet α cmp) (x : α) : RBSet α cmp := t.eraseP (cmp x)
 
 /-- `O(log n)`. Find an element in the tree using a cut function. -/