mathlib3

5ed5f594 - feat(tactic/delta_instance): handle parameters and use in library (#1483)

feat(tactic/delta_instance): handle parameters and use in library (#1483) * feat(tactic/core): improve delta_instance handler * feat(*): use delta_instance derive handler * feat(tactic/delta_instance): cleaner handling of application under binders * Revert "feat(tactic/delta_instance): cleaner handling of application under binders" This reverts commit 4005a2fad571bf922c98f94cbc1154666abc259d. * comment apply_under_pis * properly get unused name * feat(tactic/delta_instance): run with high priority and don't run on inductives * Update src/tactic/core.lean Co-Authored-By: Floris van Doorn <fpvdoorn@gmail.com>