∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  Function.Surjective ⇑f → Cardinal.lift.{v, v'} (Module.rank R M') ≤ Cardinal.lift.{v', v} (Module.rank R M)