diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index b6f57cd777..f15f9b6179 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -456,11 +456,22 @@ def isPrefixOf [BEq α] : List α → List α → Bool
   | _,     []    => false
   | a::as, b::bs => a == b && isPrefixOf as bs
 
+/-- `isPrefixOf? l₁ l₂` returns `some t` when `l₂ == l₁ ++ t`. -/
+def isPrefixOf? [BEq α] : List α → List α → Option (List α)
+  | [], l₂ => some l₂
+  | _, [] => none
+  | (x₁ :: l₁), (x₂ :: l₂) =>
+    if x₁ == x₂ then isPrefixOf? l₁ l₂ else none
+
 /--  `isSuffixOf l₁ l₂` returns `true` Iff `l₁` is a suffix of `l₂`.
 That is, there exists a `t` such that `l₂ == t ++ l₁`. -/
 def isSuffixOf [BEq α] (l₁ l₂ : List α) : Bool :=
   isPrefixOf l₁.reverse l₂.reverse
 
+/-- `isSuffixOf? l₁ l₂` returns `some t` when `l₂ == t ++ l₁`.-/
+def isSuffixOf? [BEq α] (l₁ l₂ : List α) : Option (List α) :=
+  Option.map List.reverse <| isPrefixOf? l₁.reverse l₂.reverse
+
 @[specialize] def isEqv : List α → List α → (α → α → Bool) → Bool
   | [],    [],    _   => true
   | a::as, b::bs, eqv => eqv a b && isEqv as bs eqv
diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean
index 895628da58..2f996c6bcc 100644
--- a/src/Init/Data/Option/Basic.lean
+++ b/src/Init/Data/Option/Basic.lean
@@ -76,6 +76,14 @@ instance (r : α → α → Prop) [s : DecidableRel r] : DecidableRel (Option.lt
   | some _, none   => isFalse not_false
   | none,   none   => isFalse not_false
 
+/-- Take a pair of options and if they are both `some`, apply the given fn to produce an output.
+Otherwise act like `orElse`. -/
+def merge (fn : α → α → α) : Option α → Option α → Option α
+  | none  , none   => none
+  | some x, none   => some x
+  | none  , some y => some y
+  | some x, some y => some <| fn x y
+
 end Option
 
 deriving instance DecidableEq for Option
diff --git a/src/Lean/Data/RBMap.lean b/src/Lean/Data/RBMap.lean
index 4b0cc2f82b..4b8c3b987a 100644
--- a/src/Lean/Data/RBMap.lean
+++ b/src/Lean/Data/RBMap.lean
@@ -346,6 +346,9 @@ instance [Repr α] [Repr β] : Repr (RBMap α β cmp) where
 @[inline] def fromList (l : List (α × β)) (cmp : α → α → Ordering) : RBMap α β cmp :=
   l.foldl (fun r p => r.insert p.1 p.2) (mkRBMap α β cmp)
 
+@[inline] def fromArray (l : Array (α × β)) (cmp : α → α → Ordering) : RBMap α β cmp :=
+  l.foldl (fun r p => r.insert p.1 p.2) (mkRBMap α β cmp)
+
 /-- Returns true if the given predicate is true for all items in the RBMap. -/
 @[inline] def all : RBMap α β cmp → (α → β → Bool) → Bool
   | ⟨t, _⟩, p => t.all p
diff --git a/src/Lean/Data/RBTree.lean b/src/Lean/Data/RBTree.lean
index 87e1092a68..56f0adb358 100644
--- a/src/Lean/Data/RBTree.lean
+++ b/src/Lean/Data/RBTree.lean
@@ -89,6 +89,9 @@ instance [Repr α] : Repr (RBTree α cmp) where
 def fromList (l : List α) (cmp : α → α → Ordering) : RBTree α cmp :=
   l.foldl insert (mkRBTree α cmp)
 
+def fromArray (l : Array α) (cmp : α → α → Ordering) : RBTree α cmp :=
+  l.foldl insert (mkRBTree α cmp)
+
 @[inline] def all (t : RBTree α cmp) (p : α → Bool) : Bool :=
   RBMap.all t (fun a _ => p a)
 
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 61ba73ba62..dd9d83a8a3 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -896,6 +896,17 @@ def getForallBody : Expr → Expr
   | forallE _ _ b .. => getForallBody b
   | e                => e
 
+def getForallBodyMaxDepth : (maxDepth : Nat) → Expr → Expr
+  | (n+1), forallE _ _ b _ => getForallBodyMaxDepth n b
+  | 0, e => e
+  | _, e => e
+
+/-- Given a sequence of nested foralls `(a₁ : α₁) → ... → (aₙ : αₙ) → _`,
+returns the names `[a₁, ... aₙ]`. -/
+def getForallBinderNames : Expr → List Name
+  | forallE n _ b _ => n :: getForallBinderNames b
+  | _ => []
+
 /--
 If the given expression is a sequence of
 function applications `f a₁ .. aₙ`, return `f`.
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index b729eb980d..c35ce7b3e3 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -704,6 +704,11 @@ def getLocalDeclFromUserName (userName : Name) : MetaM LocalDecl := do
   | some d => pure d
   | none   => throwError "unknown local declaration '{userName}'"
 
+/-- Given a user-facing name for a free variable, return the free variable or throw if not declared. -/
+def getFVarFromUserName (userName : Name) : MetaM Expr := do
+  let d ← getLocalDeclFromUserName userName
+  return Expr.fvar d.fvarId
+
 /--
 Lift a `MkBindingM` monadic action `x` to `MetaM`.
 -/
diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index 5239201cb2..8330f6b471 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -47,7 +47,7 @@ structure State where
   /-- We attach `Elab.Info` at various locations in the `Syntax` output in order to convey
   its semantics. While the elaborator emits `InfoTree`s, here we have no real text location tree
   to traverse, so we use a flattened map. -/
-  infos    : Std.RBMap Pos Info compare := {}
+  infos    : PosMap Info := {}
   /-- See `SubExpr.nextExtraPos`. -/
   holeIter : SubExpr.HoleIterator := {}
 
@@ -268,10 +268,10 @@ to true or `pp.notation` is set to false, it will not be called at all.",
 
 end Delaborator
 
-open SubExpr (Pos)
+open SubExpr (Pos PosMap)
 open Delaborator (OptionsPerPos topDownAnalyze)
 
-def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab := Delaborator.delab) : MetaM (Term × Std.RBMap Pos Elab.Info compare) := do
+def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab := Delaborator.delab) : MetaM (Term × PosMap Elab.Info) := do
   /- Using `erasePatternAnnotations` here is a bit hackish, but we do it
      `Expr.mdata` affects the delaborator. TODO: should we fix that? -/
   let e ← Meta.erasePatternRefAnnotations e
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index 046dd113ef..c8488f0846 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -16,6 +16,7 @@ import Lean.Server.References
 import Lean.Server.GoTo
 
 import Lean.Widget.InteractiveGoal
+import Lean.Widget.Diff
 
 namespace Lean.Server.FileWorker
 open Lsp
@@ -162,11 +163,25 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
   withWaitFindSnap doc (fun s => s.endPos >= hoverPos)
     (notFoundX := return none) fun snap => do
       if let rs@(_ :: _) := snap.infoTree.goalsAt? doc.meta.text hoverPos then
-        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.withPPForTacticGoal (Widget.goalToInteractive g))
-        return some { goals := goals.toArray }
+        let goals : List Widget.InteractiveGoals ← rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } => do
+          let ciAfter := { ci with mctx := ti.mctxAfter }
+          let ci := if useAfter then ciAfter else { ci with mctx := ti.mctxBefore }
+          -- compute the interactive goals
+          let goals ← ci.runMetaM {} (do
+            let goals := List.toArray <| if useAfter then ti.goalsAfter else ti.goalsBefore
+            let goals ← goals.mapM (fun g => Meta.withPPForTacticGoal (Widget.goalToInteractive g))
+            return {goals}
+          )
+          -- compute the goal diff
+          let goals ← ciAfter.runMetaM {} (do
+              try
+                Widget.diffInteractiveGoals useAfter ti goals
+              catch _ =>
+                -- fail silently, since this is just a bonus feature
+                return goals
+          )
+          return goals
+        return some <| goals.foldl (· ++ ·) ∅
       else
         return none
 
@@ -174,7 +189,7 @@ open Elab in
 def handlePlainGoal (p : PlainGoalParams)
     : RequestM (RequestTask (Option PlainGoal)) := do
   let t ← getInteractiveGoals p
-  return t.map <| Except.map <| Option.map <| fun ⟨goals⟩ =>
+  return t.map <| Except.map <| Option.map <| fun {goals, ..} =>
     if goals.isEmpty then
       { goals := #[], rendered := "no goals" }
     else
diff --git a/src/Lean/SubExpr.lean b/src/Lean/SubExpr.lean
index 1d83194f4e..eb30cf6517 100644
--- a/src/Lean/SubExpr.lean
+++ b/src/Lean/SubExpr.lean
@@ -98,6 +98,14 @@ def pushNaryFn (numArgs : Nat) (p : Pos) : Pos :=
 def pushNaryArg (numArgs argIdx : Nat) (p : Pos) : Pos :=
   show Nat from p.asNat * (maxChildren ^ (numArgs - argIdx)) + 1
 
+def pushNthBindingDomain : (binderIdx : Nat) → Pos → Pos
+  | 0, p => p.pushBindingDomain
+  | (n+1), p => pushNthBindingDomain n p.pushBindingBody
+
+def pushNthBindingBody : (numBinders : Nat) → Pos → Pos
+  | 0, p => p
+  | (n+1), p => pushNthBindingBody n p.pushBindingBody
+
 protected def toString (p : Pos) : String :=
   p.toArray.toList
   |>.map toString
@@ -117,9 +125,18 @@ protected def fromString? : String → Except String Pos
     | "" :: tail => Pos.ofArray <$> tail.toArray.mapM ofStringCoord
     | ss => error s!"malformed {ss}"
 
+protected def fromString! (s : String) : Pos :=
+  match Pos.fromString? s with
+  | Except.ok a => a
+  | Except.error e => panic! e
+
 instance : Ord Pos := show Ord Nat by infer_instance
 instance : DecidableEq Pos := show DecidableEq Nat by infer_instance
 instance : ToString Pos := ⟨Pos.toString⟩
+instance : EmptyCollection Pos := ⟨root⟩
+instance : Repr Pos where
+  reprPrec p _ := f!"Pos.fromString! {repr p.toString}"
+
 
 -- Note: we can't send the bare Nat over the wire because Json will convert to float
 -- if the nat is too big and least significant bits will be lost.
@@ -150,6 +167,19 @@ def mkRoot (e : Expr) : SubExpr := ⟨e, Pos.root⟩
 /-- Returns true if the selected subexpression is the topmost one.-/
 def isRoot (s : SubExpr) : Bool := s.pos.isRoot
 
+/-- Map from subexpr positions to values. -/
+abbrev PosMap (α : Type u) := Std.RBMap Pos α compare
+
+def bindingBody! : SubExpr → SubExpr
+  | ⟨.forallE _ _ b _, p⟩ => ⟨b, p.pushBindingBody⟩
+  | ⟨.lam _ _ b _, p⟩ => ⟨b, p.pushBindingBody⟩
+  | _ => panic! "subexpr is not a binder"
+
+def bindingDomain! : SubExpr → SubExpr
+  | ⟨.forallE _ t _ _, p⟩ => ⟨t, p.pushBindingDomain⟩
+  | ⟨.lam _ t _ _, p⟩ => ⟨t, p.pushBindingDomain⟩
+  | _ => panic! "subexpr is not a binder"
+
 end SubExpr
 
 open SubExpr in
diff --git a/src/Lean/Widget/Diff.lean b/src/Lean/Widget/Diff.lean
new file mode 100644
index 0000000000..b4de3948ac
--- /dev/null
+++ b/src/Lean/Widget/Diff.lean
@@ -0,0 +1,270 @@
+/-
+Copyright (c) 2022 E.W.Ayers. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: E.W.Ayers
+-/
+import Lean.Meta.PPGoal
+import Lean.Widget.InteractiveCode
+import Lean.Widget.InteractiveGoal
+import Lean.Data.Lsp.Extra
+import Lean.Elab.InfoTree
+
+namespace Lean.Widget
+
+register_builtin_option showTacticDiff : Bool := {
+  defValue := true
+  descr := "When true, interactive goals for tactics will be decorated with diffing information. "
+}
+
+open Server Std Lean SubExpr
+
+/-- A marker for a point in the expression where a subexpression has been inserted.
+
+NOTE: in the future we may add other tags.
+  -/
+inductive ExprDiffTag where
+  | change
+  | delete
+
+def ExprDiffTag.toHighlightColor : (useAfter : Bool) → ExprDiffTag → HighlightColor
+  | true,  .change => .green
+  | false, .change => .yellow
+  | _,     .delete => .red
+
+def ExprDiffTag.toString : ExprDiffTag → String
+  | .change => "change"
+  | .delete => "delete"
+
+instance : ToString ExprDiffTag := ⟨ExprDiffTag.toString⟩
+
+/-- A description of the differences between a pair of expressions `before`, `after : Expr`.
+The information can be used to display a 'visual diff' for
+either `before`, showing the parts of the expression that are about to change,
+or `after` showing which parts of the expression have changed. -/
+structure ExprDiff where
+  /-- Map from subexpr positions in `e₀` to diff points.-/
+  changesBefore : PosMap ExprDiffTag := ∅
+  /-- A map from subexpr positions in `e₁` to 'diff points' which are tags
+  describing how the expression has changed relative to `before` at the given position.-/
+  changesAfter : PosMap ExprDiffTag := ∅
+
+instance : EmptyCollection ExprDiff := ⟨{}⟩
+instance : Append ExprDiff where
+  append a b := {
+    changesBefore := RBMap.mergeBy (fun _ _ b => b) a.changesBefore b.changesBefore,
+    changesAfter := RBMap.mergeBy (fun _ _ b => b) a.changesAfter b.changesAfter
+  }
+instance : ToString ExprDiff where
+  toString x :=
+    let f := fun (p : PosMap ExprDiffTag) =>
+      RBMap.toList p |>.map (fun (k,v) => s!"({toString k}:{toString v})")
+    s!"before: {f x.changesBefore}\nafter: {f x.changesAfter}"
+
+/-- Add a tag at the given position to the `changesBefore` dict. -/
+def ExprDiff.insertBeforeChange (p : Pos) (d : ExprDiffTag := .change) (δ : ExprDiff) : ExprDiff :=
+  {δ with changesBefore := δ.changesBefore.insert p d}
+
+/-- Add a tag at the given position to the `changesAfter` dict. -/
+def ExprDiff.insertAfterChange (p : Pos) (d : ExprDiffTag := .change) (δ : ExprDiff) : ExprDiff :=
+  {δ with changesAfter := δ.changesAfter.insert p d}
+
+def ExprDiff.withChangePos (before after : Pos) (d : ExprDiffTag := .change) : ExprDiff :=
+  { changesAfter := RBMap.empty.insert after d
+    changesBefore := RBMap.empty.insert before d
+  }
+
+/-- Add a tag to the diff at the positions given by `before` and `after`. -/
+def ExprDiff.withChange (before after : SubExpr) (d : ExprDiffTag := .change) : ExprDiff :=
+  ExprDiff.withChangePos before.pos after.pos d
+
+/-- If true, the expression before and the expression after are identical. -/
+def ExprDiff.isEmpty (d : ExprDiff) : Bool :=
+  d.changesAfter.isEmpty ∧ d.changesBefore.isEmpty
+
+/-- Computes a diff between `before` and `after` expressions.
+
+This works by recursively comparing function arguments.
+
+TODO(ed): experiment with a 'greatest common subexpression' design where
+  given `e₀`, `e₁`, find the greatest common subexpressions `Xs : Array Expr` and a congruence `F` such that
+  `e₀ = F[A₀[..Xs]]` and `e₀ = F[A₁[..Xs]]`. Then, we can have fancy diff highlighting where common subexpressions are not highlighted.
+
+## Diffing binders
+
+Two binding domains are identified if they have the same user name and the same type.
+The most common tactic that modifies binders is after an `intros`.
+To deal with this case, if `before = (a : α) → β` and `after`, is not a matching binder (ie: not `(a : α) → _`)
+then we instantiate the `before` variable in a new context and continue diffing `β` against `after`.
+
+ -/
+partial def exprDiffCore (before after : SubExpr) : MetaM ExprDiff := do
+  if before.expr == after.expr then
+    return ∅
+  match before.expr, after.expr with
+  | .app .., .app .. =>
+    let (fn₀, args₀) := after.expr.withApp Prod.mk
+    let (fn₁, args₁) := before.expr.withApp Prod.mk
+    if fn₀ != fn₁ || args₀.size != args₁.size then
+      return ExprDiff.withChange before after
+    let args := Array.zip args₀ args₁
+    let args ← args.mapIdxM (fun i (beforeArg, afterArg) =>
+      exprDiffCore
+        ⟨beforeArg, before.pos.pushNaryArg args₀.size i⟩
+        ⟨afterArg,  after.pos.pushNaryArg  args₀.size i⟩
+    )
+    return args.foldl (init := ∅) (· ++ ·)
+  | .forallE .., _ => piDiff before after
+  | .lam n₀ d₀ b₀ i₀, .lam n₁ d₁ b₁ i₁=>
+    if n₀ != n₁ || i₀ != i₁ then
+      return ExprDiff.withChange before after
+    let δd ← exprDiffCore ⟨d₀, before.pos.pushBindingDomain⟩ ⟨d₁, after.pos.pushBindingDomain⟩
+    if δd.isEmpty then
+      return ← exprDiffCore ⟨b₀, before.pos.pushBindingBody⟩ ⟨b₁, after.pos.pushBindingBody⟩
+    else
+      return δd ++ ExprDiff.withChangePos before.pos.pushBindingBody after.pos.pushBindingBody
+  | _, _ => return ExprDiff.withChange before after
+  where
+    piDiff (before after : SubExpr) : MetaM ExprDiff := do
+      let .forallE n₀ d₀ b₀ i₀ := before.expr
+        | return ∅
+      if let .forallE n₁ d₁ b₁ i₁ := after.expr then
+        if n₀ == n₁ && i₀ == i₁ then
+          -- assume that these are the same binders
+          let δd ← exprDiffCore
+            ⟨d₀, before.pos.pushBindingDomain⟩
+            ⟨d₁, after.pos.pushBindingDomain⟩
+          if δd.isEmpty then
+            -- the types have changed, so we can no longer meaningfully compare the targets
+            let δt ← Lean.Meta.withLocalDecl n₀ i₀ d₀ fun x =>
+              exprDiffCore
+                ⟨b₀.instantiate1 x, before.pos.pushBindingBody⟩
+                ⟨b₁.instantiate1 x, after.pos.pushBindingBody⟩
+            return δt
+          else
+            return δd ++ ExprDiff.withChangePos before.pos.pushBindingBody after.pos.pushBindingBody
+      -- in this case, the after expression does not match the before expression.
+      -- however, a special case is intros:
+      if let some s := List.isSuffixOf? after.expr.getForallBinderNames before.expr.getForallBinderNames then
+        -- s ++ namesAfter = namesBefore
+        if s.length == 0 then
+          throwError "should not happen"
+        let body₀ := before.expr.getForallBodyMaxDepth s.length
+        let mut δ : ExprDiff ← (do
+          -- this line can fail if we are using `before`'s mvar context, in which case
+          -- we can skip giving a diff.
+          let fvars ← s.mapM Lean.Meta.getFVarFromUserName
+          return ← exprDiffCore
+            ⟨body₀.instantiateRev fvars.toArray, before.pos.pushNthBindingBody s.length⟩
+            after
+        ) <|> (pure ∅)
+        for i in [0:s.length] do
+          δ := δ.insertBeforeChange (before.pos.pushNthBindingDomain i) .delete
+        -- [todo] maybe here insert a tag on the after case indicating an expression was deleted above the expression?
+        return δ
+      return ExprDiff.withChange before after
+
+/-- Computes the diff for `e₀` and `e₁`. If `useAfter` is `false`, `e₀, e₁` are interpreted as `after, before` instead of `before, after`.-/
+def exprDiff (e₀ e₁ : Expr) (useAfter := true) : MetaM ExprDiff := do
+  let s₀ := ⟨e₀, Pos.root⟩
+  let s₁ := ⟨e₁, Pos.root⟩
+  if useAfter then
+    exprDiffCore s₀ s₁
+  else
+    exprDiffCore s₁ s₀
+
+/-- Given a `diff` between `before` and `after : Expr`, and the rendered `infoAfter : CodeWithInfos` for `after`,
+this function decorates `infoAfter` with tags indicating where the expression has changed.
+
+If `useAfter == false` before and after are swapped. -/
+def addDiffTags (useAfter : Bool) (diff : ExprDiff) (info₁ : CodeWithInfos) : MetaM CodeWithInfos := do
+  let cs := if useAfter then diff.changesAfter else diff.changesBefore
+  info₁.mergePosMap (fun info d => pure <| info.highlight <| d.toHighlightColor useAfter) cs
+
+open Meta
+
+/-- Diffs the given hypothesis bundle against the given local context.
+
+If `useAfter == true`, `ctx₀` is the context _before_ and `h₁` is the bundle _after_.
+If `useAfter == false`, these are swapped.
+ -/
+def diffHypothesesBundle (useAfter : Bool) (ctx₀  : LocalContext) (h₁ : InteractiveHypothesisBundle) : MetaM InteractiveHypothesisBundle := do
+  /- Strategy: we say a hypothesis has mutated if the ppName is the same but the fvarid has changed.
+     this indicates that something like `rewrite at` has hit it. -/
+  for (ppName, fvid) in Array.zip h₁.names h₁.fvarIds do
+    if !(ctx₀.contains fvid) then
+      if let some decl₀ := ctx₀.findFromUserName? ppName then
+        -- on ctx₀ there is an fvar with the same name as this one.
+        let t₀ := decl₀.type
+        return ← withTypeDiff t₀ h₁
+      else
+        if useAfter then
+          return {h₁ with isInserted? := true }
+        else
+          return {h₁ with isRemoved? := true }
+  -- all fvids are present on original so we can assume no change.
+  return h₁
+where
+  withTypeDiff (t₀ : Expr) (h₁ : InteractiveHypothesisBundle) : MetaM InteractiveHypothesisBundle := do
+    let some x₁ := h₁.fvarIds[0]?
+      | throwError "internal error: empty fvar list!"
+    let t₁ ← inferType <| Expr.fvar x₁
+    let tδ ← exprDiff t₀ t₁ useAfter
+    let c₁ ← addDiffTags useAfter tδ h₁.type
+    return {h₁ with type := c₁}
+
+def diffHypotheses (useAfter : Bool) (lctx₀ : LocalContext) (hs₁ : Array InteractiveHypothesisBundle) : MetaM (Array InteractiveHypothesisBundle) := do
+  -- [todo] also show when hypotheses (user-names present in lctx₀ but not in hs₁) are deleted
+  hs₁.mapM (diffHypothesesBundle useAfter lctx₀)
+
+/-- Decorates the given goal `i₁` with a diff by comparing with goal `g₀`.
+If `useAfter` is true then `i₁` is _after_ and `g₀` is _before_. Otherwise they are swapped. -/
+def diffInteractiveGoal (useAfter : Bool) (g₀ : MVarId) (i₁ : InteractiveGoal) : MetaM InteractiveGoal := do
+  let mctx ← getMCtx
+  let some md₀ := mctx.findDecl? g₀
+    | throwError "Failed to find decl for {g₀}."
+  let lctx₀ := md₀.lctx |>.sanitizeNames.run' {options := (← getOptions)}
+  let hs₁ ← diffHypotheses useAfter lctx₀ i₁.hyps
+  let i₁ := {i₁ with hyps := hs₁}
+  let some g₁ := i₁.mvarId?
+    | throwError "Expected InteractiveGoal to have an mvarId"
+  let t₀ ← instantiateMVars <|← inferType (Expr.mvar g₀)
+  let some md₁ := (← getMCtx).findDecl? g₁
+    | throwError "Unknown goal {g₁}"
+  let t₁ ← instantiateMVars md₁.type
+  let tδ ← exprDiff t₀ t₁ useAfter
+  let c₁ ← addDiffTags useAfter tδ i₁.type
+  let i₁ := {i₁ with type := c₁, isInserted? := false}
+  return i₁
+
+/-- Modifies `goalsAfter` with additional information about how it is different to `goalsBefore`.
+If `useAfter` is `true` then `igs₁` is the set of interactive goals _after_ the tactic has been applied.
+Otherwise `igs₁` is the set of interactive goals _before_. -/
+def diffInteractiveGoals (useAfter : Bool) (info : Elab.TacticInfo) (igs₁ : InteractiveGoals) : MetaM InteractiveGoals := do
+    if ! showTacticDiff.get (← getOptions) then return igs₁ else
+    let goals₀ := if useAfter then info.goalsBefore else info.goalsAfter
+    let parentMap : MVarIdMap MVarIdSet ← info.goalsBefore.foldlM (init := ∅) (fun s g => do
+      let ms ← Expr.mvar g |> Lean.Meta.getMVars
+      let ms : MVarIdSet := RBTree.fromArray ms _
+      return s.insert g ms
+    )
+    let isParent (before after : MVarId) : Bool :=
+       match parentMap.find? before with
+       | some xs => xs.contains after
+       | none => false
+    let goals ← igs₁.goals.mapM (fun ig₁ => do
+      let some g₁ := ig₁.mvarId?
+        | throwError "error: goal not found"
+      withGoalCtx (g₁ : MVarId) (fun _lctx₁ _md₁ => do
+        -- if the goal is present on the previous version then continue
+        if goals₀.any (fun g₀ => g₀ == g₁) then
+          return {ig₁ with isInserted? := none}
+        let some g₀ := goals₀.find? (fun g₀ => if useAfter then isParent g₀ g₁ else isParent g₁ g₀)
+          | return if useAfter then {ig₁ with isInserted? := true } else {ig₁ with isRemoved? := true}
+        let ig₁ ← diffInteractiveGoal useAfter g₀ ig₁
+        return ig₁
+      )
+    )
+    return {igs₁ with goals := goals}
+
+end Lean.Widget
diff --git a/src/Lean/Widget/InteractiveCode.lean b/src/Lean/Widget/InteractiveCode.lean
index 9529107253..30ffb6a991 100644
--- a/src/Lean/Widget/InteractiveCode.lean
+++ b/src/Lean/Widget/InteractiveCode.lean
@@ -15,6 +15,14 @@ with environment and subexpression information. -/
 namespace Lean.Widget
 open Server
 
+inductive HighlightColor where
+  | green
+  | blue
+  | red
+  | yellow
+  | purple
+  deriving ToJson, FromJson
+
 /-- Information about a subexpression within delaborated code. -/
 structure SubexprInfo where
   /-- The `Elab.Info` node with the semantics of this part of the output. -/
@@ -24,16 +32,29 @@ structure SubexprInfo where
   subexprPos : Lean.SubExpr.Pos
   -- TODO(WN): add fields for semantic highlighting
   -- kind : Lsp.SymbolKind
+  /-- Ask the renderer to highlight this node in the given color. -/
+  highlightColor? : Option HighlightColor := none
   deriving Inhabited, RpcEncodable
 
 /-- Pretty-printed syntax (usually but not necessarily an `Expr`) with embedded `Info`s. -/
 abbrev CodeWithInfos := TaggedText SubexprInfo
 
+def CodeWithInfos.mergePosMap [Monad m] (merger : SubexprInfo → α → m SubexprInfo) (pm : Lean.SubExpr.PosMap α) (tt : CodeWithInfos) : m CodeWithInfos :=
+  if pm.isEmpty then return tt else
+  tt.mapM (fun (info : SubexprInfo) =>
+    match pm.find? info.subexprPos with
+    | some a => merger info a
+    | none => pure info
+  )
+
 def CodeWithInfos.pretty (tt : CodeWithInfos) :=
   tt.stripTags
 
+def SubexprInfo.highlight (color : HighlightColor) (c : SubexprInfo) : SubexprInfo :=
+  {c with highlightColor? := some color }
+
 /-- Tags a pretty-printed `Expr` with infos from the delaborator. -/
-partial def tagExprInfos (ctx : Elab.ContextInfo) (infos : Std.RBMap Nat Elab.Info compare) (tt : TaggedText (Nat × Nat))
+partial def tagExprInfos (ctx : Elab.ContextInfo) (infos : SubExpr.PosMap Elab.Info) (tt : TaggedText (Nat × Nat))
     : CodeWithInfos :=
   go tt
 where
@@ -41,7 +62,12 @@ where
     tt.rewrite fun (n, _) subTt =>
       match infos.find? n with
       | none   => go subTt
-      | some i => TaggedText.tag ⟨WithRpcRef.mk { ctx, info := i }, n⟩ (go subTt)
+      | some i =>
+        let t : SubexprInfo := {
+          info := WithRpcRef.mk { ctx, info := i }
+          subexprPos := n
+        }
+        TaggedText.tag t (go subTt)
 
 def ppExprTagged (e : Expr) (explicit : Bool := false) : MetaM CodeWithInfos := do
   let delab := open PrettyPrinter.Delaborator in
diff --git a/src/Lean/Widget/InteractiveGoal.lean b/src/Lean/Widget/InteractiveGoal.lean
index bc00558b43..45b63ec1c4 100644
--- a/src/Lean/Widget/InteractiveGoal.lean
+++ b/src/Lean/Widget/InteractiveGoal.lean
@@ -13,15 +13,27 @@ import Lean.Data.Lsp.Extra
 namespace Lean.Widget
 open Server
 
+/-- In the infoview, if multiple hypotheses `h₁`, `h₂` have the same type `α`, they are rendered as `h₁ h₂ : α`.
+We call this a 'hypothesis bundle'. -/
 structure InteractiveHypothesisBundle where
   /-- The user-friendly name for each hypothesis.
   If anonymous then the name is inaccessible and hidden. -/
   names : Array Name
+  /-- The ids for each variable. Should have the same length as `names`. -/
   fvarIds : Array FVarId
   type : CodeWithInfos
+  /-- The value, in the case the hypothesis is a `let`-binder. -/
   val? : Option CodeWithInfos := none
+  /-- The hypothesis is a typeclass instance. -/
   isInstance : Bool
+  /-- The hypothesis is a type. -/
   isType : Bool
+  /-- If true, the hypothesis was not present on the previous tactic state.
+      Uses `none` instead of `some false` to save space in the json encoding. -/
+  isInserted? : Option Bool := none
+  /-- If true, the hypothesis will be removed in the next tactic state.
+      Uses `none` instead of `some false` to save space in the json encoding.  -/
+  isRemoved?  : Option Bool := none
   deriving Inhabited, RpcEncodable
 
 structure InteractiveGoal where
@@ -33,6 +45,12 @@ structure InteractiveGoal where
   name of the MVar that it is a goal for.)
   This is none when we are showing a term goal. -/
   mvarId? : Option MVarId := none
+  /-- If true, the goal was not present on the previous tactic state.
+      Uses `none` instead of `some false` to save space in the json encoding.  -/
+  isInserted?: Option Bool := none
+  /-- If true, the goal will be removed on the next tactic state.
+      Uses `none` instead of `some false` to save space in the json encoding. -/
+  isRemoved? : Option Bool := none
   deriving Inhabited, RpcEncodable
 
 namespace InteractiveGoal
@@ -66,6 +84,7 @@ def pretty (g : InteractiveGoal) : Format := Id.run do
 
 end InteractiveGoal
 
+/-- This is everything needed to render an interactive term goal in the infoview. -/
 structure InteractiveTermGoal where
   hyps      : Array InteractiveHypothesisBundle
   type      : CodeWithInfos
@@ -83,6 +102,12 @@ structure InteractiveGoals where
   goals : Array InteractiveGoal
   deriving RpcEncodable
 
+def InteractiveGoals.append (l r : InteractiveGoals) : InteractiveGoals where
+  goals := l.goals ++ r.goals
+
+instance : Append InteractiveGoals := ⟨InteractiveGoals.append⟩
+instance : EmptyCollection InteractiveGoals := ⟨{goals := #[]}⟩
+
 open Meta in
 def addInteractiveHypothesisBundle (hyps : Array InteractiveHypothesisBundle) (ids : Array (Name × FVarId)) (type : Expr) (value? : Option Expr := none) : MetaM (Array InteractiveHypothesisBundle) := do
   if ids.size == 0 then
@@ -98,16 +123,22 @@ def addInteractiveHypothesisBundle (hyps : Array InteractiveHypothesisBundle) (i
     isType     := (← instantiateMVars type).isSort
   }
 
+open Meta in
+variable [MonadControlT MetaM n] [Monad n] [MonadError n] [MonadOptions n] [MonadMCtx n] in
+def withGoalCtx (goal : MVarId) (action : LocalContext → MetavarDecl → n α) : n α := do
+  let mctx ← getMCtx
+  let some mvarDecl := mctx.findDecl? goal
+    | throwError "unknown goal {goal.name}"
+  let lctx := mvarDecl.lctx |>.sanitizeNames.run' {options := (← getOptions)}
+  withLCtx lctx mvarDecl.localInstances (action lctx mvarDecl)
+
+
 open Meta in
 /-- A variant of `Meta.ppGoal` which preserves subexpression information for interactivity. -/
 def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
-  let some mvarDecl := (← getMCtx).findDecl? mvarId
-    | throwError "unknown goal {mvarId.name}"
   let ppAuxDecls := pp.auxDecls.get (← getOptions)
   let showLetValues := pp.showLetValues.get (← getOptions)
-  let lctx := mvarDecl.lctx
-  let lctx : LocalContext := lctx.sanitizeNames.run' { options := (← getOptions) }
-  withLCtx lctx mvarDecl.localInstances do
+  withGoalCtx mvarId fun lctx mvarDecl => do
     let (hidden, hiddenProp) ← ToHide.collect mvarDecl.type
     let pushPending (ids : Array (Name × FVarId)) (type? : Option Expr) (hyps : Array InteractiveHypothesisBundle)
         : MetaM (Array InteractiveHypothesisBundle) :=
diff --git a/tests/lean/interactive/Diff.lean b/tests/lean/interactive/Diff.lean
new file mode 100644
index 0000000000..4631737d41
--- /dev/null
+++ b/tests/lean/interactive/Diff.lean
@@ -0,0 +1,35 @@
+
+def hello : (x : Nat) → (h : x = x) → True := by
+  intro x
+  --^ goals
+  intro
+--^ goals
+  trivial
+
+def hello2 : (x : Nat) → (h : x = x) → True := by
+  intros
+--^ goals
+  trivial
+
+
+theorem qqww (x y : Nat) (f : (α → x = y)) (h : y = x) : True := by
+  rw [h] at f
+   --^ goals
+  trivial
+
+theorem qqww2 (x y : Nat) (f : (α → x = y)) (h : y = x) : True := by
+  rw [h] at f
+       --^ goals
+  trivial
+
+theorem adsf : (True ∧ True) := by
+  apply And.intro
+--^ goals
+  trivial
+--^ goals
+  trivial
+--^ goals
+
+theorem comm (x y z : Nat) (h : y = x) : (x + z) = (z + y) := by
+  rw [Nat.add_comm, h]
+    --^ goals
diff --git a/tests/lean/interactive/Diff.lean.expected.out b/tests/lean/interactive/Diff.lean.expected.out
new file mode 100644
index 0000000000..0439b6d1df
--- /dev/null
+++ b/tests/lean/interactive/Diff.lean.expected.out
@@ -0,0 +1,267 @@
+{ goals := #[{ type := Lean.Widget.TaggedText.tag
+                         { subexprPos := "/", highlightColor? := none }
+                         (Lean.Widget.TaggedText.append
+                           #[Lean.Widget.TaggedText.tag
+                               { subexprPos := "/0", highlightColor? := none }
+                               (Lean.Widget.TaggedText.append
+                                 #[Lean.Widget.TaggedText.tag
+                                     { subexprPos := "/0/0/1", highlightColor? := none }
+                                     (Lean.Widget.TaggedText.text "x"),
+                                   Lean.Widget.TaggedText.text " = ",
+                                   Lean.Widget.TaggedText.tag
+                                     { subexprPos := "/0/1", highlightColor? := none }
+                                     (Lean.Widget.TaggedText.text "x")]),
+                             Lean.Widget.TaggedText.text " → ",
+                             Lean.Widget.TaggedText.tag
+                               { subexprPos := "/1", highlightColor? := none }
+                               (Lean.Widget.TaggedText.text "True")]),
+               isInserted? := some false,
+               isRemoved? := none,
+               hyps := #[{ type := Lean.Widget.TaggedText.tag
+                                     { subexprPos := "/", highlightColor? := none }
+                                     (Lean.Widget.TaggedText.text "Nat"),
+                           names := #["x"],
+                           isInserted? := some true,
+                           isRemoved? := none }] }] }
+
+{ goals := #[{ type := Lean.Widget.TaggedText.tag
+                         { subexprPos := "/", highlightColor? := none }
+                         (Lean.Widget.TaggedText.append
+                           #[Lean.Widget.TaggedText.tag
+                               { subexprPos := "/0", highlightColor? := some "red" }
+                               (Lean.Widget.TaggedText.append
+                                 #[Lean.Widget.TaggedText.tag
+                                     { subexprPos := "/0/0/1", highlightColor? := none }
+                                     (Lean.Widget.TaggedText.text "x"),
+                                   Lean.Widget.TaggedText.text " = ",
+                                   Lean.Widget.TaggedText.tag
+                                     { subexprPos := "/0/1", highlightColor? := none }
+                                     (Lean.Widget.TaggedText.text "x")]),
+                             Lean.Widget.TaggedText.text " → ",
+                             Lean.Widget.TaggedText.tag
+                               { subexprPos := "/1", highlightColor? := none }
+                               (Lean.Widget.TaggedText.text "True")]),
+               isInserted? := some false,
+               isRemoved? := none,
+               hyps := #[{ type := Lean.Widget.TaggedText.tag
+                                     { subexprPos := "/", highlightColor? := none }
+                                     (Lean.Widget.TaggedText.text "Nat"),
+                           names := #["x"],
+                           isInserted? := none,
+                           isRemoved? := none }] }] }
+
+{ goals := #[{ type := Lean.Widget.TaggedText.tag
+                         { subexprPos := "/", highlightColor? := none }
+                         (Lean.Widget.TaggedText.append
+                           #[Lean.Widget.TaggedText.text "∀ (",
+                             Lean.Widget.TaggedText.tag
+                               { subexprPos := "/", highlightColor? := none }
+                               (Lean.Widget.TaggedText.text "x"),
+                             Lean.Widget.TaggedText.text " : ",
+                             Lean.Widget.TaggedText.tag
+                               { subexprPos := "/0", highlightColor? := some "red" }
+                               (Lean.Widget.TaggedText.text "Nat"),
+                             Lean.Widget.TaggedText.text "), ",
+                             Lean.Widget.TaggedText.tag
+                               { subexprPos := "/1", highlightColor? := none }
+                               (Lean.Widget.TaggedText.append
+                                 #[Lean.Widget.TaggedText.tag
+                                     { subexprPos := "/1/0", highlightColor? := some "red" }
+                                     (Lean.Widget.TaggedText.append
+                                       #[Lean.Widget.TaggedText.tag
+                                           { subexprPos := "/1/0/0/1", highlightColor? := none }
+                                           (Lean.Widget.TaggedText.text "x"),
+                                         Lean.Widget.TaggedText.text " = ",
+                                         Lean.Widget.TaggedText.tag
+                                           { subexprPos := "/1/0/1", highlightColor? := none }
+                                           (Lean.Widget.TaggedText.text "x")]),
+                                   Lean.Widget.TaggedText.text " → ",
+                                   Lean.Widget.TaggedText.tag
+                                     { subexprPos := "/1/1", highlightColor? := none }
+                                     (Lean.Widget.TaggedText.text "True")])]),
+               isInserted? := some false,
+               isRemoved? := none,
+               hyps := #[] }] }
+
+{ goals := #[{ type := Lean.Widget.TaggedText.tag
+                         { subexprPos := "/", highlightColor? := none }
+                         (Lean.Widget.TaggedText.text "True"),
+               isInserted? := some false,
+               isRemoved? := none,
+               hyps := #[{ type := Lean.Widget.TaggedText.tag
+                                     { subexprPos := "/", highlightColor? := none }
+                                     (Lean.Widget.TaggedText.text "Sort u_1"),
+                           names := #["α"],
+                           isInserted? := none,
+                           isRemoved? := none },
+                         { type := Lean.Widget.TaggedText.tag
+                                     { subexprPos := "/", highlightColor? := none }
+                                     (Lean.Widget.TaggedText.text "Nat"),
+                           names := #["x", "y"],
+                           isInserted? := none,
+                           isRemoved? := none },
+                         { type := Lean.Widget.TaggedText.tag
+                                     { subexprPos := "/", highlightColor? := none }
+                                     (Lean.Widget.TaggedText.append
+                                       #[Lean.Widget.TaggedText.tag
+                                           { subexprPos := "/0", highlightColor? := none }
+                                           (Lean.Widget.TaggedText.text "α"),
+                                         Lean.Widget.TaggedText.text " → ",
+                                         Lean.Widget.TaggedText.tag
+                                           { subexprPos := "/1", highlightColor? := none }
+                                           (Lean.Widget.TaggedText.append
+                                             #[Lean.Widget.TaggedText.tag
+                                                 { subexprPos := "/1/0/1", highlightColor? := none }
+                                                 (Lean.Widget.TaggedText.text "x"),
+                                               Lean.Widget.TaggedText.text " = ",
+                                               Lean.Widget.TaggedText.tag
+                                                 { subexprPos := "/1/1", highlightColor? := some "yellow" }
+                                                 (Lean.Widget.TaggedText.text "y")])]),
+                           names := #["f"],
+                           isInserted? := none,
+                           isRemoved? := none },
+                         { type := Lean.Widget.TaggedText.tag
+                                     { subexprPos := "/", highlightColor? := none }
+                                     (Lean.Widget.TaggedText.append
+                                       #[Lean.Widget.TaggedText.tag
+                                           { subexprPos := "/0/1", highlightColor? := none }
+                                           (Lean.Widget.TaggedText.text "y"),
+                                         Lean.Widget.TaggedText.text " = ",
+                                         Lean.Widget.TaggedText.tag
+                                           { subexprPos := "/1", highlightColor? := none }
+                                           (Lean.Widget.TaggedText.text "x")]),
+                           names := #["h"],
+                           isInserted? := none,
+                           isRemoved? := none }] }] }
+
+{ goals := #[{ type := Lean.Widget.TaggedText.tag
+                         { subexprPos := "/", highlightColor? := none }
+                         (Lean.Widget.TaggedText.text "True"),
+               isInserted? := some false,
+               isRemoved? := none,
+               hyps := #[{ type := Lean.Widget.TaggedText.tag
+                                     { subexprPos := "/", highlightColor? := none }
+                                     (Lean.Widget.TaggedText.text "Sort u_1"),
+                           names := #["α"],
+                           isInserted? := none,
+                           isRemoved? := none },
+                         { type := Lean.Widget.TaggedText.tag
+                                     { subexprPos := "/", highlightColor? := none }
+                                     (Lean.Widget.TaggedText.text "Nat"),
+                           names := #["x", "y"],
+                           isInserted? := none,
+                           isRemoved? := none },
+                         { type := Lean.Widget.TaggedText.tag
+                                     { subexprPos := "/", highlightColor? := none }
+                                     (Lean.Widget.TaggedText.append
+                                       #[Lean.Widget.TaggedText.tag
+                                           { subexprPos := "/0", highlightColor? := none }
+                                           (Lean.Widget.TaggedText.text "α"),
+                                         Lean.Widget.TaggedText.text " → ",
+                                         Lean.Widget.TaggedText.tag
+                                           { subexprPos := "/1", highlightColor? := none }
+                                           (Lean.Widget.TaggedText.append
+                                             #[Lean.Widget.TaggedText.tag
+                                                 { subexprPos := "/1/0/1", highlightColor? := none }
+                                                 (Lean.Widget.TaggedText.text "x"),
+                                               Lean.Widget.TaggedText.text " = ",
+                                               Lean.Widget.TaggedText.tag
+                                                 { subexprPos := "/1/1", highlightColor? := some "green" }
+                                                 (Lean.Widget.TaggedText.text "x")])]),
+                           names := #["f"],
+                           isInserted? := none,
+                           isRemoved? := none },
+                         { type := Lean.Widget.TaggedText.tag
+                                     { subexprPos := "/", highlightColor? := none }
+                                     (Lean.Widget.TaggedText.append
+                                       #[Lean.Widget.TaggedText.tag
+                                           { subexprPos := "/0/1", highlightColor? := none }
+                                           (Lean.Widget.TaggedText.text "y"),
+                                         Lean.Widget.TaggedText.text " = ",
+                                         Lean.Widget.TaggedText.tag
+                                           { subexprPos := "/1", highlightColor? := none }
+                                           (Lean.Widget.TaggedText.text "x")]),
+                           names := #["h"],
+                           isInserted? := none,
+                           isRemoved? := none }] }] }
+
+{ goals := #[{ type := Lean.Widget.TaggedText.tag
+                         { subexprPos := "/", highlightColor? := some "yellow" }
+                         (Lean.Widget.TaggedText.append
+                           #[Lean.Widget.TaggedText.tag
+                               { subexprPos := "/0/1", highlightColor? := none }
+                               (Lean.Widget.TaggedText.text "True"),
+                             Lean.Widget.TaggedText.text " ∧ ",
+                             Lean.Widget.TaggedText.tag
+                               { subexprPos := "/1", highlightColor? := none }
+                               (Lean.Widget.TaggedText.text "True")]),
+               isInserted? := some false,
+               isRemoved? := none,
+               hyps := #[] }] }
+
+{ goals := #[{ type := Lean.Widget.TaggedText.tag
+                         { subexprPos := "/", highlightColor? := none }
+                         (Lean.Widget.TaggedText.text "True"),
+               isInserted? := none,
+               isRemoved? := some true,
+               hyps := #[] },
+             { type := Lean.Widget.TaggedText.tag
+                         { subexprPos := "/", highlightColor? := none }
+                         (Lean.Widget.TaggedText.text "True"),
+               isInserted? := none,
+               isRemoved? := none,
+               hyps := #[] }] }
+
+{ goals := #[{ type := Lean.Widget.TaggedText.tag
+                         { subexprPos := "/", highlightColor? := none }
+                         (Lean.Widget.TaggedText.text "True"),
+               isInserted? := none,
+               isRemoved? := some true,
+               hyps := #[] }] }
+
+{ goals := #[{ type := Lean.Widget.TaggedText.tag
+                         { subexprPos := "/", highlightColor? := none }
+                         (Lean.Widget.TaggedText.append
+                           #[Lean.Widget.TaggedText.tag
+                               { subexprPos := "/0/1", highlightColor? := none }
+                               (Lean.Widget.TaggedText.append
+                                 #[Lean.Widget.TaggedText.tag
+                                     { subexprPos := "/0/1/0/1", highlightColor? := some "yellow" }
+                                     (Lean.Widget.TaggedText.text "x"),
+                                   Lean.Widget.TaggedText.text " + ",
+                                   Lean.Widget.TaggedText.tag
+                                     { subexprPos := "/0/1/1", highlightColor? := some "yellow" }
+                                     (Lean.Widget.TaggedText.text "z")]),
+                             Lean.Widget.TaggedText.text " = ",
+                             Lean.Widget.TaggedText.tag
+                               { subexprPos := "/1", highlightColor? := none }
+                               (Lean.Widget.TaggedText.append
+                                 #[Lean.Widget.TaggedText.tag
+                                     { subexprPos := "/1/0/1", highlightColor? := none }
+                                     (Lean.Widget.TaggedText.text "z"),
+                                   Lean.Widget.TaggedText.text " + ",
+                                   Lean.Widget.TaggedText.tag
+                                     { subexprPos := "/1/1", highlightColor? := none }
+                                     (Lean.Widget.TaggedText.text "y")])]),
+               isInserted? := some false,
+               isRemoved? := none,
+               hyps := #[{ type := Lean.Widget.TaggedText.tag
+                                     { subexprPos := "/", highlightColor? := none }
+                                     (Lean.Widget.TaggedText.text "Nat"),
+                           names := #["x", "y", "z"],
+                           isInserted? := none,
+                           isRemoved? := none },
+                         { type := Lean.Widget.TaggedText.tag
+                                     { subexprPos := "/", highlightColor? := none }
+                                     (Lean.Widget.TaggedText.append
+                                       #[Lean.Widget.TaggedText.tag
+                                           { subexprPos := "/0/1", highlightColor? := none }
+                                           (Lean.Widget.TaggedText.text "y"),
+                                         Lean.Widget.TaggedText.text " = ",
+                                         Lean.Widget.TaggedText.tag
+                                           { subexprPos := "/1", highlightColor? := none }
+                                           (Lean.Widget.TaggedText.text "x")]),
+                           names := #["h"],
+                           isInserted? := none,
+                           isRemoved? := none }] }] }
+
diff --git a/tests/lean/interactive/run.lean b/tests/lean/interactive/run.lean
index f25346d91a..422cb0360c 100644
--- a/tests/lean/interactive/run.lean
+++ b/tests/lean/interactive/run.lean
@@ -4,6 +4,35 @@ open Lean
 open Lean.Lsp
 open Lean.JsonRpc
 
+namespace Client
+
+/- Client-side types for showing interactive goals. -/
+
+structure SubexprInfo where
+  subexprPos : String
+  highlightColor? : Option String
+  deriving FromJson, Repr
+
+structure Hyp where
+  type : Widget.TaggedText SubexprInfo
+  names : Array String
+  isInserted?: Option Bool
+  isRemoved?: Option Bool
+  deriving FromJson, Repr
+
+structure InteractiveGoal where
+  type : Widget.TaggedText SubexprInfo
+  isInserted?: Option Bool := none
+  isRemoved?: Option Bool := none
+  hyps : Array Hyp
+  deriving FromJson, Repr
+
+structure InteractiveGoals where
+  goals : Array InteractiveGoal
+  deriving FromJson, Repr
+
+end Client
+
 def word : Parsec String :=
   Parsec.many1Chars <| Parsec.digit <|> Parsec.asciiLetter <|> Parsec.pchar '_'
 
@@ -78,6 +107,28 @@ partial def main (args : List String) : IO Unit := do
           for diag in diags do
             IO.eprintln (toJson diag.param)
           requestNo := requestNo + 1
+        | "goals" =>
+          if rpcSessionId.isNone then
+            Ipc.writeRequest ⟨requestNo, "$/lean/rpc/connect",  RpcConnectParams.mk uri⟩
+            let r ← Ipc.readResponseAs requestNo RpcConnected
+            rpcSessionId := some r.result.sessionId
+            requestNo := requestNo + 1
+          let params : Lsp.PlainGoalParams := {
+            textDocument := { uri }
+            position := pos,
+          }
+          let ps : RpcCallParams := {
+            params := toJson params
+            textDocument := { uri }
+            position := pos,
+            sessionId := rpcSessionId.get!,
+            method := `Lean.Widget.getInteractiveGoals
+          }
+          Ipc.writeRequest ⟨requestNo, "$/lean/rpc/call", ps⟩
+          let response ← Ipc.readResponseAs requestNo Client.InteractiveGoals
+          requestNo := requestNo + 1
+          IO.eprintln (repr response.result)
+          IO.eprintln ""
         | "widgets" =>
           if rpcSessionId.isNone then
             Ipc.writeRequest ⟨requestNo, "$/lean/rpc/connect",  RpcConnectParams.mk uri⟩