feat: rename get_elem_tactic_trivial to get_elem_tactic_extensible

[kim-em]

This PR renames the get_elem_tactic_trivial tactic (recall this is the extensibility mechanism for get_elem_tactic, which is invoked to produce a proof whenever a xs[i] term appears) to get_elem_tactic_extensible.

[kim-em]

Currently this branches off nightly-with-mathlib so we can get a Mathlib test. Before merging (manually), I'll need to rebase back onto master.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-8478 has successfully built against this PR. (2025-05-26 02:20:04) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 03e905d994a7922f7793fa8a7811c14bf4f32c2e --onto 2a1354b3cc1eb05e1b67c656d2172ada8f54a937. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-26 04:05:22)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b97d35d879324bd5aa88291287505720bbe15863 --onto 9b9dd8546a123d746580649b239f26c26d370d20. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-06 03:05:52)

[Kha]

The general idea seems perfectly fine :) . Did you want any other parts to be reviewed?

[kim-em]

Merged manually, since it requires a stage0 update.