diff --git a/lean4-mode/lean4-eri.el b/lean4-mode/lean4-eri.el
index f0df8d74f7..db9d58fb81 100644
--- a/lean4-mode/lean4-eri.el
+++ b/lean4-mode/lean4-eri.el
@@ -6,7 +6,7 @@
 
 ;;; Code:
 
-(require 'cl)
+(require 'cl-lib)
 
 (defun lean4-eri-current-line-length nil
   "Calculate length of current line."
diff --git a/lean4-mode/lean4-input.el b/lean4-mode/lean4-input.el
index cc06a458f1..72ead5bbd1 100644
--- a/lean4-mode/lean4-input.el
+++ b/lean4-mode/lean4-input.el
@@ -23,8 +23,6 @@
 
 (require 'quail)
 
-(eval-when-compile
-  (require 'cl))
 ;; Quail is quite stateful, so be careful when editing this code.  Note
 ;; that with-temp-buffer is used below whenever buffer-local state is
 ;; modified.