Lean4
/-- O(log n). Modify an element in the set with the given function,
doing nothing if the key is not found.
Note that the element returned by `f` must be equivalent to `x`.
adjustWith f 0 {1, 2, 3} = {1, 2, 3}
adjustWith f 1 {1, 2, 3} = {f 1, 2, 3}
Using a preorder on `ℕ × ℕ` that only compares the first coordinate:
adjustWith f (1, 1) {(0, 1), (1, 2)} = {(0, 1), f (1, 2)}
adjustWith f (3, 1) {(0, 1), (1, 2)} = {(0, 1), (1, 2)} -/
def adjustWith (f : α → α) (x : α) : Ordnode α → Ordnode α
| nil => nil
| _t@(node sz l y r) =>
match cmpLE x y with
| Ordering.lt => node sz (adjustWith f x l) y r
| Ordering.eq => node sz l (f y) r
| Ordering.gt => node sz l y (adjustWith f x r)
