chore: use elab_as_elim directly, now that lean4#1900 is fixed (#9288)

Adds the attribute `elab_as_elim` directly to the declarations of `strongSubRecursion`
and `pincerRecursion`, rather than in separate commands.

This change was made possible by leanprover/lean4@8a573b5, which fixed leanprover/lean4#1900.

Mathlib/Data/Nat/Basic.lean

@@ -560,21 +560,18 @@ theorem decreasingInduction_succ_left {P : ℕ → Sort*} (h : ∀ n, P (n + 1)
 strictly below `(a,b)` to `P a b`, then we have `P n m` for all `n m : ℕ`.
 Note that for non-`Prop` output it is preferable to use the equation compiler directly if possible,
 since this produces equation lemmas. -/
+@[elab_as_elim]
 def strongSubRecursion {P : ℕ → ℕ → Sort*} (H : ∀ a b, (∀ x y, x < a → y < b → P x y) → P a b) :
     ∀ n m : ℕ, P n m
   | n, m => H n m fun x y _ _ => strongSubRecursion H x y
 #align nat.strong_sub_recursion Nat.strongSubRecursion
 
--- Porting note:
--- we can't put this on the definition itself because of
--- https://github.com/leanprover/lean4/issues/1900
-attribute [elab_as_elim] strongSubRecursion
-
 /-- Given `P : ℕ → ℕ → Sort*`, if we have `P i 0` and `P 0 i` for all `i : ℕ`,
 and for any `x y : ℕ` we can extend `P` from `(x,y+1)` and `(x+1,y)` to `(x+1,y+1)`
 then we have `P n m` for all `n m : ℕ`.
 Note that for non-`Prop` output it is preferable to use the equation compiler directly if possible,
 since this produces equation lemmas. -/
+@[elab_as_elim]
 def pincerRecursion {P : ℕ → ℕ → Sort*} (Ha0 : ∀ a : ℕ, P a 0) (H0b : ∀ b : ℕ, P 0 b)
     (H : ∀ x y : ℕ, P x y.succ → P x.succ y → P x.succ y.succ) : ∀ n m : ℕ, P n m
   | a, 0 => Ha0 a
@@ -583,11 +580,6 @@ def pincerRecursion {P : ℕ → ℕ → Sort*} (Ha0 : ∀ a : ℕ, P a 0) (H0b
 termination_by pincerRecursion Ha0 Hab H n m => n + m
 #align nat.pincer_recursion Nat.pincerRecursion
 
--- Porting note:
--- we can't put this on the definition itself because of
--- https://github.com/leanprover/lean4/issues/1900
-attribute [elab_as_elim] pincerRecursion
-
 /-- Recursion starting at a non-zero number: given a map `C k → C (k+1)` for each `k ≥ n`,
 there is a map from `C n` to each `C m`, `n ≤ m`. -/
 @[elab_as_elim]