feat: conv arg now can access more arguments

[kmill]

Specializes the congr lemma generated for the arg conv tactic to only rewrite the chosen argument. This makes it much more likely that the chosen argument is able to be accessed.

Lets arg access the domain and codomain of pi types via arg 1 and arg 2 in more situations. Upstreams pi_congr for this from mathlib.

Adds a negative indexing option, where arg -2 accesses the second-to-last argument for example, making the behavior of lhs available to arg. This works for enter as well.

Other improvement: when there is an error in the enter [...] tactic, individual locations get underlined with the error. The tactic info now also is like rw, so you can see the intermediate conv states.

Closes #5871

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-5894 build failed against this PR. (2024-10-31 07:21:25) View Log
• ✅ Mathlib branch lean-pr-testing-5894 has successfully built against this PR. (2024-10-31 08:04:56) View Log
• ✅ Mathlib branch lean-pr-testing-5894 has successfully built against this PR. (2024-10-31 17:12:02) View Log
• ✅ Mathlib branch lean-pr-testing-5894 has successfully built against this PR. (2024-10-31 21:29:21) View Log
• 💥 Mathlib branch lean-pr-testing-5894 build failed against this PR. (2024-11-01 00:40:39) View Log
• ✅ Mathlib branch lean-pr-testing-5894 has successfully built against this PR. (2024-11-01 01:37:57) View Log