diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp
index fa9f0501c2..ab8d22816b 100644
--- a/src/frontends/lean/info_manager.cpp
+++ b/src/frontends/lean/info_manager.cpp
@@ -160,6 +160,11 @@ void info_manager::add_hole_info(pos_info const & begin_pos, pos_info const & en
 #endif
     info_data d = mk_hole_info(s, hole_args, begin_pos, end_pos);
     add_info(begin_pos, d);
+    if (end_pos.first > begin_pos.first) {
+        for (unsigned i = begin_pos.first + 1; i < end_pos.first; i++)
+            add_info({i, 0}, d);
+        add_info(end_pos, d);
+    }
 }
 
 void info_manager::add_vm_obj_format_info(pos_info pos, environment const & env, vm_obj const & thunk) {
diff --git a/tests/lean/interactive/hole3.lean b/tests/lean/interactive/hole3.lean
new file mode 100644
index 0000000000..c7f6faca58
--- /dev/null
+++ b/tests/lean/interactive/hole3.lean
@@ -0,0 +1,8 @@
+def x : nat → nat :=
+λ a, {!
+
+     0 = a
+ --^ "command": "hole", "action": "Infer"
+
+        !}
+      --^ "command": "hole", "action": "Infer"
diff --git a/tests/lean/interactive/hole3.lean.expected.out b/tests/lean/interactive/hole3.lean.expected.out
new file mode 100644
index 0000000000..8c660bc362
--- /dev/null
+++ b/tests/lean/interactive/hole3.lean.expected.out
@@ -0,0 +1,4 @@
+{"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}
+{"message":"Prop\n","response":"ok","seq_num":5}
+{"message":"Prop\n","response":"ok","seq_num":8}