Binary Search Trees in Lean 4 with proofs

This is part of the Lean 4 manual, an example of using Lean to define BSTs and guarantee inorder key insertion with formal proofs.

The implementation is quite idiomatic Lean with constructs ranging from simple `def` and `inductive` to elaborate tactics macros.

The proofs of the theorems can be quite hard to follow if you are not familiar with Lean's proof system, but it is still worth glancing to get a feel for them.