`induction_eliminator` and `cases_eliminator` only key on the head symbol

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The @[induction_eliminator] and @[cases_eliminator] attribute cannot be used to register eliminators for two different types with the same head symbol.

Context

This is necessary to register eliminators for quotients of additive and multiplicative groups in Mathlib, where both have head symbol HasQuotient.quotient (leanprover-community/mathlib#12605)

Steps to Reproduce

1. Run the following:

inductive Foo : Bool → Type
  | ofTrue (x : Nat) : Foo true
  | ofFalse (x : Nat) : Foo false

-- insert an `id` term to make it easy to check these are actually being used.

@[elab_as_elim]
theorem Foo.true_rec {P : Foo true → Prop} (h : ∀ x, P (id <| .ofTrue x))
    (x : Foo true) : P x := by
  cases x; apply h

@[elab_as_elim]
theorem Foo.false_rec {P : Foo false → Prop} (h : ∀ x, P (id <| .ofFalse x))
    (x : Foo false) : P x := by
  cases x; apply h

example (x : Foo true) : x = x := by
  cases x using Foo.true_rec -- works
  sorry

example (x : Foo false) : x = x := by
  cases x using Foo.false_rec -- works
  sorry

attribute [cases_eliminator] Foo.true_rec Foo.false_rec

example (x : Foo true) : x = x := by
  cases x -- fails, tried to use `Foo.false_rec`
  sorry

example (x : Foo false) : x = x := by
  cases x --works
  sorry

Expected behavior: Both false_rec and true_rec can be registered, and the correct eliminator is chosen based on the full type of x

Actual behavior: The last-registered eliminator wins, causes the penultimate example to fail as the eliminator does not actually match the type of the major premise.

Versions

4.9.0-rc3

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

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

Start by running the minimal Lean reproducer in the issue and then trace the implementation of the cases_eliminator and induction_eliminator attributes and their eliminator-selection logic. Done means both eliminators can be registered for types sharing a head symbol, with the correct one selected from the full type and all four examples behaving as expected.