Can grind be used to infer implicit arguments?

Stream: Is there code for X?

[Shubakur Mitra]

Is there an easy way (without metaprogramming) to let grind (or other tactic) synthesize typeclass parameters instead of infer_instance for certain classes?

In our project we use a data structure and a well-formedness (WF) predicate (we intentionally decided not to merge WF and data in the same structure - to separate code from proofs). We pass the [x.WF] as argument to many theorems, where x is a term of our data structure. However, in many cases, typeclass inference is not enough to synthesize the arguments, so we usually do:

have : x.WF := by grind
have : y.WF := by grind
have : z.WF := by grind
apply my_theorem

where my_theorem is something like theorem my_theorem {x y z : MyStruct} [x.WF] [y.WF] [z.WF] : someResult x y z. Is there a way to avoid explicitly stating necessary typeclass instances in the proof context and let grind infer them implicitly based on the theorem we applied or the rewriting rule we invoked?

[Shubakur Mitra]

We have tried

theorem my_theorem {x y z : MyStruct} (_ : x.WF := by grind)
    (_ : y.WF := by grind) (_ : z.WF := by grind) : someResult x y z

but it is very unpleasant to work with.

[Floris van Doorn]

The intended way is indeed

theorem my_theorem {x y z : MyStruct} (_ : x.WF := by grind)
    (_ : y.WF := by grind) (_ : z.WF := by grind) : someResult x y z

There is an undesired interaction between certain tactics (apply, rw, simp) and these "auto-params": lean#3475