chore: deprecate Expr.forallArity, per todo (#1046)

Batteries/Lean/Expr.lean

@@ -27,17 +27,8 @@ def toSyntax (e : Expr) : TermElabM Syntax.Term := withFreshMacroScope do
 @[deprecated (since := "2024-10-16"), inherit_doc getNumHeadLambdas]
 abbrev lambdaArity := @getNumHeadLambdas
 
-/--
-Returns the number of leading `∀` binders of an expression. Ignores metadata.
--/
-def forallArity : Expr → Nat
-  | mdata _ b => forallArity b
-  | forallE _ _ body _ => 1 + forallArity body
-  | _ => 0
-
--- TODO: replace `forallArity` after https://github.com/leanprover/lean4/pull/5729
--- @[deprecated (since := "2024-10-16"), inherit_doc getNumHeadForalls]
--- abbrev forallArity := @getNumHeadForalls
+@[deprecated (since := "2024-11-13"), inherit_doc getNumHeadForalls]
+abbrev forallArity := @getNumHeadForalls
 
 /-- Like `withApp` but ignores metadata. -/
 @[inline]