From 229f16f4213cc087aa0715b2896758dfb421becb Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Fri, 16 Feb 2024 13:08:47 +1100
Subject: [PATCH] chore: upstream MVarId.applyConst (#3362)

Helper function for applying a constant to the goal, with fresh universe
metavariables.
---
 src/Lean/Meta/Tactic/Apply.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Lean/Meta/Tactic/Apply.lean b/src/Lean/Meta/Tactic/Apply.lean
index 23e21d9b20..c8c5532199 100644
--- a/src/Lean/Meta/Tactic/Apply.lean
+++ b/src/Lean/Meta/Tactic/Apply.lean
@@ -188,6 +188,10 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig :=
 def apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig := {}) : MetaM (List MVarId) :=
   mvarId.apply e cfg
 
+/-- Short-hand for applying a constant to the goal. -/
+def _root_.Lean.MVarId.applyConst (mvar : MVarId) (c : Name) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := do
+  mvar.apply (← mkConstWithFreshMVarLevels c) cfg
+
 partial def splitAndCore (mvarId : MVarId) : MetaM (List MVarId) :=
   mvarId.withContext do
     mvarId.checkNotAssigned `splitAnd