fix: deduplicate elaboration of constant argument to rw (#8232)

This PR fixes elaboration of constants in the `rewrite` tactic.
previously, `rw [eq_self]` would elaborate `eq_self` twice, and add it
to the infotree twice. This would lead to the "Expected type" being
delaborated with an unknown universe metavariable.

I added a test to show this error during delaboration of the "Expected
type".

This was reported on Zulip as a panic message during delaboration:
[#mathlib4 > Crash in `sup`/`inf` /
`max`/`min`
delaborators](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Crash.20in.20.60sup.60.2F.60inf.60.20.2F.20.60max.60.2F.60min.60.20delaborators/with/515946714)

Author: JovanGerb

src/Lean/Elab/Tactic/Rewrite.lean

@@ -51,7 +51,7 @@ def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool)
         let term := rule[1]
         let processId (id : Syntax) : TacticM Unit := do
           -- See if we can interpret `id` as a hypothesis first.
-          if (← optional <| getFVarId id).isSome then
+          if (← withMainContext <| Term.isLocalIdent? id).isSome then
             x symm term
           else
             -- Try to get equation theorems for `id`.
@@ -62,8 +62,8 @@ def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool)
             let rec go : List Name →  TacticM Unit
               | [] => throwError "failed to rewrite using equation theorems for '{declName}'.{hint}"
               | eqThm::eqThms => (x symm (mkCIdentFrom id eqThm)) <|> go eqThms
-            go eqThms.toList
             discard <| Term.addTermInfo id (← mkConstWithFreshMVarLevels declName) (lctx? := ← getLCtx)
+            go eqThms.toList
         match term with
         | `($id:ident)  => processId id
         | `(@$id:ident) => processId id

tests/lean/interactive/rwElabConst.lean

@@ -0,0 +1,21 @@
+import Lean
+
+/-!
+Previously, `rw [my_lemma]` would elaborate `my_lemma` twice, both times generating new universe metavariables.
+This caused the "Expected type" to contain a universe metavariable that wasn't in the metavariable context.
+
+This test verifies that the generated universe level is in the metavariable context.
+-/
+
+open Lean PrettyPrinter Delaborator SubExpr
+/-- No-op delaborator that checks that the universe level is in the metavariable context -/
+@[delab app.Eq]
+def checkUniv : Delab := do
+  let .const _ [.mvar u] := (← getExpr).getAppFn | failure
+  _ ← u.getLevel -- if `u` isn't in the metavariable context, this throws an error during elaboration
+  failure
+
+example : True := by
+  try rw [eq_self]
+          --^ $/lean/plainTermGoal
+  trivial

tests/lean/interactive/rwElabConst.lean.expected.out

@@ -0,0 +1,5 @@
+{"textDocument": {"uri": "file:///rwElabConst.lean"},
+ "position": {"line": 18, "character": 12}}
+{"range":
+ {"start": {"line": 18, "character": 10}, "end": {"line": 18, "character": 17}},
+ "goal": "⊢ ∀ {α : Sort ?u} (a : α), (a = a) = True"}