chore: cherry-pick stray test from #3850

[kim-em]

#3850 included a commit that added an extra test for exact?, but was otherwise unrelated the to PR. It also removed a test. I've cherry-picked that test over, and restored the deleted test, and next will remove the commit from #3850.

[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 458835360f8ca16f06a514c347dc5b0b183f3976 --onto 1cf71e54cf268e87cf5c43c830d953f5c88e6c39. (2024-06-20 01:03:39)