diff --git a/lean4-mode/lean4-input.el b/lean4-mode/lean4-input.el
index 72ead5bbd1..646e47a301 100644
--- a/lean4-mode/lean4-input.el
+++ b/lean4-mode/lean4-input.el
@@ -1,3 +1,4 @@
+;;;  -*- lexical-binding: t -*-
 ;;; lean4-input.el --- The Lean input method (based/copied from Agda)
 ;;;
 ;;; DISCLAIMER: This file is based on agda-input.el provided with the Agda language.
@@ -22,6 +23,7 @@
 ;;; Code:
 
 (require 'quail)
+(require 'cl-lib)
 
 ;; Quail is quite stateful, so be careful when editing this code.  Note
 ;; that with-temp-buffer is used below whenever buffer-local state is
@@ -53,17 +55,13 @@ removing all space and newline characters."
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Functions used to tweak translation pairs
 
-;; lexical-let is used since Elisp lacks lexical scoping.
-
 (defun lean4-input-compose (f g)
   "\x -> concatMap F (G x)"
-  (lexical-let ((f1 f) (g1 g))
-    (lambda (x) (lean4-input-concat-map f1 (funcall g1 x)))))
+  (lambda (x) (lean4-input-concat-map f (funcall g x))))
 
 (defun lean4-input-or (f g)
   "\x -> F x ++ G x"
-  (lexical-let ((f1 f) (g1 g))
-    (lambda (x) (append (funcall f1 x) (funcall g1 x)))))
+  (lambda (x) (append (funcall f x) (funcall g x))))
 
 (defun lean4-input-nonempty ()
   "Only keep pairs with a non-empty first component."
@@ -71,42 +69,36 @@ removing all space and newline characters."
 
 (defun lean4-input-prepend (prefix)
   "Prepend PREFIX to all key sequences."
-  (lexical-let ((prefix1 prefix))
-    (lambda (x) `((,(concat prefix1 (car x)) . ,(cdr x))))))
+    (lambda (x) `((,(concat prefix (car x)) . ,(cdr x)))))
 
 (defun lean4-input-prefix (prefix)
   "Only keep pairs whose key sequence starts with PREFIX."
-  (lexical-let ((prefix1 prefix))
-    (lambda (x)
-      (if (equal (substring (car x) 0 (length prefix1)) prefix1)
-          (list x)))))
+  (lambda (x)
+    (if (equal (substring (car x) 0 (length prefix)) prefix)
+        (list x))))
 
 (defun lean4-input-suffix (suffix)
   "Only keep pairs whose key sequence ends with SUFFIX."
-  (lexical-let ((suffix1 suffix))
-    (lambda (x)
-      (if (equal (substring (car x)
-                            (- (length (car x)) (length suffix1)))
-                 suffix1)
-          (list x)))))
+  (lambda (x)
+    (if (equal (substring (car x)
+                          (- (length (car x)) (length suffix)))
+               suffix)
+        (list x))))
 
 (defun lean4-input-drop (ss)
   "Drop pairs matching one of the given key sequences.
 SS should be a list of strings."
-  (lexical-let ((ss1 ss))
-    (lambda (x) (unless (member (car x) ss1) (list x)))))
+  (lambda (x) (unless (member (car x) ss) (list x))))
 
 (defun lean4-input-drop-beginning (n)
   "Drop N characters from the beginning of each key sequence."
-  (lexical-let ((n1 n))
-    (lambda (x) `((,(substring (car x) n1) . ,(cdr x))))))
+  (lambda (x) `((,(substring (car x) n) . ,(cdr x)))))
 
 (defun lean4-input-drop-end (n)
   "Drop N characters from the end of each key sequence."
-  (lexical-let ((n1 n))
-    (lambda (x)
-      `((,(substring (car x) 0 (- (length (car x)) n1)) .
-         ,(cdr x))))))
+  (lambda (x)
+    `((,(substring (car x) 0 (- (length (car x)) n)) .
+       ,(cdr x)))))
 
 (defun lean4-input-drop-prefix (prefix)
   "Only keep pairs whose key sequence starts with PREFIX.
@@ -118,10 +110,9 @@ This prefix is dropped."
 (defun lean4-input-drop-suffix (suffix)
   "Only keep pairs whose key sequence ends with SUFFIX.
 This suffix is dropped."
-  (lexical-let ((suffix1 suffix))
-    (lean4-input-compose
-     (lean4-input-drop-end (length suffix1))
-     (lean4-input-suffix suffix1))))
+  (lean4-input-compose
+   (lean4-input-drop-end (length suffix))
+   (lean4-input-suffix suffix)))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Customization