fix: increase the priority of lemma notation (#17533)

This makes it take precedence over the Batteries version, which in turn simplifies the resulting `Syntax` object to not have a `choice` node.

Presumably there is a very marginal performance gain too.

[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/348111-batteries/topic/lemma.20notation)

Mathlib/Tactic/Lemma.lean

@@ -12,8 +12,9 @@ import Lean.Parser.Command
 
 open Lean
 
+-- higher priority to override the one in Batteries
 /-- `lemma` means the same as `theorem`. It is used to denote "less important" theorems -/
-syntax (name := lemma) declModifiers
+syntax (name := lemma) (priority := default + 1) declModifiers
   group("lemma " declId ppIndent(declSig) declVal) : command
 
 /-- Implementation of the `lemma` command, by macro expansion to `theorem`. -/