[Merged by Bors] - chore(Analysis/Convex/Approximation): reuse sSup_of_nat_affine_eq

[yuanyi-350]

This PR shortens the proof of univ_sSup_of_nat_affine_eq by applying the already available theorem sSup_of_nat_affine_eq to s = univ. This removes the ad hoc split on whether the family is empty, and reuses the more general result instead.

This is extracted from #37968.

[github-actions]

PR summary 1a3500f1bf

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[grunweg]

Can you also comment on the performance of this change? Thanks!

[yuanyi-350]

!bench

[leanprover-radar]

Benchmark results for c33ff46 against 1a3500f are in. No significant results found. @yuanyi-350

• 🟥 build//instructions: +20.0G (+0.01%)

Small changes (1✅, 2🟥)

• ✅ build/module/Mathlib.Analysis.Convex.Approximation//instructions: -1.3G (-2.03%)
• 🟥 build/module/Mathlib.CategoryTheory.Limits.Types.Coequalizers//instructions: +393.1M (+6.55%)
• 🟥 build/module/Mathlib.Lean.Elab.InfoTree//instructions: +125.6M (+4.95%)

[themathqueen]

Thanks. I think this is fine.

[yuanyi-350]

I ran a profiler comparison for the changed declaration in this PR.

Results ([Elab.definition.value], seconds, 2 runs each):

• ConvexOn.univ_sSup_of_nat_affine_eq: first run 12.494 -> 2.607, second run 11.902 -> 3.203; average 12.198 -> 2.905 (-76.2%).

Overall:

• This change is a clear speedup for ConvexOn.univ_sSup_of_nat_affine_eq; both runs were about 4x faster on the PR head.

Caveat:

• The measurements were taken in isolated worktrees for the PR head and the merge-base (1a3500f1bf47ea7a2be35118599b5e5ec828b576), but they reused the current checkout's existing dependency .oleans via LEAN_PATH instead of rebuilding the full dependency graph inside each temporary worktree.

[grunweg]

Thanks!
bors merge

[grunweg]

As side note, 12 seconds for a single declaration is very slow --- this is suspicious (but unrelated to this PR).

[themathqueen]

As side note, 12 seconds for a single declaration is very slow --- this is suspicious (but unrelated to this PR).

There is absolutely no way that takes 12 seconds (unless I'm misunderstanding something). It compiles almost instantly on the web editor. Could it be that they meant 0.12?

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-Build Step
• ci (staging) / Build
• ci (staging) / Lint style
• ci (staging) / Post-CI job

[grunweg]

As side note, 12 seconds for a single declaration is very slow --- this is suspicious (but unrelated to this PR).

There is absolutely no way that takes 12 seconds (unless I'm misunderstanding something). It compiles almost instantly on the web editor. Could it be that they meant 0.12?

I disagree: running this locally in VS Code, I see the orange bars disappear quickly except on the declaration itself --- i.e., it is kernel checking which is taking so long. This takes several seconds on my computer, so 12 seconds seems possible.