∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Semiring R] [StrongRankCondition R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [Module.Free R M] [inst_5 : AddCommMonoid M'] [inst_6 : Module R M'] [Module.Free R M'],
  Cardinal.lift.{v', v} (Module.rank R M) = Cardinal.lift.{v, v'} (Module.rank R M') → Nonempty (M ≃ₗ[R] M')