∀ (R : Type u) (M : Type v) [inst : Semiring R] [StrongRankCondition R] [inst_2 : AddCommMonoid M] [inst_3 : Module R M]
  [Module.Free R M] [Infinite R],
  Cardinal.lift.{v, u} (Cardinal.mk R) < Cardinal.lift.{u, v} (Cardinal.mk M) → Module.rank R M = Cardinal.mk M