Lean/Mathlib: extendScalars is Additive and preserves f.g. projective modules

Mathlib has no Functor.Additive (ModuleCat.extendScalars f) instance. Get it from the adjunction: have : PreservesColimitsOfSize.{0,0} (extendScalars.{u,u,u} f) := (extendRestrictScalarsAdj f).leftAdjoint_preservesColimits (the universe ascription is needed, otherwise 'failed to infer universe levels'), then preservesBinaryBiproducts_of_preservesBinaryCoproducts _ and Functor.additive_of_preservesBinaryBiproducts _. Projectivity: (extendRestrictScalarsAdj f).map_projective _ M.projective_of_categoryTheory_projective then projective_of_module_projective. Finiteness: let := f.toAlgebra; exact Module.Finite.base_change R S M typechecks against the extendScalars object despite it being built from restrictScalars. For finrank use Module.finrank_baseChange (R := S) (S := R) (M' := M) (note the swapped roles of R and S).