fix: Incorrect promotion from index to paramater

[arthur-adjedj]

Depends on #3590

Closes #3458

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-3591 has successfully built against this PR. (2024-03-04 12:38:08) View Log
• 🟡 Mathlib branch lean-pr-testing-3591 build against this PR was cancelled. (2024-03-04 13:13:11) View Log
• ✅ Mathlib branch lean-pr-testing-3591 has successfully built against this PR. (2024-03-04 14:19:23) View Log
• ✅ Mathlib branch lean-pr-testing-3591 has successfully built against this PR. (2024-03-04 19:46:23) View Log
• ✅ Mathlib branch lean-pr-testing-3591 has successfully built against this PR. (2024-03-07 19:09:05) View Log
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 605cecdde33e2ae84dec5653af4d8f9bc2649b17 --onto 62cdb51ed5b9d8487877d5a4adbcd4659d81fc6a. (2024-04-24 20:35:06)

[kim-em]

@arthur-adjedj, I've sent #3590 to the merge queue now. Please ping me when this one is ready to go.

[arthur-adjedj]

@semorrison This PR is in a ready state. My only worry is that the added condition to visit might be a bit costly, since the function is called frequently in other places. If that was the case, it might be better to make another function entirely for the stopWhenVisited := true case. Could this warrant a !bench ?

[kim-em]

!bench

[leanprover-bot]

Here are the benchmark results for commit 19a9de41505364f54e6cdec6cd4f2bfbee1c4a87. There were no significant changes against commit 49f41a6224a489793eb9a75ac3626d1f5049a06f.

[kim-em]

Sorry it took a while to get back to this.