Auto-port missing `noindex!` annotations

[dselsam]

Here is one example:

import Lean3Lib.init.data.list.basic

namespace Mathlib

-- Fails to simplify
theorem nthOne : list.nth [1, 2] 1 = some 2 := by simp

@[simp]
theorem Mathlib.list.nth.equations._eqn_3_alt {α : Type} (x : α) (l : List α) (n : Nat)
: list.nth (x :: l) (noindex! (n + 1)) = list.nth l n :=
  rfl

-- Works
theorem nthOneAlt : list.nth [1, 2] 1 = some 2 := by simp

end Mathlib

It is easy to detect a particular pattern and to always wrap it with noindex!. The issue is which patterns to do this for, and in what contexts to do it. Since [simp] can be toggled after-the-fact, presumably we need to translate all theorem types.

[dselsam]

Examples of other indexing issues (besides (n + <offset>)) would be very helpful. Please post here if you stumble on one.

[dselsam]

Leo added offset support: https://github.com/leanprover/lean4/commit/cc0712fc827fb0e60b0e00c875aaf2a715455c47

I'll keep this issue open for now to encourage reporting other problematic examples.