chore: change by precedence

@Kha it now uses the same precedence of `fun`.
The main motivation is to allow us to write `@by { ... }` instead of
`@(by { ... })`.

BTW, I am considering disabling implicit lambdas for `by ...` expressions.
It is automatically "intro"ducing the implicit variables without
giving an opportunity for users to pick their names.

src/Lean/Parser/Term.lean

@@ -224,7 +224,7 @@ stx.isAntiquot || stx.isIdent
 @[builtinTermParser] def seqRight    := tparser! infixR " *> "  60
 @[builtinTermParser] def map         := tparser! infixR " <$> " 100
 
-@[builtinTermParser] def byTactic    := parser!:leadPrec "by " >> Tactic.nonEmptySeq
+@[builtinTermParser] def byTactic    := parser!:maxPrec "by " >> Tactic.nonEmptySeq
 
 @[builtinTermParser] def funBinder.quot : Parser := parser! "`(funBinder|"  >> toggleInsideQuot funBinder >> ")"
 end Term

tests/lean/run/new_frontend2.lean

@@ -25,3 +25,9 @@ by {
   subst h₁;
   exact rfl
 }
+
+theorem ex : {α : Type} → {a b c : α} → a = b → b = c → a = c :=
+@by {
+  intro α a b c h₁ h₂;
+  exact Eq.trans h₁ h₂
+}