feat: Add getElem_swapIfInBounds* lemmas and deprecate getElem_swap'

[linesthatinterlace]

This PR adds lemmas of the form getElem_swapIfInBounds* and deprecates getElem_swap'.

[linesthatinterlace]

changelog-library

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f40d72ea4795561b7e656898482ca022bf013d0f --onto efe2ab4c04e81fe2a3edcc0d861449490b4431b2. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-19 17:18:56)

[linesthatinterlace]

The alternative incidentally would be something like:

theorem getElem_swapIfInBounds {as : Array α} {i j k : ℕ} (hk : k < (as.swapIfInBounds i j).size) :
    (as.swapIfInBounds i j)[k] =
    if h : i < as.size ∧ j < as.size then (as.swap i j)[k]'
      (hk.trans_eq ((as.size_swapIfInBounds).trans (as.size_swap).symm))
    else as[k]'(hk.trans_eq as.size_swapIfInBounds) := by
  unfold swapIfInBounds
  split
  · split <;> simp_all
  · simp_all

I think this is a more compact form but it will generally result in more rewrites. There are places where this is what you'd want though.