fix: address symm and label bugs from #3408 (#3429)

#3408 was somewhat large and didn't properly test the symm and label
attribute code after edits to the builtin versions.

This migrates the code for generating labeled attributes from Init back
to Lean so that the required definitions are in scope.

This also addresses a mistake in the symm elaborator that prevented symm
without location information from elaborating.

Both fixes have been tested on the Std test suite and successfully
passed.

src/Init/Meta.lean

@@ -1429,24 +1429,6 @@ declare_simp_like_tactic (dsimp := true) dsimpAutoUnfold "dsimp! " fun (c : Lean
 
 end Tactic
 
-namespace Command
-
-/--
-Initialize a new "label" attribute.
-Declarations tagged with the attribute can be retrieved using `Std.Tactic.LabelAttr.labelled`.
--/
-macro (name := _root_.Lean.Parser.Command.registerLabelAttr)
-  doc:(docComment)? "register_label_attr " id:ident : command => do
-  let str := id.getId.toString
-  let idParser := mkIdentFrom id (`Parser.Attr ++ id.getId)
-  let descr := quote (removeLeadingSpaces
-    (doc.map (·.getDocString) |>.getD ("labelled declarations for " ++ id.getId.toString)))
-  `($[$doc:docComment]? initialize ext : LabelExtension ←
-      registerLabelAttr $(quote id.getId) $descr $(quote id.getId)
-    $[$doc:docComment]? syntax (name := $idParser:ident) $(quote str):str : attr)
-
-end Command
-
 end Parser
 
 end Lean

src/Init/Tactics.lean

@@ -1167,7 +1167,7 @@ syntax (name := normCastAddElim) "norm_cast_add_elim" ident : command
   It replaces the target with `u ~ t`.
 * `symm at h` will rewrite a hypothesis `h : t ~ u` to `h : u ~ t`.
 -/
-syntax (name := symm) "symm" (Parser.Tactic.location)? : tactic
+syntax (name := symm) "symm" (location)? : tactic
 
 /-- For every hypothesis `h : a ~ b` where a `@[symm]` lemma is available,
 add a hypothesis `h_symm : b ~ a`. -/

src/Lean/Elab/Tactic/Symm.lean

@@ -12,10 +12,11 @@ namespace Lean.Elab.Tactic
 @[builtin_tactic Lean.Parser.Tactic.symm]
 def evalSymm : Tactic := fun stx =>
   match stx with
-  | `(tactic| symm $(loc)) => do
+  | `(tactic| symm $(loc?)?) => do
     let atHyp h := liftMetaTactic1 fun g => g.applySymmAt h
     let atTarget := liftMetaTactic1 fun g => g.applySymm
-    withLocation (expandOptLocation loc) atHyp atTarget fun _ => throwError "symm made no progress"
+    let loc := if let some loc := loc? then expandLocation loc else Location.targets #[] true
+    withLocation loc atHyp atTarget fun _ => throwError "symm made no progress"
   | _ => throwUnsupportedSyntax
 
 @[builtin_tactic Lean.Parser.Tactic.symmSaturate]

src/Lean/LabelAttribute.lean

@@ -72,6 +72,20 @@ def registerLabelAttr (attrName : Name) (attrDescr : String)
   labelExtensionMapRef.modify fun map => map.insert attrName ext
   return ext
 
+/--
+Initialize a new "label" attribute.
+Declarations tagged with the attribute can be retrieved using `Std.Tactic.LabelAttr.labelled`.
+-/
+macro (name := _root_.Lean.Parser.Command.registerLabelAttr)
+  doc:(docComment)? "register_label_attr " id:ident : command => do
+  let str := id.getId.toString
+  let idParser := mkIdentFrom id (`Parser.Attr ++ id.getId)
+  let descr := quote (removeLeadingSpaces
+    (doc.map (·.getDocString) |>.getD ("labelled declarations for " ++ id.getId.toString)))
+  `($[$doc:docComment]? initialize ext : Lean.LabelExtension ←
+      registerLabelAttr $(quote id.getId) $descr $(quote id.getId)
+    $[$doc:docComment]? syntax (name := $idParser:ident) $(quote str):str : attr)
+
 /-- When `attrName` is an attribute created using `register_labelled_attr`,
 return the names of all declarations labelled using that attribute. -/
 def labelled (attrName : Name) : CoreM (Array Name) := do