diff --git a/src/frontends/lean/interactive.cpp b/src/frontends/lean/interactive.cpp
index 81bedb9e7c..23beb144ed 100644
--- a/src/frontends/lean/interactive.cpp
+++ b/src/frontends/lean/interactive.cpp
@@ -277,7 +277,7 @@ bool json_of_hole(hole_info_data const & hole, std::string const & file, json &
     j["start"]["line"]   = hole.get_begin_pos().first;
     j["start"]["column"] = hole.get_begin_pos().second;
     j["end"]["line"]     = hole.get_end_pos().first;
-    j["end"]["column"]   = hole.get_end_pos().second + 1;
+    j["end"]["column"]   = hole.get_end_pos().second;
     return true;
 }
 
@@ -332,7 +332,7 @@ void execute_hole_command(module_info const & m_mod_info,
         j["replacements"]["start"]["line"]   = hole.get_begin_pos().first;
         j["replacements"]["start"]["column"] = hole.get_begin_pos().second;
         j["replacements"]["end"]["line"]     = hole.get_end_pos().first;
-        j["replacements"]["end"]["column"]   = hole.get_end_pos().second + 1;
+        j["replacements"]["end"]["column"]   = hole.get_end_pos().second;
     }
 }
 
diff --git a/tests/lean/interactive/hole1.lean.expected.out b/tests/lean/interactive/hole1.lean.expected.out
index 1b7f19b310..dfbaed564c 100644
--- a/tests/lean/interactive/hole1.lean.expected.out
+++ b/tests/lean/interactive/hole1.lean.expected.out
@@ -1,3 +1,3 @@
 {"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"warning","text":"declaration 'x' uses sorry"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
-{"replacements":{"alternatives":[{"code":"a + a","description":""}],"end":{"column":17,"line":2},"file":"f","start":{"column":5,"line":2}},"response":"ok","seq_num":3}
+{"replacements":{"alternatives":[{"code":"a + a","description":""}],"end":{"column":16,"line":2},"file":"f","start":{"column":5,"line":2}},"response":"ok","seq_num":3}
diff --git a/tests/lean/interactive/hole2.lean.expected.out b/tests/lean/interactive/hole2.lean.expected.out
index 57d535ea3f..7562a2da73 100644
--- a/tests/lean/interactive/hole2.lean.expected.out
+++ b/tests/lean/interactive/hole2.lean.expected.out
@@ -1,3 +1,3 @@
 {"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"warning","text":"declaration 'x' uses sorry"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
-{"end":{"column":17,"line":2},"file":"f","response":"ok","results":[{"description":"Infer type of the expression in the hole","name":"Infer"},{"description":"Show the current goal","name":"Show"},{"description":"Try to fill the hole using the given argument","name":"Use"}],"seq_num":3,"start":{"column":5,"line":2}}
+{"end":{"column":16,"line":2},"file":"f","response":"ok","results":[{"description":"Infer type of the expression in the hole","name":"Infer"},{"description":"Show the current goal","name":"Show"},{"description":"Try to fill the hole using the given argument","name":"Use"}],"seq_num":3,"start":{"column":5,"line":2}}