∀ {R : Type w} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {R' : Type w'}
  {S' : Type v'} [inst_3 : CommSemiring R'] [inst_4 : Semiring S'] [inst_5 : Algebra R' S'] (i : R' →+* R)
  (j : S →+* S'),
  Function.Injective ⇑i →
    Function.Injective ⇑j →
      (j.comp (algebraMap R S)).comp i = algebraMap R' S' →
        Cardinal.lift.{v', v} (Module.rank R S) ≤ Cardinal.lift.{v, v'} (Module.rank R' S')