feat: add deprecated_syntax

[wkrozowski]

This PR adds deprecated_syntax command.

[wkrozowski]

!bench

[leanprover-radar]

Benchmark results for e30db6b against 9ffd748 are in. There are no significant changes. @wkrozowski

• 🟥 build//instructions: +6.6G (+0.05%)

Small changes (5🟥)

• 🟥 build/module/Lean.Elab.BuiltinCommand//instructions: +389.5M (+2.40%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Elab.Tactic.Basic//instructions: +256.3M (+1.92%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.Term.TermElabM//instructions: +229.1M (+0.82%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Parser.Command//instructions: +169.8M (+1.40%)
• 🟥 elab/bv_decide_large_aig//instructions: +294.1M (+0.72%)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9ffd74810487f75bef686b9b9e15da28bed44aac --onto e6df474dd9c3ad0e21771eaa808c53f66222216d. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-24 19:06:37)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 9ffd74810487f75bef686b9b9e15da28bed44aac --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-24 19:06:38)