add Mathlib.Tactic.Common, and import !4#4056

Stream: PR reviews

[Scott Morrison]

This makes a mathlib4 version of mathlib3's tactic.basic, now called Mathlib.Tactic.Common, which imports all tactics which do not have significant theory requirements, and then is imported all across the base of the hierarchy.

This ensures that all common tactics are available nearly everywhere in the library, rather than having to be imported one-by-one as you need them.

[Kevin Buzzard]

You clearly imported LibrarySearch once too often :-) (I had imported Ring and Linarith once too often and that's why I made Mathlib/Tactic.lean)

[Eric Wieser]

Can we port #assert_not_exists first so that we can prevent unwanted dependencies appearing here?

[Scott Morrison]

#assert_not_exists is only ever used in mathlib3 for theory, not for tactics, so it should be irrelevant here.

[Eric Wieser]

My point is that we should add #assert_not_exists SomeBasicTheory to the tactic/common file

[Scott Morrison]

What would you want to put there? I think we are already protected against this by the fact that we have import Mathlib.Tactic.Common in all the basic theory files, so if something gets imported accidentally, there will be an import loop.

[Scott Morrison]

:ping_pong: