chore(RepresentationTheory/FiniteIndex): generalize universes

[Whysoserioushah]

---

[github-actions]

PR summary d0376242cf

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).

[riccardobrasca]

!radar

[leanprover-radar]

Benchmark results for 26b3d4a against 55b0702 are in. Significant changes detected! @riccardobrasca @robin-carlier

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

Large changes (1🟥)

• 🟥 build/module/Mathlib.RepresentationTheory.FiniteIndex//instructions: +30.2G (+53.92%)

Small changes (1✅)

• ✅ build/module/Mathlib.RingTheory.TwoSidedIdeal.Kernel//instructions: -615.3M (-9.45%)

[Whysoserioushah]

!radar

[leanprover-radar]

Benchmark results for b92e1d0 against 9f0aee2 are in. Significant changes detected! @Whysoserioushah

• 🟥 build//instructions: +32.0G (+0.02%)

Large changes (1🟥)

• 🟥 build/module/Mathlib.RepresentationTheory.FiniteIndex//instructions: +30.5G (+54.57%)

[riccardobrasca]

The biggest slowdown seems to be in resIndAdjunction_unit_app. Looking at the trace I still see

[Meta.isDefEq] [17940362.000000] ❌️ (𝟭 (Rep.{max ?u.140033 u v, u, v} k G)).obj B ⟶
              (resFunctor S.subtype ⋙ indFunctor k S.subtype).obj
                B =?= (𝟭 (Rep.{max v w u, u, v} k G)).obj B ⟶ ind S.subtype (res S.subtype B)

Can we get rid of universe 140033?

[riccardobrasca]

!radar

[riccardobrasca]

I gave a try, let's see.

[leanprover-radar]

Benchmark results for 2bd7083 against d037624 are in. Significant changes detected! @riccardobrasca

• 🟥 main exited with code 1

No significant changes detected.