mathlib3

c0afa80e - chore(tactic/simp_result): forgot to import in tactic.basic (#2462)

chore(tactic/simp_result): forgot to import in tactic.basic (#2462) When I write a new tactic, I tend not to import it into `tactic.basic` or `tactic.interactive` while testing it and PR'ing it, to save having to recompile the whole library every time I tweak the tactic. But then, inevitably, I forget to add the import before the review process is finished. This imports `simp_result`, from #2356, into `tactic.basic`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>