feat: allow simp priority explanations

src/Init/Data/Array/Lemmas.lean

@@ -1662,7 +1662,8 @@ theorem getElem_of_append {l l₁ l₂ : Array α} (eq : l = l₁.push a ++ l₂
   rw [← getElem?_eq_getElem, eq, getElem?_append_left (by simp; omega), ← h]
   simp
 
-@[simp 1100] theorem append_singleton {a : α} {as : Array α} : as ++ #[a] = as.push a := rfl
+@[simp 1100 "explanation of higher priority"]
+theorem append_singleton {a : α} {as : Array α} : as ++ #[a] = as.push a := rfl
 
 theorem push_eq_append {a : α} {as : Array α} : as.push a = as ++ #[a] := rfl
 

src/Init/Tactics.lean

@@ -1646,7 +1646,7 @@ If there are several with the same priority, it is uses the "most recent one". E
   cases d <;> rfl
 ```
 -/
-syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
+syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio (ppSpace str)?)? : attr
 
 /-- The possible `norm_cast` kinds: `elim`, `move`, or `squash`. -/
 syntax normCastLabel := &"elim" <|> &"move" <|> &"squash"

tests/lean/run/simpPrio.lean

@@ -3,3 +3,11 @@ opaque n : Nat
 @[simp 10] axiom prio_10 : n = 10
 -- simp should prefer the prio_1000 lemma with the higher priority
 example : n = 1000 := by simp
+
+-- Check that explanation strings are allowed after a priority.
+@[simp 1 "really low priority"] axiom prio_1 : n = 1
+example : n = 1000 := by simp
+
+#guard_msgs in
+-- but that explanation strings are not allowed if there is no priority
+@[simp "foo"] axiom foo : 1 = 2