fix: do not ban `..` with a `.` on the next line

[eric-wieser]

Without this change,

example : True := by
  refine' trivial ..
  . trivial

is a parse error.

Read this section before submitting

• Ensure your PR follows the External Contribution Guidelines.
• Please make sure the PR has excellent documentation and tests. If we label it missing documentation or missing tests then it needs fixing!
• Include the link to your RFC or bug issue in the description.
• If the issue does not already have approval from a developer, submit the PR as draft.
• The PR title/description will become the commit message. Keep it up-to-date as the PR evolves.
• If you rebase your PR onto nightly-with-mathlib then CI will test Mathlib against your PR.
• You can manage the awaiting-review, awaiting-author, and WIP labels yourself, by writing a comment containing one of these labels on its own line.
• Remove this section, up to and including the --- before submitting.

---

Closes #0000 (RFC or bug issue number fixed by this PR, if any)

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1a12f63f742a578a514536ef45cf9df0c9793af0 --onto 7aec6c9ae7a54935ada0df0b4cc1efafc2291007. (2024-07-17 01:32:53)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1a12f63f742a578a514536ef45cf9df0c9793af0 --onto 647a5e94925791f6a16b629b6c16ffad60a7f478. (2024-08-05 21:35:26)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1a12f63f742a578a514536ef45cf9df0c9793af0 --onto 9ce15fb0c61e3a1bee17fd81647ed4d02b4f6c6d. (2024-08-29 22:47:38)

[Kha]

Why is this a draft?

[eric-wieser]

It has no tests yet and the description implies it should be draft if I haven't filed an issue first.

[eric-wieser]

I've added the test from the description

[Kha]

Thanks. Please add a module docstring to the test describing its purpose as mentioned in testing.md

[eric-wieser]

Sorry for the delay, the docstring is now present.