feat: Extend the match code action to also show an implicit-arguments code action

[MoritzBeroRoos]

This PR extends the match code action, to also show a new Option

Generate a list of equations with implicit arguments for this match.

in those cases where at least one constructor might be interesting to use with @.
Here interesting is defined as has at least one implicit argument that is not a parameter of the inductive type,
where a parameter is an argument to the inductive type that is fixed over constructors.

E.g. invoking Generate a list of equations with implicit arguments for this match. in
the following

inductive TermWithImplicit (F : Nat → Type u) (α : Type w)
  | var (x : α) : TermWithImplicit F α
  | func {l : Nat} (f : F l) (ts : Fin l → TermWithImplicit F α) : TermWithImplicit F α

def myfun4 (t : TermWithImplicit F α) : Nat := by
  match t with

produces

def myfun4 (t : TermWithImplicit F α) : Nat := by
  match t with
  | .var x => _
  | .func (l := l) f ts => _

where the implicit argument {l : Nat} is now usable.
Note that the arguments F and α are not filled since they are parameters
(a parameter is an argument to an inductive type that is fixed over constructors), i.e.
they are already determined by the match discriminant t. This means they don't provide any
new information for you.

[fgdorais]

Wouldn't it be better to generate this?

def myfun4 (t : TermWithImplicit F α) : Nat := by
  match t with
  | .var x => _
  | .func (l := l) f ts => _

[MoritzBeroRoos]

I don't really like how the (h := h) syntax doubles the name. For slightly longer names such as hPremiseLeq
lines quickly get really long.
I hope to at some point also introduce such an option to the cases tactic, and there i think we definitely want the @ syntax, since one typically needs more of the implicit variables and wants to avoid duplicating all the names.
For match i think the story might not be so clear, how many of the implicits one typically needs.
The (h := h) here has going for it that one can easily delete unneeded implicits.

However it also breaks as soon as one renames in the definition

[fgdorais]

How about (h := _)? Short and the code does not break if the order of implicit arguments is changed in the definition.

[MoritzBeroRoos]

Then one has to copy a bunch of more names before one can get on with the writing.
I think it might be a good idea to try to get some more opinions on Zulip on this

[MoritzBeroRoos]

After thinking about it some more and not receiving much opinions on zulip i think the best way forward is your original suggestion of

def myfun4 (t : TermWithImplicit F α) : Nat := by
  match t with
  | .var x => _
  | .func (l := l) f ts => _

The long lines argument isn't really valid since with this syntax one would be expected to delete unneeded args.
I think a big argument against using the syntax (h := _) is, that typing is a much more error prone and slower process than deleting args. And the purpose of this PR is to have less typing (and name look up) anyway :)

i have adapted the description and the doc comments accordingly.