chore: extract API from #38807 and golf

[bryangingechen]

I wanted to understand why these two proofs in #38807 were long (and also play around more with the API in this corner of the library) so I walked through them with Claude Opus.

prepared with Claude code

[github-actions]

PR summary 45f0cc9e9b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ IsCofinalFor.nonempty
+ IsLUB.of_isCofinalFor

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[vihdzp]

Thanks for this! I suspected my proofs were more complicated than they needed to be. I'll take a closer look tomorrow morning.

[vihdzp]

Neat! I can't say I fully understand the new proofs but I can't find ways to golf them further.