feat: multiple universe polymorphism for the equational criterion for flatness

[trivial1711]

Algebra/Module/FinitePresentation.lean is now fully universe polymorphic. This had the side effect of somehow breaking RingTheory/Flat/EquationalCriterion.lean, even though I didn't even touch that file. Should I even be trying to do this?

---

• [ ] depends on: #12666

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#12666~~ By Dependent Issues (🤖). Happy coding!

[github-actions[bot]]

PR summary c2377b1395

Import changes

Dependency changes

File	Base Count	Head Count	Change
Mathlib.LinearAlgebra.TensorProduct.Vanishing	1095	1096	+1 (+0.09%)

---

Declarations diff

+ VanishesTrivially.equiv.{uι'} + VanishesTrivially.universe_shift

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[alreadydone]

I'm trying to use the equational criterion in the proof of https://stacks.math.columbia.edu/tag/00NZ, but it doesn't apply directly due to universe non-polymorphism. I'd like to take over this PR if no one objects. (Or maybe it's better to open a new PR; will post here.)

[trivial1711]

I'm trying to use the equational criterion in the proof of https://stacks.math.columbia.edu/tag/00NZ, but it doesn't apply directly due to universe non-polymorphism. I'd like to take over this PR if no one objects. (Or maybe it's better to open a new PR; will post here.)

Please do.

[alreadydone]

Thanks! Opened #20452.