diff --git a/src/emacs/lean-company.el b/src/emacs/lean-company.el
index 4c01143ac2..1f304b2ccc 100644
--- a/src/emacs/lean-company.el
+++ b/src/emacs/lean-company.el
@@ -34,22 +34,18 @@
                 file-name))
    (t file-name)))
 
-(defun company-lean--import-candidates-main (&optional root-dir)
-  (interactive)
-  (unless root-dir
-    (setq root-dir
-          (f--traverse-upwards (f-exists? (f-expand ".project" it))
-                               (f-dirname (buffer-file-name)))))
-  (let* ((lean-files (f-files root-dir
-                              (lambda (file) (equal (f-ext file) "lean"))
-                              t))
-         ;; Relative to project root-dir
-         (lean-files-r (--map (f-relative it root-dir) lean-files))
-         (candidates
-          (--map (s-replace-all `((,(f-path-separator)  . "."))
-                                (company-lean--import-remove-lean it))
-                 lean-files-r)))
-    (--zip-with (propertize it 'file-name other) candidates lean-files)))
+(defun company-lean--import-candidates-main (root-dir)
+  (when root-dir
+    (let* ((lean-files (f-files root-dir
+                                (lambda (file) (equal (f-ext file) "lean"))
+                                t))
+           ;; Relative to project root-dir
+           (lean-files-r (--map (f-relative it root-dir) lean-files))
+           (candidates
+            (--map (s-replace-all `((,(f-path-separator)  . "."))
+                                  (company-lean--import-remove-lean it))
+                   lean-files-r)))
+      (--zip-with (propertize it 'file-name other) candidates lean-files))))
 
 (defun company-lean--import-prefix ()
   "FINDG is triggered when it looks at '_'"
@@ -63,6 +59,8 @@
 (defun company-lean--import-candidates (prefix)
   (let* ((cur-dir (f-dirname (buffer-file-name)))
          (parent-dir (f-parent cur-dir))
+         (project-dir (f--traverse-upwards (f-exists? (f-expand ".project" it))
+                                           (f-dirname (buffer-file-name))))
          (candidates
           (cond
            ;; prefix = ".."
@@ -73,7 +71,10 @@
            ((s-starts-with? "." prefix)
             (--map (concat "." it)
                    (company-lean--import-candidates-main cur-dir)))
-           (t (company-lean--import-candidates-main)))))
+           ;; normal prefix
+           (t (-flatten
+               (-map 'company-lean--import-candidates-main
+                     (lean-path-list)))))))
     (--filter (s-starts-with? prefix it) candidates)))
 
 (defun company-lean--import-location (arg)
diff --git a/src/emacs/lean-tags.el b/src/emacs/lean-tags.el
index c4a07fed5a..1426a9c572 100644
--- a/src/emacs/lean-tags.el
+++ b/src/emacs/lean-tags.el
@@ -5,41 +5,24 @@
 ;;
 
 (require 'dash)
+(require 'f)
+(require 'lean-util)
+
 (defun lean-tags-table-list ()
-  (let* ((lean-path-env-list
-          (parse-colon-path (getenv "LEAN_PATH")))
-         (lean--path-list
-          (parse-colon-path
-           (ignore-errors
-             (car (process-lines (lean-get-executable lean-executable-name)
-                                 "--path")))))
-         (lean-path-list
-          (-uniq (append lean-path-env-list lean--path-list)))
-         (tags-file-list
-          (-non-nil
-           (--map (let ((tags-file (concat (file-name-as-directory it)
-                                           "TAGS")))
-                    (if (file-exists-p tags-file)
-                        tags-file
-                      nil))
-                  lean-path-list))))
-    tags-file-list))
+  (-filter 'f-exists?
+           (--map (f-join it "TAGS") (lean-path-list))))
 
 (defun lean-generate-tags ()
   "Run linja TAGS and let emacs use the generated TAGS file."
   (interactive)
-  (let ((ltags-file-name (lean-get-executable "linja"))
-        tags-file)
+  (let ((ltags-file-name (lean-get-executable "linja")))
     (message "Generating TAGS...")
     (apply 'call-process
            (append `(,ltags-file-name nil "*lean-tags*" nil)
                    lean-flycheck-checker-options
                    '("TAGS")))
     (message "TAGS generated.")
-    (setq tags-table-list (lean-tags-table-list))
-    (setq tags-file (lean-find-file-upward "TAGS"))
-    (when tags-file
-      (add-to-list 'tags-table-list tags-file))))
+    (setq tags-table-list (lean-tags-table-list))))
 
 (defmacro lean-tags-make-advice-to-call-ltags (f)
   (let* ((f-name (symbol-name f))
diff --git a/src/emacs/lean-util.el b/src/emacs/lean-util.el
index 400395339a..e48b89d70a 100644
--- a/src/emacs/lean-util.el
+++ b/src/emacs/lean-util.el
@@ -5,6 +5,10 @@
 ;;
 
 (require 'cl-lib)
+(require 'f)
+(require 's)
+(require 'dash)
+(require 'dash-functional)
 
 (defun lean-concat-paths (&rest seq)
   "Concatenate paths"
@@ -43,4 +47,24 @@
   (let ((lean-bin-dir-name "bin"))
     (lean-concat-paths (lean-get-rootdir) lean-bin-dir-name exe-name)))
 
+(defun lean-path-list ()
+  (interactive)
+  (let* ((lean-path-env-list
+          (parse-colon-path (getenv "LEAN_PATH")))
+         (lean--path-list
+          (parse-colon-path
+           (ignore-errors
+             (car (process-lines (lean-get-executable lean-executable-name)
+                                 "--path")))))
+         (project-dir (f--traverse-upwards (f-exists? (f-expand ".project" it))
+                                           (f-dirname (buffer-file-name))))
+         (path-list (append lean-path-env-list lean--path-list)))
+    (when project-dir
+      (setq path-list
+            (--map-when (f-relative? it)
+                        (f-canonical (f-join project-dir it))
+                        path-list)))
+    (-uniq (-map (-compose 'f-slash 'f-canonical)
+                 path-list))))
+
 (provide 'lean-util)