mathlib

92d508a7 - chore(*): import tactic.basic as early as possible, and reduce imports (#3333)

chore(*): import tactic.basic as early as possible, and reduce imports (#3333) As discussed on [zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/import.20refactor.20and.20library_search), #3235 had the unfortunate effect of making `library_search` and `#where` and various other things unavailable in many places in mathlib. This PR makes an effort to import `tactic.basic` as early as possible, while otherwise reducing unnecessary imports. 1. import `tactic.basic` "as early as possible" (i.e. in any file that `tactic.basic` doesn't depend on, and which imports any tactic strictly between `tactic.core` and `tactic.basic`, just `import tactic.basic` itself 2. add `tactic.finish`, `tactic.tauto` and `tactic.norm_cast` to tactic.basic (doesn't requires adding any dependencies) 3. delete various unnecessary imports Co-authored-by: Scott Morrison <scott.morrison@gmail.com>