diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index a5353a9c8..ad3aaaf61 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -152,16 +152,6 @@ enabled and disabled respectively.")
   (add-to-list 'lean-hooks-alist '(after-change-functions  . lean-after-change-function))
   (add-to-list 'lean-hooks-alist '(before-change-functions . lean-before-change-function)))
 
-(defun lean-choose-minor-mode-based-on-extension ()
-  ;; Based on the extension of buffer, return either 'HoTT or 'Standard
-  (interactive)
-  (let ((file-name (buffer-file-name)))
-    (cond ((s-ends-with? ".lean" file-name)
-           'Standard)
-          ((s-ends-with? ".hlean" file-name)
-           'HoTT)
-          (t 'Standard))))
-
 (defun lean-mode-setup ()
   "Default lean-mode setup"
   ;; Flycheck
diff --git a/src/emacs/lean-util.el b/src/emacs/lean-util.el
index f90d7498d..7a0c90f34 100644
--- a/src/emacs/lean-util.el
+++ b/src/emacs/lean-util.el
@@ -184,4 +184,14 @@
     (when lean-delete-trailing-whitespace
       (delete-trailing-whitespace)))
 
+(defun lean-choose-minor-mode-based-on-extension ()
+  ;; Based on the extension of buffer, return either 'hott or 'standard
+  (interactive)
+  (let ((file-name (buffer-file-name)))
+    (cond ((s-ends-with? ".lean" file-name)
+           'standard)
+          ((s-ends-with? ".hlean" file-name)
+           'hott)
+          (t 'standard))))
+
 (provide 'lean-util)