diff --git a/src/Lean/Elab/Tactic/Simpa.lean b/src/Lean/Elab/Tactic/Simpa.lean
index 778b380966..4e43093a6d 100644
--- a/src/Lean/Elab/Tactic/Simpa.lean
+++ b/src/Lean/Elab/Tactic/Simpa.lean
@@ -31,84 +31,93 @@ open Lean Parser.Tactic Elab Meta Term Tactic Simp Linter
 def getLinterUnnecessarySimpa (o : LinterOptions) : Bool :=
   getLinterValue linter.unnecessarySimpa o
 
-deriving instance Repr for UseImplicitLambdaResult
-
 @[builtin_tactic Lean.Parser.Tactic.simpa] def evalSimpa : Tactic := fun stx => do
   match stx with
   | `(tactic| simpa%$tk $[?%$squeeze]? $[!%$unfold]? $cfg:optConfig $(disch)? $[only%$only]?
-        $[[$args,*]]? $[using $usingArg]?) => Elab.Tactic.focus do withSimpDiagnostics do
+        $[[$args,*]]? $[using%$usingTk? $usingArg]?) => Elab.Tactic.focus do withSimpDiagnostics do
     let stx ← `(tactic| simp $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]?)
-    let { ctx, simprocs, dischargeWrapper, .. } ←
-      withMainContext <| mkSimpContext stx (eraseLocal := false)
-    let ctx := if unfold.isSome then ctx.setAutoUnfold else ctx
-    -- TODO: have `simpa` fail if it doesn't use `simp`.
-    let ctx := ctx.setFailIfUnchanged false
-    dischargeWrapper.with fun discharge? => do
-      let (some (_, g), stats) ← simpGoal (← getMainGoal) ctx (simprocs := simprocs)
-          (simplifyTarget := true) (discharge? := discharge?)
-        | if getLinterUnnecessarySimpa (← getLinterOptions) then
-            logLint linter.unnecessarySimpa (← getRef) "try 'simp' instead of 'simpa'"
-          return {}
-      g.withContext do
-      let stats ← if let some stx := usingArg then
-        let mvarCounterSaved := (← getMCtx).mvarCounter
-        let e ← Tactic.elabTerm stx none (mayPostpone := true)
-        unless ← occursCheck g e do
-          throwError "Occurs check failed: Expression{indentExpr e}\ncontains the goal {Expr.mvar g}"
-        -- Copy the goal. We want to defer assigning `g := g'` to prevent `MVarId.note` from
-        -- partially assigning the goal in case we need to log unassigned metavariables.
-        -- Without deferring, this can cause `logUnassignedAndAbort` to report that `g` could not
-        -- be synthesized; recall that this function reports that a metavariable could not be
-        -- synthesized if, after mvar instantiation, it contains one of the provided mvars.
-        let gCopy ← mkFreshExprSyntheticOpaqueMVar (← g.getType) (← g.getTag)
-        let (h, g') ← gCopy.mvarId!.note `h e
-        let (result?, stats) ← simpGoal g' ctx (simprocs := simprocs) (fvarIdsToSimp := #[h])
-          (simplifyTarget := false) (stats := stats) (discharge? := discharge?)
-        match result? with
-        | some (xs, g') =>
-          let h := xs[0]?.getD h
-          let name ← mkFreshUserName `h
-          let g' ← g'.rename h name
-          setGoals [g']
-          g'.withContext do
-            let gType ← g'.getType
-            let h ← Term.elabTerm (mkIdent name) gType
-            Term.synthesizeSyntheticMVarsNoPostponing
-            let hType ← inferType h
-            unless (← withAssignableSyntheticOpaque <| isDefEq gType hType) do
-              -- `e` still is valid in this new local context
-              Term.throwTypeMismatchError gType hType h
-                (header? := some m!"Type mismatch: After simplification, term{indentExpr e}\n")
-            logUnassignedAndAbort (← filterOldMVars (← getMVars e) mvarCounterSaved)
-            closeMainGoal `simpa (checkUnassigned := false) h
-        | none =>
-          if getLinterUnnecessarySimpa (← getLinterOptions) then
-            if let .fvar h := e then
-              if (← getLCtx).getRoundtrippingUserName? h |>.isSome then
-                logLint linter.unnecessarySimpa (← getRef)
-                  m!"Try `simp at {Expr.fvar h}` instead of `simpa using {Expr.fvar h}`"
-        g.assign gCopy
-        pure stats
-      else if let some ldecl := (← getLCtx).findFromUserName? `this then
-        if let (some (_, g), stats) ← simpGoal g ctx (simprocs := simprocs)
-            (fvarIdsToSimp := #[ldecl.fvarId]) (simplifyTarget := false) (stats := stats)
-            (discharge? := discharge?) then
-          g.assumption; pure stats
-        else
-          pure stats
-      else
-        g.assumption; pure stats
-      if tactic.simp.trace.get (← getOptions) || squeeze.isSome then
-        let usingArg : Option Term := usingArg.map (⟨·.raw.unsetTrailing⟩)
-        let stx ← match ← mkSimpOnly stx.raw.unsetTrailing stats.usedTheorems with
-          | `(tactic| simp $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]?) =>
-            if unfold.isSome then
-              `(tactic| simpa! $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
+    let stats ← do
+      let { ctx, simprocs, dischargeWrapper, .. } ← withMainContext <| mkSimpContext stx (eraseLocal := false)
+      let ctx := if unfold.isSome then ctx.setAutoUnfold else ctx
+      -- TODO: have `simpa` fail if it doesn't use `simp`.
+      let ctx := ctx.setFailIfUnchanged false
+      dischargeWrapper.with fun discharge? => do
+        -- When there is a `using` clause we add tactic info showing the simplified goal.
+        -- The span is `simpa ... using`.
+        let mkInfo ← mkInitialTacticInfo (mkNullNode #[tk, usingTk?.getD .missing])
+        let (some (_, g), stats) ← simpGoal (← getMainGoal) ctx (simprocs := simprocs) (simplifyTarget := true) (discharge? := discharge?)
+          | if getLinterUnnecessarySimpa (← getLinterOptions) then
+              logLint linter.unnecessarySimpa (← getRef) "try 'simp' instead of 'simpa'"
+            return {}
+        -- Replace the goal; captured by `mkInfo` in `using` case below.
+        replaceMainGoal [g]
+        g.withContext do
+          if let some stx := usingArg then
+            if (← getInfoState).enabled then
+              let trees ← getResetInfoTrees
+              withInfoContext (mkInfo := mkInfo) do
+                -- Re-nest info trees so far into tactic info node
+                modifyInfoState fun st => { st with trees }
+            let mvarCounterSaved := (← getMCtx).mvarCounter
+            let e ← Tactic.elabTerm stx none (mayPostpone := true)
+            unless ← occursCheck g e do
+              throwError "Occurs check failed: Expression{indentExpr e}\ncontains the goal {Expr.mvar g}"
+            -- Copy the goal. We want to defer assigning `g := g'` to prevent `MVarId.note` from
+            -- partially assigning the goal in case we need to log unassigned metavariables.
+            -- Without deferring, this can cause `logUnassignedAndAbort` to report that `g` could not
+            -- be synthesized; recall that this function reports that a metavariable could not be
+            -- synthesized if, after mvar instantiation, it contains one of the provided mvars.
+            let gCopy ← mkFreshExprSyntheticOpaqueMVar (← g.getType) (← g.getTag)
+            let (h, g') ← gCopy.mvarId!.note `h e
+            let (result?, stats) ← simpGoal g' ctx (simprocs := simprocs) (fvarIdsToSimp := #[h])
+              (simplifyTarget := false) (stats := stats) (discharge? := discharge?)
+            match result? with
+            | some (xs, g') =>
+              let h := xs[0]?.getD h
+              let name ← mkFreshUserName `h
+              let g' ← g'.rename h name
+              g'.withContext do
+                let gType ← g'.getType
+                let h ← Term.elabTerm (mkIdent name) gType
+                Term.synthesizeSyntheticMVarsNoPostponing
+                let hType ← inferType h
+                unless (← withAssignableSyntheticOpaque <| isDefEq gType hType) do
+                  -- `e` still is valid in this new local context
+                  Term.throwTypeMismatchError gType hType h
+                    (header? := some m!"Type mismatch: After simplification, term{indentExpr e}\n")
+                logUnassignedAndAbort (← filterOldMVars (← getMVars e) mvarCounterSaved)
+                pushGoal g'
+                closeMainGoal `simpa (checkUnassigned := false) h
+            | none =>
+              if getLinterUnnecessarySimpa (← getLinterOptions) then
+                if let .fvar h := e then
+                  if (← getLCtx).getRoundtrippingUserName? h |>.isSome then
+                    logLint linter.unnecessarySimpa (← getRef)
+                      m!"Try `simp at {Expr.fvar h}` instead of `simpa using {Expr.fvar h}`"
+            g.assign gCopy
+            pure stats
+          else if let some ldecl := (← getLCtx).findFromUserName? `this then
+            if let (some (_, g), stats) ← simpGoal g ctx (simprocs := simprocs)
+                (fvarIdsToSimp := #[ldecl.fvarId]) (simplifyTarget := false) (stats := stats)
+                (discharge? := discharge?) then
+              g.assumption
+              pure stats
             else
-              `(tactic| simpa $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
-          | _ => unreachable!
-        TryThis.addSuggestion tk stx (origSpan? := ← getRef)
-      return stats.diag
+              pure stats
+          else
+            g.assumption
+            pure stats
+    if tactic.simp.trace.get (← getOptions) || squeeze.isSome then
+      let usingArg : Option Term := usingArg.map (⟨·.raw.unsetTrailing⟩)
+      let stx ← match ← mkSimpOnly stx.raw.unsetTrailing stats.usedTheorems with
+        | `(tactic| simp $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]?) =>
+          if unfold.isSome then
+            `(tactic| simpa! $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
+          else
+            `(tactic| simpa $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
+        | _ => unreachable!
+      TryThis.addSuggestion tk stx (origSpan? := ← getRef)
+    return stats.diag
     | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic.Simpa
diff --git a/tests/lean/interactive/plainGoal.lean b/tests/lean/interactive/plainGoal.lean
index 302f709d51..3ccaad33f0 100644
--- a/tests/lean/interactive/plainGoal.lean
+++ b/tests/lean/interactive/plainGoal.lean
@@ -148,3 +148,14 @@ example : True := by induction 1 with done
                                 --^ $/lean/plainGoal
 
 end
+
+section
+
+example (f : Nat → Nat) (n : Nat) (hf : ∀ x, f x = x + 0 + 1) : f n + 0 = 1 + n := by
+  simpa [Nat.add_zero, Nat.add_comm] using hf n
+--^ $/lean/plainGoal
+ --^ $/lean/plainGoal
+                                       --^ $/lean/plainGoal
+                                         --^ $/lean/plainGoal
+
+end
diff --git a/tests/lean/interactive/plainGoal.lean.expected.out b/tests/lean/interactive/plainGoal.lean.expected.out
index f1e139df74..599e7a33d0 100644
--- a/tests/lean/interactive/plainGoal.lean.expected.out
+++ b/tests/lean/interactive/plainGoal.lean.expected.out
@@ -185,3 +185,24 @@ null
 {"textDocument": {"uri": "file:///plainGoal.lean"},
  "position": {"line": 146, "character": 34}}
 {"rendered": "```lean\nx✝ : Nat\n⊢ True\n```", "goals": ["x✝ : Nat\n⊢ True"]}
+{"textDocument": {"uri": "file:///plainGoal.lean"},
+ "position": {"line": 154, "character": 2}}
+{"rendered":
+ "```lean\nf : Nat → Nat\nn : Nat\nhf : ∀ (x : Nat), f x = x + 0 + 1\n⊢ f n + 0 = 1 + n\n```",
+ "goals":
+ ["f : Nat → Nat\nn : Nat\nhf : ∀ (x : Nat), f x = x + 0 + 1\n⊢ f n + 0 = 1 + n"]}
+{"textDocument": {"uri": "file:///plainGoal.lean"},
+ "position": {"line": 154, "character": 3}}
+{"rendered":
+ "```lean\nf : Nat → Nat\nn : Nat\nhf : ∀ (x : Nat), f x = x + 0 + 1\n⊢ f n = n + 1\n```",
+ "goals":
+ ["f : Nat → Nat\nn : Nat\nhf : ∀ (x : Nat), f x = x + 0 + 1\n⊢ f n = n + 1"]}
+{"textDocument": {"uri": "file:///plainGoal.lean"},
+ "position": {"line": 154, "character": 41}}
+{"rendered":
+ "```lean\nf : Nat → Nat\nn : Nat\nhf : ∀ (x : Nat), f x = x + 0 + 1\n⊢ f n = n + 1\n```",
+ "goals":
+ ["f : Nat → Nat\nn : Nat\nhf : ∀ (x : Nat), f x = x + 0 + 1\n⊢ f n = n + 1"]}
+{"textDocument": {"uri": "file:///plainGoal.lean"},
+ "position": {"line": 154, "character": 43}}
+{"rendered": "no goals", "goals": []}
diff --git a/tests/lean/run/5634.lean b/tests/lean/run/5634.lean
index cad02e82ef..801f8aa2f4 100644
--- a/tests/lean/run/5634.lean
+++ b/tests/lean/run/5634.lean
@@ -18,7 +18,6 @@ htrue : True
 ---
 error: unsolved goals
 htrue : True
-h✝ : False
 ⊢ False
 -/
 #guard_msgs in
@@ -35,7 +34,6 @@ context:
 ⊢ False
 ---
 error: unsolved goals
-h✝ : False
 ⊢ False
 -/
 #guard_msgs in