Provides context-sensitive auto completion for lean-mode.