chore(tactic/elementwise): fixes (#7188)
These fixes, while an improvement, still don't fix the problem @justus-springer observed in #7092.
Really we should generate a second copy of the `_apply` lemma, with the category specialized to `Type u`, and in that one remove all the coercions. Maybe later.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
