perf: speed up kernel typechecking of mathlib's slowest declarations

[kbuzzard]

This PR golfs 14 of the 20 declarations in mathlib which are slowest to typecheck in the kernel. In every case (at least in all the ones I've checked) there was some kind of defeq abuse going on which the elaborator is quick to accept but which the kernel doesn't like, typically resulting in the unfolding of a large amount of stuff.

This is WIP for now because an LLM wrote all the code (including a bunch of comments) and I have not yet read it myself to check that the comments are accurate.

[github-actions]

PR summary cded8f6afd

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ GradedAlgebra.lift_ι_eq_aux
+ restrictDomain_arrowCongr_apply
+ strictMono_valueGroupEquiv

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

• +1 new declarations
• −0 removed declarations

+IsDedekindDomain.HeightOneSpectrum.adicCompletion.strictMono_valueGroupEquiv

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit cded8f6afd
Reference commit b86f7b9ebe

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

[kbuzzard]

!radar

[leanprover-radar]

Benchmark results for cded8f6 against b86f7b9 are in. There are significant results. @kbuzzard

• ✅ build//instructions: -141.0G (-0.09%)

Large changes (5✅)

• ✅ build/module/Mathlib.Algebra.Category.ModuleCat.Presheaf.PushforwardZeroMonoidal//instructions: -74.0G (-68.07%)
• ✅ build/module/Mathlib.Condensed.Light.Sequence//instructions: -34.8G (-42.09%)
• ✅ build/module/Mathlib.FieldTheory.CardinalEmb//instructions: -23.9G (-23.72%)
• ✅ build/module/Mathlib.LinearAlgebra.CliffordAlgebra.Grading//instructions: -18.8G (-49.40%)
• ✅ build/module/Mathlib.RingTheory.DedekindDomain.AdicValuation//instructions: -49.8G (-30.81%)

Medium changes (4✅)

• ✅ build/module/Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous//instructions: -21.7G (-16.62%)
• ✅ build/module/Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed//instructions: -5.7G (-28.38%)
• ✅ build/module/Mathlib.Analysis.InnerProductSpace.Adjoint//instructions: -22.2G (-9.20%)
• ✅ build/module/Mathlib.RingTheory.Etale.Field//instructions: -8.1G (-18.51%)

Small changes (1✅)

• ✅ build/module/Mathlib.AlgebraicGeometry.AffineTransitionLimit//instructions: -11.5G (-4.90%)

[kbuzzard]

I doubt it says that!