mathlib3

9a425726 - feat(tactic/apply'): apply without unfolding type definitions (#1234)

feat(tactic/apply'): apply without unfolding type definitions (#1234) * feat(tactic/apply'): apply without unfolding type definitions * Update src/tactic/interactive.lean Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com> * improve doc * more doc * Update core.lean * add test case * add test case * improve treatment of type class instances for apply' * tweak application of instance resolution * fix * move `apply'` to its own file * adjust docs * import apply from tactic.default * fix import in test * Update tactics.lean