chore: bump lean and mathlib to 4.15.0

[mpenciak]

This PR bumps Lean to toolchain version 4.15.0 and correspondingly pins Mathlib to v4.15.0-patch1. Most required updates were largely mechanical.

The main changes this entails are:

• Mathlib.Vector has been renamed to List.Vector
• List, Array, and Vector deprecating versions of getNth
• TacticM no longer automatically lifts Options? I needed to add a bunch of liftOptions to Tactic.SeparationLogic
• tauto has always been a finishing tactic, and the instances of non-finishing tauto were not being flagged in 4.12.0 for some reason. A simple fix was to replace tauto -> try tauto, but maybe a more principled approach is worth exploring.
• rfl doesn't see through decomposeToRadix anymore for some reason? There's a few ways to make the examples in the Builtin.Helpers file, and depending on the importance of the change it may be worth thinking about.

Things that need to be done before this is mergeable:

• Decide on the fate of @[reducible] for decomposeToRadix
• rebase on Extractor improvements #24 and Minimize Mathlib imports #31

[utkn]

Looks good to me! :)