Mathlib: change universe of projectiveDimension via projectiveDimension_eq_of_linearEquiv

ModuleCat.projectiveDimension_eq_of_linearEquiv (Algebra/Category/ModuleCat/ProjectiveDimension.lean) works across universes: M : ModuleCat.{v} R, N : ModuleCat.{v'} R with [Small.{v} R] [Small.{v'} R]. So a theorem proved for ModuleCat.{u} R (R : Type u) generalizes to any v in three lines: have : Small.{u} M := Module.Finite.small.{u} A M (explicit universe needed, else it infers Small.{v}), then rewrite with an equiv to Shrink.{u} M. Gotcha under the module system: passing e : Shrink.{u} X ≃ₗ[R] Shrink.{v} X fails with 'Shrink not exposed' because the expected type is ↑(ModuleCat.of R _) ≃ₗ ↑?N; state the equiv's type as ModuleCat.of R (Shrink.{u} X) ≃ₗ[R] ModuleCat.of R (Shrink.{v} X) and it unifies.