Do indent lines below blank lines if the line below is indented.

This seems like better behavior for the case of:

```

lemma foo : ... :=
  have : stuff := ...

  -- inserting an additional line *here* from below
  have : otherstuff := ...
```

Author: Julian

lua/lean/indent.lua

@@ -142,7 +142,7 @@ function M.indentexpr(linenr)
     -- repetaedly over lines backwards, so we cheat and just check whether the
     -- previous line looks like it has a binder on it.
     local is_end_of_binders = dedent_one > 0 and last:find '^%s*[({[]'
-    return is_end_of_binders and dedent_one or last_indent
+    return is_end_of_binders and dedent_one or last_indent == 0 and current_indent or last_indent
   end
 
   return current_indent ---@type integer

spec/indent_spec.lua

@@ -209,6 +209,51 @@ describe('indent', function()
     )
   )
 
+  it(
+    'does not indent after blank lines with no indent below',
+    helpers.clean_buffer(
+      [[
+        theorem foo : 37 = 37 := by
+          rfl
+
+      ]],
+      function()
+        helpers.feed 'G'
+        assert.current_line.is ''
+
+        helpers.feed 'o#check 37'
+        assert.contents.are [[
+          theorem foo : 37 = 37 := by
+            rfl
+
+          #check 37
+      ]]
+      end
+    )
+  )
+
+  it(
+    'does indent after blank lines with indent below',
+    helpers.clean_buffer(
+      [[
+        theorem foo : 37 = 37 := by
+          have : 1 = 1 := rfl
+
+          have : 38 = 38 := rfl
+      ]],
+      function()
+        helpers.feed 'GOhave : 37 = 37 := rfl'
+        assert.contents.are [[
+          theorem foo : 37 = 37 := by
+            have : 1 = 1 := rfl
+
+            have : 37 = 37 := rfl
+            have : 38 = 38 := rfl
+      ]]
+      end
+    )
+  )
+
   for each in fixtures.indent() do
     it(each.description, function()
       vim.cmd.edit { each.unindented, bang = true }