diff --git a/src/Lean/Data/Lsp/Basic.lean b/src/Lean/Data/Lsp/Basic.lean
index e2db6ff3d0a8..41a4bcf03c2a 100644
--- a/src/Lean/Data/Lsp/Basic.lean
+++ b/src/Lean/Data/Lsp/Basic.lean
@@ -101,6 +101,47 @@ structure TextDocumentEdit where
 -- both of these are pretty global, we can look at their
 -- uses when single file behaviour works.
 
+structure ChangeAnnotation where
+  label : String
+  needsConfirmation? : Option Bool
+  description? : Option String
+  deriving ToJson, FromJson
+
+def WorkspaceEditChanges := Std.RBMap DocumentUri (TextEditBatch) compare
+
+instance : ToJson WorkspaceEditChanges := ⟨fun c => Id.run do
+  let oldList := c.toList
+  let mut newList := []
+  for ⟨key, value⟩ in oldList do
+    let newValue := ⟨key, (toJson value)⟩
+    newList := newValue::newList
+  let newMap := Std.RBMap.fromList newList Ord.compare
+  return Json.obj newMap.val
+⟩
+
+def WorkspaceEditChangeAnnotations := Std.RBMap String (ChangeAnnotation) compare
+
+instance : ToJson WorkspaceEditChangeAnnotations := ⟨fun c => Id.run do
+  let oldList := c.toList
+  let mut newList := []
+  for ⟨key, value⟩ in oldList do
+    let newValue := ⟨key, (toJson value)⟩
+    newList := newValue::newList
+  let newMap := Std.RBMap.fromList newList Ord.compare
+  return Json.obj newMap.val
+⟩
+
+structure WorkspaceEdit where
+  changes? : Option (WorkspaceEditChanges)
+  documentChanges? : Option (Array TextDocumentEdit)
+  changeAnnotations? : Option (WorkspaceEditChangeAnnotations)
+  deriving ToJson
+
+structure ApplyWorkspaceEditParams where
+  label? : Option String
+  edit : WorkspaceEdit
+  deriving ToJson
+
 structure TextDocumentItem where
   uri : DocumentUri
   languageId : String
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 9ad6ca53373d..4eac3db89fe6 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -407,6 +407,7 @@ section MessageHandling
          srcSearchPath
          doc := st.doc
          hLog := ctx.hLog
+         hOut := ctx.hOut
          initParams := ctx.initParams }
      let t? ← EIO.toIO' <| handleLspRequest method params rc
      let t₁ ← match t? with
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index 0e2660c93a0e..25bbe32573fb 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -200,6 +200,7 @@ def handlePlainTermGoal (p : PlainTermGoalParams)
 def getConvZoomCommands (expr: Widget.SubexprInfo) (p: Lsp.PlainGoalParams)
     : RequestM (RequestTask (Option Widget.ConvZoomCommands)) := do
   let t ← getInteractiveGoals p
+  let ctx ← read
   let goals := match t.get with
   | Except.ok x => match x with
     | some val => val.goals
@@ -211,8 +212,11 @@ def getConvZoomCommands (expr: Widget.SubexprInfo) (p: Lsp.PlainGoalParams)
   withWaitFindSnap doc (fun s => s.endPos >= hoverPos)
     (notFoundX := pure none) fun snap => do
       let ret ← (expr.info.val.ctx.runMetaM expr.info.val.info.lctx
-        (Widget.buildConvZoomCommands expr goals[0]! snap.stx hoverPos text))
-      return some ret
+        (Widget.buildConvZoomCommands expr goals[0]! snap.stx hoverPos doc))
+      let hOut := ctx.hOut
+      let request : JsonRpc.Request ApplyWorkspaceEditParams := { id := "applyEdit", method := "workspace/applyEdit", param := ret.params }
+      let _ := ←hOut.writeLspMessage request
+      return some ret.commands
 
 partial def handleDocumentHighlight (p : DocumentHighlightParams)
     : RequestM (RequestTask (Array DocumentHighlight)) := do
diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean
index dd905307b86d..575cb3223807 100644
--- a/src/Lean/Server/Requests.lean
+++ b/src/Lean/Server/Requests.lean
@@ -59,6 +59,7 @@ structure RequestContext where
   srcSearchPath : SearchPath
   doc           : FileWorker.EditableDocument
   hLog          : IO.FS.Stream
+  hOut          : IO.FS.Stream
   initParams    : Lsp.InitializeParams
 
 abbrev RequestTask α := Task (Except RequestError α)
diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index ce09f372cf30..56c8e059f0d4 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -642,6 +642,8 @@ section MainLoop
         mainLoop (←runClientTask)
       | Message.response "register_ilean_watcher" _      =>
         mainLoop (←runClientTask)
+      | Message.response "applyEdit" _ =>
+        mainLoop (←runClientTask)
       | _ => throwServerError "Got invalid JSON-RPC message"
     | ServerEvent.clientError e => throw e
     | ServerEvent.workerEvent fw ev =>
diff --git a/src/Lean/Widget/ConvZoomCommands.lean b/src/Lean/Widget/ConvZoomCommands.lean
index 3c91d4b3c0d0..21d87b9e0bb4 100644
--- a/src/Lean/Widget/ConvZoomCommands.lean
+++ b/src/Lean/Widget/ConvZoomCommands.lean
@@ -6,6 +6,8 @@ Authors: Robin Böhne
 import Lean.Widget.InteractiveGoal
 import Lean.Meta.ExprLens
 import Lean.Server.InfoUtils
+import Lean.Server.FileWorker.Utils
+import Lean.Data.Lsp.Utf16
 
 namespace Lean.Widget
 open Server
@@ -179,6 +181,7 @@ private def locate (tParam : Syntax.Traverser) (pos : String.Pos) : LocateReturn
   return {pathBeforeConv := path.reverse, pathAfterConv := pathAfterConv }
 
 private def syntaxInsert (stx : Syntax) (pathBeforeConvParam : List Nat) (pathAfterConvParam : List Nat) (value : String) : Syntax := Id.run do
+  if value == "" then return stx
   let mut t := Syntax.Traverser.fromSyntax stx
   let mut pathBeforeConv := pathBeforeConvParam
   while pathBeforeConv.length > 0 do
@@ -234,6 +237,18 @@ private def syntaxInsert (stx : Syntax) (pathBeforeConvParam : List Nat) (pathAf
       t := t.down pathAfterConv.head!
       pathAfterConv := pathAfterConv.tail!
 
+    -- check if it's an enter and if yes merge them
+    let argAsString := reprint! t.cur.getArgs[pathAfterConv.head!]!
+    let mut newval := value
+    let mut convsMerged := false
+    if "enter".isPrefixOf argAsString then
+      let mut additionalArgs := (argAsString.splitOn "\n").head!
+      additionalArgs := (additionalArgs.drop 7).dropRight 1
+
+      let left := value.take 7
+      let right := value.drop 7
+      newval := left ++ additionalArgs ++ ", " ++ right
+      convsMerged := true
     --get whitespace from previous tactic and make new node
 
 
@@ -271,17 +286,23 @@ private def syntaxInsert (stx : Syntax) (pathBeforeConvParam : List Nat) (pathAf
 
 
 
-    let newNode := Syntax.atom (SourceInfo.original "".toSubstring 0 "".toSubstring 0) (frontWhitespace ++ value ++ "\n" ++ whitespace)
+    let newNode := Syntax.atom (SourceInfo.original "".toSubstring 0 "".toSubstring 0) (frontWhitespace ++ newval ++ "\n" ++ whitespace)
     -- add new node to syntax and move to the very top
     let argList := t.cur.getArgs.toList
-    let newArgList := List.append (argList.take (pathAfterConv.head! + 1) ) (newNode::(argList.drop (pathAfterConv.head! + 1)))
+    let newArgList := match convsMerged with
+      | false => List.append (argList.take (pathAfterConv.head! + 1) ) (newNode::(argList.drop (pathAfterConv.head! + 1)))
+      | true => List.append (argList.take (pathAfterConv.head!) ) (newNode::(argList.drop (pathAfterConv.head! + 1)))
     t := t.setCur (t.cur.setArgs newArgList.toArray)
     while t.parents.size > 0 do
       t := t.up
 
     return t.cur
 
-def buildConvZoomCommands (subexprParam : SubexprInfo) (goalParam : InteractiveGoal) (stx : Syntax) (p: String.Pos) (text: FileMap): MetaM ConvZoomCommands := do
+structure ConvZoomReturn where
+  commands : ConvZoomCommands
+  params : Lsp.ApplyWorkspaceEditParams
+
+def buildConvZoomCommands (subexprParam : SubexprInfo) (goalParam : InteractiveGoal) (stx : Syntax) (p : String.Pos) (doc : Lean.Server.FileWorker.EditableDocument): MetaM ConvZoomReturn := do
   let mut list := (SubExpr.Pos.toArray subexprParam.subexprPos).toList
   let mut expr := (getExprFromCodeWithInfos goalParam.type).head!
   let mut ret := ""
@@ -312,6 +333,7 @@ def buildConvZoomCommands (subexprParam : SubexprInfo) (goalParam : InteractiveG
         | none => panic! "could not get range"
 
   -- insert new syntax into document
+  let text := doc.meta.text
   let part1 := text.source.take range.start.byteIdx
   let part2 := text.source.drop (range.stop.byteIdx + 2)
   let newsrc := part1 ++ val ++ part2
@@ -319,6 +341,12 @@ def buildConvZoomCommands (subexprParam : SubexprInfo) (goalParam : InteractiveG
   ret := ret ++ "--Result after inserting enter:\n"
   ret := ret ++ "/-\n" ++ newsrc ++ "\n-/"
 
-  return { commands? := ret }
+  let commands : ConvZoomCommands := { commands? := "" }
+
+  let textEdit : Lsp.TextEdit := { range := { start := text.utf8PosToLspPos range.start, «end» := text.utf8PosToLspPos {byteIdx := range.stop.byteIdx + 2} }, newText := val}
+  let textDocumentEdit : Lsp.TextDocumentEdit := { textDocument := { uri := doc.meta.uri, version? := doc.meta.version }, edits := [textEdit].toArray }
+  let edit : Lsp.WorkspaceEdit := { changes? := none, documentChanges? := [textDocumentEdit].toArray , changeAnnotations? := none}
+  let params : Lsp.ApplyWorkspaceEditParams := { label? := none, edit := edit }
+  return { commands:= commands, params := params }
 
 end Lean.Widget