diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index 72909bd33..63062fccc 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -52,7 +52,7 @@
   (local-set-key "\C-c\C-t" 'lean-eldoc-documentation-function)
   (local-set-key "\C-c\C-f" 'lean-fill-placeholder)
   (local-set-key "\M-."     'lean-find-tag)
-  (local-set-key [tab]      'lean-complete-tag))
+  (local-set-key [tab]      'completion-at-point))
 
 (define-abbrev-table 'lean-abbrev-table
   '(("var"    "variable")
@@ -92,13 +92,18 @@
     (remove-hook 'lean-mode-hook 'whitespace-cleanup-mode))
   ;; eldoc
   (set (make-local-variable 'eldoc-documentation-function)
-       'lean-eldoc-documentation-function))
+       'lean-eldoc-documentation-function)
+  ;; company-mode
+  (when lean-company-use
+    (require 'company)
+    (company-mode t)
+    (set (make-local-variable 'company-backends) '(company-etags))))
 
 ;; Automatically use lean-mode for .lean files.
 ;;;###autoload
 (push '("\\.lean$" . lean-mode) auto-mode-alist)
 ;; Use utf-8 encoding
-;;;###autoload
+;;;### autoload
 (modify-coding-system-alist 'file "\\.lean\\'" 'utf-8)
 
 (provide 'lean-mode)
diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el
index dba1480be..f06ddb46e 100644
--- a/src/emacs/lean-settings.el
+++ b/src/emacs/lean-settings.el
@@ -35,6 +35,11 @@
   :group 'lean
   :type 'boolean)
 
+(defcustom lean-company-use t
+  "Use company mode for lean."
+  :group 'lean
+  :type 'boolean)
+
 (defcustom lean-flycheck-checker-name "lmake"
   "lean-flychecker checker name"
   :group 'lean