diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean
index d914c04bde..00d9e99665 100644
--- a/src/Lean/Elab/InfoTree.lean
+++ b/src/Lean/Elab/InfoTree.lean
@@ -78,7 +78,6 @@ structure TacticInfo extends ElabInfo where
   goalsBefore : List MVarId
   mctxAfter   : MetavarContext
   goalsAfter  : List MVarId
-  inConv      : Bool
   deriving Inhabited
 
 structure MacroExpansionInfo where
@@ -189,17 +188,17 @@ def FieldInfo.format (ctx : ContextInfo) (info : FieldInfo) : IO Format := do
   ctx.runMetaM info.lctx do
     return f!"{info.fieldName} : {← Meta.ppExpr (← Meta.inferType info.val)} := {← Meta.ppExpr info.val} @ {formatStxRange ctx info.stx}"
 
-def ContextInfo.ppGoals (ctx : ContextInfo) (goals : List MVarId) (inConv : Bool) : IO Format :=
+def ContextInfo.ppGoals (ctx : ContextInfo) (goals : List MVarId) : IO Format :=
   if goals.isEmpty then
     return "no goals"
   else
-    ctx.runMetaM {} (return Std.Format.prefixJoin "\n" (← goals.mapM (Meta.ppGoal . inConv)))
+    ctx.runMetaM {} (return Std.Format.prefixJoin "\n" (← goals.mapM (Meta.ppGoal .)))
 
 def TacticInfo.format (ctx : ContextInfo) (info : TacticInfo) : IO Format := do
   let ctxB := { ctx with mctx := info.mctxBefore }
   let ctxA := { ctx with mctx := info.mctxAfter }
-  let goalsBefore ← ctxB.ppGoals info.goalsBefore info.inConv
-  let goalsAfter  ← ctxA.ppGoals info.goalsAfter info.inConv
+  let goalsBefore ← ctxB.ppGoals info.goalsBefore
+  let goalsAfter  ← ctxA.ppGoals info.goalsAfter
   return f!"Tactic @ {formatElabInfo ctx info.toElabInfo}\n{info.stx}\nbefore {goalsBefore}\nafter {goalsAfter}"
 
 def MacroExpansionInfo.format (ctx : ContextInfo) (info : MacroExpansionInfo) : IO Format := do
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 4d51c255e4..c75a16989b 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -39,8 +39,6 @@ structure Context where
   main       : MVarId
   -- declaration name of the executing elaborator, used by `mkTacticInfo` to persist it in the info tree
   elaborator : Name
-  -- `true` when in `conv` tactic mode. This flag is only used to pretty print the goals showing just the left-hand-side
-  inConv     : Bool := false
 
 structure State where
   goals : List MVarId
@@ -121,7 +119,6 @@ def mkTacticInfo (mctxBefore : MetavarContext) (goalsBefore : List MVarId) (stx
     stx           := stx
     mctxAfter     := (← getMCtx)
     goalsAfter    := (← getUnsolvedGoals)
-    inConv        := (← read).inConv
   }
 
 def mkInitialTacticInfo (stx : Syntax) : TacticM (TacticM Info) := do
diff --git a/src/Lean/Elab/Tactic/Conv/Basic.lean b/src/Lean/Elab/Tactic/Conv/Basic.lean
index fae3711420..7a78696bc9 100644
--- a/src/Lean/Elab/Tactic/Conv/Basic.lean
+++ b/src/Lean/Elab/Tactic/Conv/Basic.lean
@@ -14,7 +14,7 @@ open Meta
 def mkConvGoalFor (lhs : Expr) : MetaM (Expr × Expr) := do
   let lhsType ← inferType lhs
   let rhs ← mkFreshExprMVar lhsType
-  let targetNew ← mkEq lhs rhs
+  let targetNew := mkLHSGoal (← mkEq lhs rhs)
   let newGoal ← mkFreshExprSyntheticOpaqueMVar targetNew
   return (rhs, newGoal)
 
@@ -23,7 +23,7 @@ def convert (lhs : Expr) (conv : TacticM Unit) : TacticM (Expr × Expr) := do
   let savedGoals ← getGoals
   try
     setGoals [newGoal.mvarId!]
-    withReader (fun ctx => { ctx with inConv := true }) conv
+    conv
     pruneSolvedGoals
     for mvarId in (← getGoals) do
       try
@@ -52,7 +52,7 @@ def getRhs : TacticM Expr :=
 /-- `⊢ lhs = rhs` ~~> `⊢ lhs' = rhs` using `h : lhs = lhs'`. -/
 def updateLhs (lhs' : Expr) (h : Expr) : TacticM Unit := do
   let rhs ← getRhs
-  let newGoal ← mkFreshExprSyntheticOpaqueMVar (← mkEq lhs' rhs)
+  let newGoal ← mkFreshExprSyntheticOpaqueMVar (mkLHSGoal (← mkEq lhs' rhs))
   assignExprMVar (← getMainGoal) (← mkEqTrans h newGoal)
   replaceMainGoal [newGoal.mvarId!]
 
@@ -60,7 +60,7 @@ def updateLhs (lhs' : Expr) (h : Expr) : TacticM Unit := do
 def changeLhs (lhs' : Expr) : TacticM Unit := do
   let rhs ← getRhs
   liftMetaTactic1 fun mvarId => do
-    replaceTargetDefEq mvarId (← mkEq lhs' rhs)
+    replaceTargetDefEq mvarId (mkLHSGoal (← mkEq lhs' rhs))
 
 @[builtinTactic Lean.Parser.Tactic.Conv.skip] def evalSkip : Tactic := fun stx => do
    liftMetaTactic1 fun mvarId => do
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 182180f7d7..f673f9d319 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -1038,6 +1038,22 @@ def annotation? (kind : Name) (e : Expr) : Option Expr :=
   | Expr.mdata d b _ => if d.size == 1 && d.getBool kind false then some b else none
   | _                => none
 
+/--
+  Annotate `e` with the LHS annotation. The delaborator displays
+  expressions of the form `lhs = rhs` as `lhs` when they have this annotation.
+-/
+def mkLHSGoal (e : Expr) : Expr :=
+  mkAnnotation `_lhsGoal e
+
+def isLHSGoal? (e : Expr) : Option Expr :=
+  match annotation? `_lhsGoal e with
+  | none => none
+  | some e =>
+    if e.isAppOfArity `Eq 3 then
+      some e.appFn!.appArg!
+    else
+      none
+
 def mkFreshFVarId {m : Type → Type} [Monad m] [MonadNameGenerator m] : m FVarId :=
   mkFreshId
 
diff --git a/src/Lean/Meta/PPGoal.lean b/src/Lean/Meta/PPGoal.lean
index e4862f13d4..0a1276c700 100644
--- a/src/Lean/Meta/PPGoal.lean
+++ b/src/Lean/Meta/PPGoal.lean
@@ -144,20 +144,7 @@ end ToHide
 private def addLine (fmt : Format) : Format :=
   if fmt.isNil then fmt else fmt ++ Format.line
 
-/--
-  Return the target type for the given goal.
-  If `inConv == true` and target type is an equality, then return the left-hand-side only. -/
-def getGoalTarget (mvarDecl : MetavarDecl) (inConv : Bool) : MetaM Expr := do
-  let target ← instantiateMVars mvarDecl.type
-  if inConv then
-    if let some (_, lhs, _) ← matchEq? target then
-      instantiateMVars lhs
-    else
-      return target
-  else
-    return target
-
-def ppGoal (mvarId : MVarId) (inConv := false) : MetaM Format := do
+def ppGoal (mvarId : MVarId) : MetaM Format := do
   match (← getMCtx).findDecl? mvarId with
   | none          => pure "unknown goal"
   | some mvarDecl => do
@@ -214,7 +201,7 @@ def ppGoal (mvarId : MVarId) (inConv := false) : MetaM Format := do
            ppVars varNames prevType? fmt localDecl
       let fmt ← pushPending varNames type? fmt
       let fmt := addLine fmt
-      let typeFmt ← ppExpr (← getGoalTarget mvarDecl inConv)
+      let typeFmt ← ppExpr (← instantiateMVars mvarDecl.type)
       let fmt := fmt ++ "⊢ " ++ Format.nest indent typeFmt
       match mvarDecl.userName with
       | Name.anonymous => pure fmt
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 11539b2e3d..ad442a1512 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -446,6 +446,8 @@ def delabMData : Delab := do
       `(.($s)) -- We only include the inaccessible annotation when we are delaborating patterns
     else
       return s
+  else if let some _ := isLHSGoal? (← getExpr) then
+    withMDataExpr <| withAppFn <| withAppArg <| delab
   else
     withMDataOptions delab
 
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index 1aea04063e..1a044207f8 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -148,7 +148,7 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
           let goals ← List.join <$> rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter } =>
             let ci := if useAfter then { ci with mctx := ti.mctxAfter } else { ci with mctx := ti.mctxBefore }
             let goals := if useAfter then ti.goalsAfter else ti.goalsBefore
-            ci.runMetaM {} <| goals.mapM (fun g => Meta.withPPInaccessibleNames (Widget.goalToInteractive g ti.inConv))
+            ci.runMetaM {} <| goals.mapM (fun g => Meta.withPPInaccessibleNames (Widget.goalToInteractive g))
           return some { goals := goals.toArray }
 
       return none
@@ -182,7 +182,7 @@ partial def getInteractiveTermGoal (p : Lsp.PlainTermGoalParams)
          -- for binders, hide the last hypothesis (the binder itself)
          let lctx' := if ti.isBinder then i.lctx.pop else i.lctx
          let goal ← ci.runMetaM lctx' do
-           Meta.withPPInaccessibleNames <| Widget.goalToInteractive (← Meta.mkFreshExprMVar ty).mvarId! (inConv := false)
+           Meta.withPPInaccessibleNames <| Widget.goalToInteractive (← Meta.mkFreshExprMVar ty).mvarId!
          let range := if let some r := i.range? then r.toLspRange text else ⟨p.position, p.position⟩
          return some { goal with range }
       return none
diff --git a/src/Lean/Widget/InteractiveGoal.lean b/src/Lean/Widget/InteractiveGoal.lean
index 99ec1b1e4d..97947156dc 100644
--- a/src/Lean/Widget/InteractiveGoal.lean
+++ b/src/Lean/Widget/InteractiveGoal.lean
@@ -66,7 +66,7 @@ structure InteractiveGoals where
 
 open Meta in
 /-- A variant of `Meta.ppGoal` which preserves subexpression information for interactivity. -/
-def goalToInteractive (mvarId : MVarId) (inConv : Bool) : MetaM InteractiveGoal := do
+def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
   let some mvarDecl ← (← getMCtx).findDecl? mvarId
     | throwError "unknown goal {mvarId}"
   let ppAuxDecls := pp.auxDecls.get (← getOptions)
@@ -118,7 +118,7 @@ def goalToInteractive (mvarId : MVarId) (inConv : Bool) : MetaM InteractiveGoal
         else
           ppVars varNames prevType? hyps localDecl
     let hyps ← pushPending varNames type? hyps
-    let goalTp ← getGoalTarget mvarDecl inConv
+    let goalTp ← instantiateMVars mvarDecl.type
     let goalFmt ← exprToInteractive goalTp
     let userName? := match mvarDecl.userName with
       | Name.anonymous => none