chore: remove FileMap.lines and add FileMap.getLine

[joneugster]

FileMap.lines is an array that seems to be manually managed to have the form #[1, 2, ..., n-1, n-1] with same length as FileMap.positions. Remove this structure field in favour of calculating the line number as min(x+1, positions.size-1) when needed.

Follow-up on #3221

[joneugster]

a) I'm a bit surprised that FileMap.lines seems not to be used anywhere else in the code.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-3237 has successfully built against this PR. (2024-02-01 14:07:59) View Log
• ✅ Mathlib branch lean-pr-testing-3237 has successfully built against this PR. (2024-02-01 14:45:56) View Log
• 🟡 Mathlib branch lean-pr-testing-3237 build this PR didn't complete normally. (2024-02-02 12:24:31) View Log

[joneugster]

@Kha if you want to review/adapt this PR you requested in #3221, please feel free to do so. Otherwise, I'll close it next week as part of cleaning up my open PRs.

[Kha]

Thanks for the reminder!