diff --git a/src/Lean/Elab/Tactic/LibrarySearch.lean b/src/Lean/Elab/Tactic/LibrarySearch.lean
index d4be2053f879..119ed1ae23ec 100644
--- a/src/Lean/Elab/Tactic/LibrarySearch.lean
+++ b/src/Lean/Elab/Tactic/LibrarySearch.lean
@@ -24,28 +24,70 @@ Implementation of the `exact?` tactic.
 def exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireClose : Bool) :
     TacticM Unit := do
   let mvar ← getMainGoal
+  let initialState ← saveState
   let (_, goal) ← (← getMainGoal).intros
   goal.withContext do
     let required := (← (required.getD #[]).mapM getFVarId).toList.map .fvar
     let tactic := fun exfalso =>
-          solveByElim required (exfalso := exfalso) (maxDepth := 6)
+      solveByElim required (exfalso := exfalso) (maxDepth := 6)
     let allowFailure := fun g => do
       let g ← g.withContext (instantiateMVars (.mvar g))
       return required.all fun e => e.occurs g
-    match ← librarySearch goal tactic allowFailure with
+    match (← librarySearch goal tactic allowFailure) with
     -- Found goal that closed problem
     | none =>
-      addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta
+      addSuggestionIfValid ref mvar initialState
     -- Found suggestions
     | some suggestions =>
-      if requireClose then throwError
-        "`exact?` could not close the goal. Try `apply?` to see partial suggestions."
+      if requireClose then
+        let hint := if suggestions.isEmpty then "" else " Try `apply?` to see partial suggestions."
+        throwError "`exact?` could not close the goal.{hint}"
       reportOutOfHeartbeats `apply? ref
       for (_, suggestionMCtx) in suggestions do
         withMCtx suggestionMCtx do
-          addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta (addSubgoalsMsg := true)
+          addSuggestionIfValid ref mvar initialState (addSubgoalsMsg := true) (errorOnInvalid := false)
       if suggestions.isEmpty then logError "apply? didn't find any relevant lemmas"
       admitGoal goal
+where
+  /--
+  Executes `tac` in `savedState` (then restores the current state). Used to ensure that a suggested
+  tactic is valid.
+
+  Remark: we don't merely elaborate the proof term's syntax because it may successfully round-trip
+  (d)elaboration but still produce an invalid tactic (see the example in #5407).
+  -/
+  evalTacticWithState (savedState : Tactic.SavedState) (tac : TSyntax `tactic) : TacticM Unit := do
+    let currState ← saveState
+    savedState.restore
+    try
+      Term.withoutErrToSorry <| withoutRecover <| evalTactic tac
+    finally
+      currState.restore
+
+  /--
+  Suggests using the value of `goal` as a proof term if the corresponding tactic is valid at
+  `origGoal`, or else informs the user that a proof exists but is not syntactically valid.
+  -/
+  addSuggestionIfValid (ref : Syntax) (goal : MVarId) (initialState : Tactic.SavedState)
+                       (addSubgoalsMsg := false) (errorOnInvalid := true) : TacticM Unit := do
+    let proofExpr := (← instantiateMVars (mkMVar goal)).headBeta
+    let proofMVars ← getMVars proofExpr
+    let hasMVars := !proofMVars.isEmpty
+    let suggestion ← mkExactSuggestionSyntax proofExpr (useRefine := hasMVars) (exposeNames := false)
+    let mut exposeNames := false
+    try evalTacticWithState initialState suggestion
+    catch _ =>
+      exposeNames := true
+      let suggestion' ← mkExactSuggestionSyntax proofExpr (useRefine := hasMVars) (exposeNames := true)
+      try evalTacticWithState initialState suggestion'
+      catch _ =>
+        let suggestionStr ← SuggestionText.prettyExtra suggestion
+        -- Pretty-print the version without `expose_names` so variable names match the Infoview
+        let msg := m!"found a {if hasMVars then "partial " else ""}proof, \
+                      but the corresponding tactic failed:{indentD suggestionStr}"
+        if errorOnInvalid then throwError msg else logInfo msg
+        return
+    addExactSuggestion ref proofExpr (addSubgoalsMsg := addSubgoalsMsg) (exposeNames := exposeNames)
 
 @[builtin_tactic Lean.Parser.Tactic.exact?]
 def evalExact : Tactic := fun stx => do
@@ -69,7 +111,7 @@ def elabExact?Term : TermElab := fun stx expectedType? => do
     introdGoal.withContext do
       if let some suggestions ← librarySearch introdGoal then
         if suggestions.isEmpty then logError "`exact?%` didn't find any relevant lemmas"
-        else logError "`exact?%` could not close the goal. Try `by apply` to see partial suggestions."
+        else logError "`exact?%` could not close the goal. Try `by apply?` to see partial suggestions."
         mkLabeledSorry expectedType (synthetic := true) (unique := true)
       else
         addTermSuggestion stx (← instantiateMVars goal).headBeta
diff --git a/src/Lean/Elab/Tactic/Try.lean b/src/Lean/Elab/Tactic/Try.lean
index 8ebd70b5d745..2ddff5b6ff00 100644
--- a/src/Lean/Elab/Tactic/Try.lean
+++ b/src/Lean/Elab/Tactic/Try.lean
@@ -48,14 +48,6 @@ private def isExprAccessible (e : Expr) : MetaM Bool := do
   let (_, s) ← e.collectFVars |>.run {}
   s.fvarIds.allM isAccessible
 
-/-- Creates a temporary local context where all names are exposed, and executes `k`-/
-private def withExposedNames (k : MetaM α) : MetaM α := do
-  withNewMCtxDepth do
-    -- Create a helper goal to apply
-    let mvarId := (← mkFreshExprMVar (mkConst ``True)).mvarId!
-    let mvarId ← mvarId.exposeNames
-    mvarId.withContext do k
-
 /-- Executes `tac` in the saved state. This function is used to validate a tactic before suggesting it. -/
 def checkTactic (savedState : SavedState) (tac : TSyntax `tactic) : TacticM Unit := do
   let currState ← saveState
diff --git a/src/Lean/Meta/Tactic/ExposeNames.lean b/src/Lean/Meta/Tactic/ExposeNames.lean
index eb9759e10886..c565d7d2927d 100644
--- a/src/Lean/Meta/Tactic/ExposeNames.lean
+++ b/src/Lean/Meta/Tactic/ExposeNames.lean
@@ -7,15 +7,13 @@ prelude
 import Lean.Meta.Tactic.Util
 
 namespace Lean.Meta
-/--
-Creates a new goal whose local context has been "exposed" so that every local declaration has a clear, accessible name.
-If no local declarations require renaming, the original goal is returned unchanged.
--/
-def _root_.Lean.MVarId.exposeNames (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
-  mvarId.checkNotAssigned `expose_names
+
+/-- Returns a copy of the local context in which all declarations have clear, accessible names. -/
+private def getLCtxWithExposedNames : MetaM LocalContext := do
   let mut map : Std.HashMap Name FVarId := {}
   let mut toRename := #[]
-  for localDecl in (← getLCtx) do
+  let mut lctx ← getLCtx
+  for localDecl in lctx do
     let userName := localDecl.userName
     if userName.hasMacroScopes then
       toRename := toRename.push localDecl.fvarId
@@ -25,9 +23,8 @@ def _root_.Lean.MVarId.exposeNames (mvarId : MVarId) : MetaM MVarId := mvarId.wi
         toRename := toRename.push fvarId
       map := map.insert userName localDecl.fvarId
   if toRename.isEmpty then
-    return mvarId
+    return lctx
   let mut next : Std.HashMap Name Nat := {}
-  let mut lctx ← getLCtx
   -- Remark: Shadowed variables may be inserted later.
   toRename := toRename.qsort fun fvarId₁ fvarId₂ =>
     (lctx.get! fvarId₁).index < (lctx.get! fvarId₂).index
@@ -49,8 +46,21 @@ def _root_.Lean.MVarId.exposeNames (mvarId : MVarId) : MetaM MVarId := mvarId.wi
     next := next.insert baseName i
     map := map.insert userName fvarId
     lctx := lctx.modifyLocalDecl fvarId (·.setUserName userName)
+  return lctx
+
+/--
+Creates a new goal whose local context has been "exposed" so that every local declaration has a clear, accessible name.
+If no local declarations require renaming, the original goal is returned unchanged.
+-/
+def _root_.Lean.MVarId.exposeNames (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
+  mvarId.checkNotAssigned `expose_names
+  let lctx ← getLCtxWithExposedNames
   let mvarNew ← mkFreshExprMVarAt lctx (← getLocalInstances) (← mvarId.getType) .syntheticOpaque (← mvarId.getTag)
   mvarId.assign mvarNew
   return mvarNew.mvarId!
 
+/-- Creates a temporary local context where all names are exposed, and executes `k` -/
+def withExposedNames (k : MetaM α) : MetaM α := do
+  withNewMCtxDepth <| withLCtx (← getLCtxWithExposedNames) (← getLocalInstances) k
+
 end Lean.Meta
diff --git a/src/Lean/Meta/Tactic/TryThis.lean b/src/Lean/Meta/Tactic/TryThis.lean
index 04845bf3fa11..feb1fc67f3fe 100644
--- a/src/Lean/Meta/Tactic/TryThis.lean
+++ b/src/Lean/Meta/Tactic/TryThis.lean
@@ -8,6 +8,7 @@ import Lean.Server.CodeActions
 import Lean.Widget.UserWidget
 import Lean.Data.Json.Elab
 import Lean.Data.Lsp.Utf16
+import Lean.Meta.Tactic.ExposeNames
 
 /-!
 # "Try this" support
@@ -430,13 +431,23 @@ def addSuggestions (ref : Syntax) (suggestions : Array Suggestion)
   logInfoAt ref m!"{header}{msgs}"
   addSuggestionCore ref suggestions header (isInline := false) origSpan? style? codeActionPrefix?
 
-private def addExactSuggestionCore (addSubgoalsMsg : Bool) (e : Expr) : MetaM Suggestion :=
+/--
+Returns the syntax for an `exact` or `refine` (as indicated by `useRefine`) tactic corresponding to
+`e`. If `exposeNames` is `true`, prepends the tactic with `expose_names.`
+-/
+def mkExactSuggestionSyntax (e : Expr) (useRefine : Bool) (exposeNames : Bool) : MetaM (TSyntax `tactic) :=
+  withOptions (pp.mvars.set · false) do
+  let exprStx ← (if exposeNames then withExposedNames else id) <| delabToRefinableSyntax e
+  let tac ← if useRefine then `(tactic| refine $exprStx) else `(tactic| exact $exprStx)
+  let tacSeq ← if exposeNames then `(tactic| (expose_names; $tac)) else pure tac
+  return tacSeq
+
+private def addExactSuggestionCore (addSubgoalsMsg : Bool) (exposeNames : Bool) (e : Expr) :
+    MetaM Suggestion :=
   withOptions (pp.mvars.set · false) do
-  let stx ← delabToRefinableSyntax e
   let mvars ← getMVars e
-  let suggestion ← if mvars.isEmpty then `(tactic| exact $stx) else `(tactic| refine $stx)
-  let pp ← ppExpr e
-  let messageData? := if mvars.isEmpty then m!"exact {pp}" else m!"refine {pp}"
+  let mut suggestion ← mkExactSuggestionSyntax e (useRefine := !mvars.isEmpty) exposeNames
+  let messageData? ← SuggestionText.prettyExtra suggestion
   let postInfo? ← if !addSubgoalsMsg || mvars.isEmpty then pure none else
     let mut str := "\nRemaining subgoals:"
     for g in mvars do
@@ -457,11 +468,12 @@ The parameters are:
   `Remaining subgoals:`
 * `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text if the
   suggestion does not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is used.
+* `exposeNames`: if true (default false), will insert `expose_names` prior to the generated tactic
 -/
 def addExactSuggestion (ref : Syntax) (e : Expr)
     (origSpan? : Option Syntax := none) (addSubgoalsMsg := false)
-    (codeActionPrefix? : Option String := none): MetaM Unit := do
-  addSuggestion ref (← addExactSuggestionCore addSubgoalsMsg e)
+    (codeActionPrefix? : Option String := none) (exposeNames := false) : MetaM Unit := do
+  addSuggestion ref (← addExactSuggestionCore addSubgoalsMsg exposeNames e)
     (origSpan? := origSpan?) (codeActionPrefix? := codeActionPrefix?)
 
 /-- Add `exact e` or `refine e` suggestions.
@@ -479,8 +491,8 @@ The parameters are:
 -/
 def addExactSuggestions (ref : Syntax) (es : Array Expr)
     (origSpan? : Option Syntax := none) (addSubgoalsMsg := false)
-    (codeActionPrefix? : Option String := none) : MetaM Unit := do
-  let suggestions ← es.mapM <| addExactSuggestionCore addSubgoalsMsg
+    (codeActionPrefix? : Option String := none) (exposeNames := false) : MetaM Unit := do
+  let suggestions ← es.mapM <| addExactSuggestionCore addSubgoalsMsg exposeNames
   addSuggestions ref suggestions (origSpan? := origSpan?) (codeActionPrefix? := codeActionPrefix?)
 
 /-- Add a term suggestion.
diff --git a/tests/lean/librarySearch.lean b/tests/lean/librarySearch.lean
index 41e274b50dc2..44a7de15e803 100644
--- a/tests/lean/librarySearch.lean
+++ b/tests/lean/librarySearch.lean
@@ -49,7 +49,7 @@ example : x < x + 1 := exact?%
 #guard_msgs in
 example {α : Sort u} (x y : α) : Eq x y := exact?%
 
-/-- error: `exact?%` could not close the goal. Try `by apply` to see partial suggestions. -/
+/-- error: `exact?%` could not close the goal. Try `by apply?` to see partial suggestions. -/
 #guard_msgs in
 example (x y : Nat) : x ≤ y := exact?%
 
diff --git a/tests/lean/run/3922.lean b/tests/lean/run/3922.lean
index 3cc1acf20a48..401f719b21bc 100644
--- a/tests/lean/run/3922.lean
+++ b/tests/lean/run/3922.lean
@@ -20,7 +20,8 @@ axiom r.trans {a b c : Nat} : r a b → r b c → r a c
 /--
 info: Try this: refine r.symm ?_
 ---
-info: Try this: refine r.trans ?_ ?_
+info: found a partial proof, but the corresponding tactic failed:
+  refine r.trans ?_ ?_
 ---
 warning: declaration uses 'sorry'
 -/
diff --git a/tests/lean/run/5407.lean b/tests/lean/run/5407.lean
new file mode 100644
index 000000000000..6044530b2c6e
--- /dev/null
+++ b/tests/lean/run/5407.lean
@@ -0,0 +1,73 @@
+/-!
+# Library search should not return invalid tactics
+
+https://github.com/leanprover/lean4/issues/5407
+
+The library-search tactics `exact?` and `apply?` should not suggest proof terms that do not
+compile. If such proof terms are generated, these tactics should instead provide users with
+appropriate feedback.
+-/
+
+/-! Discards unprintable implicit argument to lambda -/
+inductive Odd : Nat → Prop
+  | one : Odd 1
+  | add_two : Odd n → Odd (n + 2)
+
+theorem odd_iff {n : Nat} : Odd n ↔ n % 2 = 1 := by
+  refine ⟨fun h => by induction h <;> omega, ?_⟩
+  match n with
+  | 0 => simp
+  | 1 => exact fun _ => Odd.one
+  | n + 2 => exact fun _ => Odd.add_two (odd_iff.mpr (by omega))
+
+/--
+error: found a proof, but the corresponding tactic failed:
+  exact fun a => (fun {n} => odd_iff.mpr) a
+-/
+#guard_msgs in
+example {n : Nat} : n % 2 = 1 → Odd n :=
+  by exact?
+
+
+/-! Detects shadowed variables -/
+opaque A : Type
+opaque B : Type
+opaque C : Prop
+axiom imp : A → B → C
+axiom a : A
+axiom b : B
+/--
+info: Try this: (expose_names; exact imp h_1 h)
+-/
+#guard_msgs in
+example : C := by
+  have h : A := a
+  have h : B := b
+  exact?
+
+
+/-! Detects lambdas with insufficient explicit binder types -/
+inductive EqExplicit {α} : α → α → Prop
+  | intro : (a b : α) → a = b → EqExplicit a b
+/--
+error: found a proof, but the corresponding tactic failed:
+  exact EqExplicit.intro (fun f => (fun g x => g x) f) id rfl
+-/
+#guard_msgs in
+example : EqExplicit (fun (f : α → β) => (fun g x => g x) f) id := by
+  exact?
+
+/-! `apply?` logs info instead of erroring -/
+opaque D : Prop
+axiom option1 : A → D
+axiom option2 {_ : B} : D
+/--
+info: Try this: refine option1 ?_
+---
+info: found a partial proof, but the corresponding tactic failed:
+  refine option2
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example : D := by apply?
diff --git a/tests/lean/run/info_trees.lean b/tests/lean/run/info_trees.lean
index b1b70ee23696..2ef75ea014a6 100644
--- a/tests/lean/run/info_trees.lean
+++ b/tests/lean/run/info_trees.lean
@@ -5,64 +5,76 @@
 /--
 info: Try this: exact Nat.zero_le n
 ---
-info: • command @ ⟨69, 0⟩-⟨69, 40⟩ @ Lean.Elab.Command.elabDeclaration
-  • Nat : Type @ ⟨69, 15⟩-⟨69, 18⟩ @ Lean.Elab.Term.elabIdent
-    • [.] Nat : some Sort.{?_uniq.1} @ ⟨69, 15⟩-⟨69, 18⟩
-    • Nat : Type @ ⟨69, 15⟩-⟨69, 18⟩
-  • n (isBinder := true) : Nat @ ⟨69, 11⟩-⟨69, 12⟩
-  • 0 ≤ n : Prop @ ⟨69, 22⟩-⟨69, 27⟩ @ «_aux_Init_Notation___macroRules_term_≤__2»
+info: • command @ ⟨81, 0⟩-⟨81, 40⟩ @ Lean.Elab.Command.elabDeclaration
+  • Nat : Type @ ⟨81, 15⟩-⟨81, 18⟩ @ Lean.Elab.Term.elabIdent
+    • [.] Nat : some Sort.{?_uniq.1} @ ⟨81, 15⟩-⟨81, 18⟩
+    • Nat : Type @ ⟨81, 15⟩-⟨81, 18⟩
+  • n (isBinder := true) : Nat @ ⟨81, 11⟩-⟨81, 12⟩
+  • 0 ≤ n : Prop @ ⟨81, 22⟩-⟨81, 27⟩ @ «_aux_Init_Notation___macroRules_term_≤__2»
     • Macro expansion
       0 ≤ n
       ===>
       binrel% LE.le✝ 0 n
-      • 0 ≤ n : Prop @ ⟨69, 22⟩†-⟨69, 27⟩† @ Lean.Elab.Term.Op.elabBinRel
-        • 0 ≤ n : Prop @ ⟨69, 22⟩†-⟨69, 27⟩†
-          • [.] LE.le✝ : none @ ⟨69, 22⟩†-⟨69, 27⟩†
-          • 0 : Nat @ ⟨69, 22⟩-⟨69, 23⟩ @ Lean.Elab.Term.elabNumLit
-          • n : Nat @ ⟨69, 26⟩-⟨69, 27⟩ @ Lean.Elab.Term.elabIdent
-            • [.] n : none @ ⟨69, 26⟩-⟨69, 27⟩
-            • n : Nat @ ⟨69, 26⟩-⟨69, 27⟩
-  • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨69, 8⟩-⟨69, 9⟩
-  • n (isBinder := true) : Nat @ ⟨69, 11⟩-⟨69, 12⟩
+      • 0 ≤ n : Prop @ ⟨81, 22⟩†-⟨81, 27⟩† @ Lean.Elab.Term.Op.elabBinRel
+        • 0 ≤ n : Prop @ ⟨81, 22⟩†-⟨81, 27⟩†
+          • [.] LE.le✝ : none @ ⟨81, 22⟩†-⟨81, 27⟩†
+          • 0 : Nat @ ⟨81, 22⟩-⟨81, 23⟩ @ Lean.Elab.Term.elabNumLit
+          • n : Nat @ ⟨81, 26⟩-⟨81, 27⟩ @ Lean.Elab.Term.elabIdent
+            • [.] n : none @ ⟨81, 26⟩-⟨81, 27⟩
+            • n : Nat @ ⟨81, 26⟩-⟨81, 27⟩
+  • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨81, 8⟩-⟨81, 9⟩
+  • n (isBinder := true) : Nat @ ⟨81, 11⟩-⟨81, 12⟩
   • CustomInfo(Lean.Elab.Term.BodyInfo)
-    • Tactic @ ⟨69, 31⟩-⟨69, 40⟩
+    • Tactic @ ⟨81, 31⟩-⟨81, 40⟩
       (Term.byTactic "by" (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])])))
       before ⏎
       n : Nat
       ⊢ 0 ≤ n
       after no goals
-      • Tactic @ ⟨69, 31⟩-⟨69, 33⟩
+      • Tactic @ ⟨81, 31⟩-⟨81, 33⟩
         "by"
         before ⏎
         n : Nat
         ⊢ 0 ≤ n
         after no goals
-        • Tactic @ ⟨69, 34⟩-⟨69, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq
+        • Tactic @ ⟨81, 34⟩-⟨81, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq
           (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])]))
           before ⏎
           n : Nat
           ⊢ 0 ≤ n
           after no goals
-          • Tactic @ ⟨69, 34⟩-⟨69, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq1Indented
+          • Tactic @ ⟨81, 34⟩-⟨81, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq1Indented
             (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])])
             before ⏎
             n : Nat
             ⊢ 0 ≤ n
             after no goals
-            • Tactic @ ⟨69, 34⟩-⟨69, 40⟩ @ Lean.Elab.LibrarySearch.evalExact
+            • Tactic @ ⟨81, 34⟩-⟨81, 40⟩ @ Lean.Elab.LibrarySearch.evalExact
               (Tactic.exact? "exact?" [])
               before ⏎
               n : Nat
               ⊢ 0 ≤ n
               after no goals
+              • Tactic @ ⟨81, 34⟩†-⟨81, 40⟩† @ Lean.Elab.Tactic.evalExact
+                (Tactic.exact "exact" (Term.app `Nat.zero_le [`n]))
+                before ⏎
+                n : Nat
+                ⊢ 0 ≤ n
+                after no goals
+                • Nat.zero_le n : 0 ≤ n @ ⟨1, 1⟩†-⟨1, 1⟩† @ Lean.Elab.Term.elabApp
+                  • [.] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.36 @ ⟨1, 0⟩†-⟨1, 0⟩†
+                  • Nat.zero_le : ∀ (n : Nat), 0 ≤ n @ ⟨1, 0⟩†-⟨1, 0⟩†
+                  • n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩† @ Lean.Elab.Term.elabIdent
+                    • [.] n : some Nat @ ⟨1, 5⟩†-⟨1, 5⟩†
+                    • n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩†
               • CustomInfo(Lean.Meta.Tactic.TryThis.TryThisInfo)
               • UserWidget Lean.Meta.Tactic.TryThis.tryThisWidget
                 {"suggestions": [{"suggestion": "exact Nat.zero_le n"}],
                  "style": null,
                  "range":
-                 {"start": {"line": 68, "character": 34}, "end": {"line": 68, "character": 40}},
+                 {"start": {"line": 80, "character": 34}, "end": {"line": 80, "character": 40}},
                  "isInline": true,
-                 "header": "Try this: "} • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨69, 8⟩-⟨69, 9⟩
+                 "header": "Try this: "} • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨81, 8⟩-⟨81, 9⟩
 -/
 #guard_msgs in
 #info_trees in