doc: expand elab_as_elim docstring and fix typo

[jrr6]

This PR adds additional information from a recent Zulip thread to the docstring for the elab_as_elim attribute and fixes the associated example code.

The Zulip thread can be found here.

[leanprover-community-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 0931033c72fea3544133ae5bd86ec9953ae77313 --onto 18a82c04fc59d3dba392308e09d65ee431240d89. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-14 17:05:25)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 0931033c72fea3544133ae5bd86ec9953ae77313 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-14 17:05:27)