From c816524d8d695fecfd7332773877f795bf93fccf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 18 Jan 2022 14:26:14 -0800
Subject: [PATCH] feat: add `subst?`

---
 src/Lean/Meta/Tactic/Subst.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Tactic/Subst.lean b/src/Lean/Meta/Tactic/Subst.lean
index 2e7b6f3256..c0540b5849 100644
--- a/src/Lean/Meta/Tactic/Subst.lean
+++ b/src/Lean/Meta/Tactic/Subst.lean
@@ -165,8 +165,11 @@ def subst (mvarId : MVarId) (hFVarId : FVarId) : MetaM MVarId :=
         | throwTacticEx `subst mvarId m!"did not find equation for eliminating '{mkFVar hFVarId}'"
       return (← substCore mvarId fvarId (symm := symm) (tryToSkip := true)).2
 
+def subst? (mvarId : MVarId) (hFVarId : FVarId) : MetaM (Option MVarId) :=
+  observing? (subst mvarId hFVarId)
+
 def trySubst (mvarId : MVarId) (hFVarId : FVarId) : MetaM MVarId := do
-  match (← observing? (subst mvarId hFVarId)) with
+  match (← subst? mvarId hFVarId) with
   | some mvarId => return mvarId
   | none => return mvarId