test: remove universe metavariables in variables

[robin-carlier]

LLM-generated on the warnings generated by the linter from #42519. This is mainly an experiment to see if there is a performance improvement possible by removing these. I don’t trust the full diff to have 0 monomorphization, please don’t bother reviewing this.

---

[robin-carlier]

!radar

[leanprover-radar]

Benchmark results for 4b4fd21 against 9d302fc are in. There are significant results. @robin-carlier

• ✅ build//instructions: -317.0G (-0.22%)

Large changes (2✅)

• ✅ build/module/Mathlib.Algebra.Category.ModuleCat.Stalk//instructions: -24.3G (-40.87%)
• and 1 hidden

Medium changes (14✅)

• ✅ build/module/Mathlib.Algebra.Module.FinitePresentation//instructions: -6.5G (-7.48%)
• ✅ build/module/Mathlib.Algebra.Polynomial.Module.AEval//instructions: -6.8G (-19.60%)
• ✅ build/module/Mathlib.AlgebraicGeometry.ColimitsOver//instructions: -9.4G (-17.23%)
• ✅ build/module/Mathlib.AlgebraicGeometry.Cover.Directed//instructions: -4.4G (-16.11%)
• ✅ build/module/Mathlib.AlgebraicGeometry.Cover.Over//instructions: -3.7G (-16.27%)
• ✅ build/module/Mathlib.CategoryTheory.FiberedCategory.Grothendieck//instructions: -1.9G (-14.72%)
• ✅ build/module/Mathlib.CategoryTheory.GradedObject.Trifunctor//instructions: -6.5G (-12.50%)
• ✅ build/module/Mathlib.CategoryTheory.Limits.Shapes.Grothendieck//instructions: -3.2G (-17.93%)
• ✅ build/module/Mathlib.CategoryTheory.Shift.Induced//instructions: -3.2G (-18.83%)
• ✅ build/module/Mathlib.Geometry.RingedSpace.OpenImmersion//instructions: -16.4G (-17.94%)
• ✅ build/module/Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree//instructions: -7.0G (-13.86%)
• ✅ build/module/Mathlib.RingTheory.DedekindDomain.Different//instructions: -24.8G (-7.21%)
• ✅ build/module/Mathlib.RingTheory.QuotSMulTop//instructions: -3.2G (-14.14%)
• ✅ build/module/Mathlib.RingTheory.Spectrum.Prime.Polynomial//instructions: -4.8G (-15.05%)

Small changes (16✅, 1🟥)

• ✅ build/module/Mathlib.Algebra.Homology.ModelCategory.Injective//instructions: -1.1G (-6.86%)
• 🟥 build/module/Mathlib.Algebra.Homology.SpectralObject.Basic//instructions: +1.8G (+7.28%)
• ✅ build/module/Mathlib.AlgebraicGeometry.ResidueField//instructions: -1.3G (-5.57%)
• ✅ build/module/Mathlib.CategoryTheory.Bicategory.CatEnriched//instructions: -1.3G (-5.58%)
• ✅ build/module/Mathlib.CategoryTheory.Bicategory.InducedBicategory//instructions: -1.1G (-6.92%)
• ✅ build/module/Mathlib.CategoryTheory.Limits.Final//instructions: -1.4G (-2.64%)
• ✅ build/module/Mathlib.CategoryTheory.Monoidal.Cartesian.GrpLimits//instructions: -780.2M (-10.40%)
• ✅ build/module/Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory//instructions: -554.8M (-7.85%)
• ✅ build/module/Mathlib.CategoryTheory.Triangulated.SpectralObject//instructions: -2.1G (-7.72%)
• ✅ build/module/Mathlib.FieldTheory.IntermediateField.Basic//instructions: -2.0G (-3.82%)
• ✅ build/module/Mathlib.Geometry.RingedSpace.PresheafedSpace//instructions: -2.7G (-6.68%)
• ✅ build/module/Mathlib.LinearAlgebra.BilinearForm.DualLattice//instructions: -1.4G (-10.33%)
• ✅ build/module/Mathlib.ModelTheory.DirectLimit//instructions: -1.4G (-5.95%)
• ✅ build/module/Mathlib.Order.Interval.Lex//instructions: -707.2M (-13.43%)
• ✅ build/module/Mathlib.RepresentationTheory.Homological.FiniteCyclic//instructions: -1.2G (-4.62%)
• ✅ build/module/Mathlib.RingTheory.Extension.Basic//instructions: -2.0G (-3.55%)
• ✅ build/module/Mathlib.RingTheory.Extension.Generators//instructions: -2.7G (-4.57%)

[github-actions]

PR summary 4b4fd2193f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

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

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.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 4b4fd21).

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 4b4fd2193f
Reference commit 9d302fc708

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

[robin-carlier]

To compare, #32842 removed 1.2T instruction by switching Category to Category*, this one is much less dramatic apparently so categories were the real hot spot for this kind of improvements.