elab_as_elim does not support function application in resulting motive arguments

[JamesGallicchio]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

I would like to mark the following lemma elab_as_elim:

theorem natAbs_elim {motive : Nat → Prop} (i : Int)
  (hpos : ∀ (n : Nat), i = n → motive n)
  (hneg : ∀ (n : Nat), i = -↑n → motive n)
  : motive (Int.natAbs i)
  := by sorry

in order for apply to succeed at e.g.:

example (x : Int) (y : Nat) : x.natAbs < y := by
  apply natAbs_elim x
  sorry

However currently the elab_as_elim annotation fails with

unexpected eliminator resulting type
  motive i.natAbs

Context

Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/apply.20motive.20failure

Steps to Reproduce

Expected behavior: elab_as_elim succeeds on the natAbs_elim example

Actual behavior: elab_as_elim fails on natAbs_elim

Versions

Lean 4.8.0-rc1
NixOS unstable

Additional Information

N/A

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.