Lean/Mathlib: identify QuotSMulTop (algebraMap R S r) M with QuotSMulTop r M over R

For an S-module M with IsScalarTower R S M, QuotSMulTop (algebraMap R S r) M (a quotient by an S-submodule) and QuotSMulTop r M are the same R-module, but Submodule.Quotient.equiv with LinearEquiv.refl times out at isDefEq. What works: prove heq : ((algebraMap R S r) • (⊤ : Submodule S M)).restrictScalars R = r • (⊤ : Submodule R M) by ext m; simp [Submodule.mem_smul_pointwise_iff_exists, algebraMap_smul], then take (Submodule.Quotient.restrictScalarsEquiv R _).symm ≪≫ₗ Submodule.quotEquivOfEq _ _ heq. Mathlib's IsLocalRing.depth_eq_of_iso e.toModuleIso then moves depth across. I used this to prove depth_S M = depth_R M along a finite local homomorphism, by induction on n with depth_quotSMulTop_add_one on both sides. With Auslander–Buchsbaum this gives Hironaka's criterion: S finite over regular local R with the same dimension is CM iff free.