Deprecate and remove `Array` literal patterns

We added support for #[...] patterns early on for syntax match and didn't have a plan for supporting reasoning about it; we never used it in syntax match and still don't have a reasoning plan. Because of the complexity of even the current implementation, the most reasonable way to move forward is to deprecate and remove the syntax.

A perhaps naive regex '\| #\[ finds about a dozen uses in core and another dozen in the Mathlib tree:

$ git grep -E '\| #\['
src/Init/Meta.lean:  | #[]  => fn
src/Lean/Elab/Deriving/FromToJson.lean:    | #[], _ => ``(toJson $(quote ctorStr))
src/Lean/Elab/Deriving/FromToJson.lean:    | #[(x, t)], none => ``(mkObj [($(quote ctorStr), $(← mkToJson x t))])
src/Lean/Elab/Quotation.lean:  | #[]  => `(Unit.unit)
src/Lean/Elab/Quotation.lean:  | #[e] => return e
src/Lean/Elab/Quotation.lean:            | #[id] => pure id
src/Lean/Elab/Quotation.lean:      | #[] =>
src/Lean/Elab/Syntax.lean:      | #[]       => Parser.ensureConstantParserAlias aliasName; ``(ParserDescr.const $(quote aliasName))
src/Lean/Elab/Syntax.lean:      | #[p1]     => Parser.ensureUnaryParserAlias aliasName; ``(ParserDescr.unary $(quote aliasName) $p1)
src/Lean/Elab/Syntax.lean:      | #[p1, p2] => Parser.ensureBinaryParserAlias aliasName; ``(ParserDescr.binary $(quote aliasName) $p1 $p2)
src/Lean/Elab/Tactic/Simpa.lean:          let h := match xs with | #[h] | #[] => h | _ => unreachable!
src/Lean/Widget/TaggedText.lean:  | #[] => acc
tests/bench/liasolver.lean:  | #[]           => panic! "Cannot calculate GCD of empty list of coefficients"
tests/bench/liasolver.lean:  | #[(i, x)]     => x
tests/lean/match1.lean:| #[x]    => x
tests/lean/match1.lean:| #[x, y] => x + y
tests/lean/match1.lean:  | #[1, 2]    => 2
tests/lean/match1.lean:  | #[]        => 0
tests/lean/match1.lean:  | #[3, 4, 5] => 3
tests/lean/match1.lean.expected.out:  | #[1, 2] => 2
tests/lean/match1.lean.expected.out:  | #[] => 0
tests/lean/match1.lean.expected.out:  | #[3, 4, 5] => 3
tests/lean/run/matchArrayLit.lean:| #[]           => _
tests/lean/run/matchArrayLit.lean:| #[a₁]         => _
tests/lean/run/matchArrayLit.lean:| #[a₁, a₂, a₃] => _
$ grep -E '\| #\[' ../mathlib4 -r
../mathlib4/Cache/IO.lean:          runCmd (← getLeanTar) <| #[zipPath.toString, trace] ++
../mathlib4/Mathlib/RingTheory/WittVector/IsPoly.lean:    | #[x] => evalTactic (← `(tactic| refine IsPoly.ext (f := $fS) (g := $gS) ?_ ?_ ?_ _ $x))
../mathlib4/Mathlib/RingTheory/WittVector/IsPoly.lean:    | #[x, y] => evalTactic (← `(tactic| refine IsPoly₂.ext (f := $fS) (g := $gS) ?_ ?_ ?_ _ $x $y))
../mathlib4/Mathlib/Tactic/Linter/Lint.lean:      | #[id] =>
../mathlib4/lake-packages/std/Std/Tactic/Lint/Misc.lean:    | #[u] => some u
../mathlib4/lake-packages/std/Std/Tactic/RCases.lean:  | #[_, pat] => RCasesPatt.parse pat
../mathlib4/lake-packages/std/Std/Tactic/RCases.lean:  | #[] => pure $ RCasesPatt.tuple tk []
../mathlib4/lake-packages/std/Std/Tactic/Simpa.lean:        let h := match xs with | #[h] | #[] => h | _ => unreachable!
../mathlib4/lake-packages/aesop/Aesop/BuiltinRules/DestructProducts.lean:    | #[α, β] =>
../mathlib4/lake-packages/Cli/Cli/Basic.lean:              return some <| #[(inputFlagName, ⟨flag, ""⟩)] ++ tail
../mathlib4/lake-packages/proofwidgets/ProofWidgets/Data/Html.lean:  let `(term| #[ $[($as:str, $vs)],* ] ) := attrs | failure
../mathlib4/lake-packages/proofwidgets/ProofWidgets/Data/Html.lean:  let `(term| #[ $cs,* ]) := children | failure
../mathlib4/.lake/packages/batteries/Batteries/Tactic/Lint/Misc.lean:    | #[u] => some u
../mathlib4/.lake/packages/aesop/Aesop/BuiltinRules/DestructProducts.lean:    | #[α, β] =>
../mathlib4/.lake/packages/proofwidgets/ProofWidgets/Data/Html.lean:  -- into ``children ← `(term| #[a, Html.text " text "] ++ cs ++ #[d])``.
../mathlib4/.lake/packages/proofwidgets/ProofWidgets/Data/Html.lean:        csArrs ← csArrs.push <$> `(term| #[$csArr,*])
../mathlib4/.lake/packages/proofwidgets/ProofWidgets/Data/Html.lean:    csArrs ← csArrs.push <$> `(term| #[$csArr,*])
../mathlib4/.lake/packages/proofwidgets/ProofWidgets/Data/Html.lean:      | #[w], #[] => pure w
../mathlib4/.lake/packages/proofwidgets/ProofWidgets/Data/Html.lean:      `(term| #[$vs',*]))
../mathlib4/.lake/packages/importGraph/ImportGraph/Cli.lean:    | #[] => Std.HashSet.empty.insert "dot"
../mathlib4/.lake/packages/importGraph/ImportGraph/Cli.lean:  | #[] => writeFile "import_graph.dot" (outFiles["dot"]!)
../mathlib4/.lake/packages/Cli/Cli/Basic.lean:              return some <| #[(inputFlagName, ⟨flag, ""⟩)] ++ tail

Start by reviewing the listed pattern matches in src/Lean and the related tests under tests/lean, then use the provided git grep commands to audit core and Mathlib usage. Done means the #[...] pattern syntax and its remaining uses are removed or updated consistently, with the affected tests reflecting the new behavior.