import Mathlib.Tactic issues

Stream: new members

[Newell Jensen]

When I put import Mathlib.Tactic at the top of Mathlib.Algebra.Order.Field.Basic I am getting errors where virtually all of the files contents are saying 'BLAH' has already been declared/aligned. I haven't been able to figure out why this is causing issues and wondering if there are some files in Mathlib that you just can't use import Mathlib.Tactic? I suspect it might be some sort of import cycle issue? If so, how does one verify that this is the case?

I am on commit ea02b9e2f48c3b5d2d9bd8208f25276ad4af7915.

[Kevin Buzzard]

Indeed I think that in all files in mathlib you can't put import Mathlib.Tactic, with the one exception being Mathlib.lean. The point of that file is to make teaching and writing other projects easier. If there is any tactic which uses ordered fields then it will definitely cause an inport loop.

[Newell Jensen]

So how does one get the tactics like rw? and apply? in this file? Reason I even put import Mathlib.Tactic at the top was because these showed up as unknown tactic when trying to use them. Usually within Mathlib I have access to the main tactics but I noticed in this file I don't.

[Kevin Buzzard]

You don't want those tactics imported in that file because you can't use those tactics in mathlib files.

[Kevin Buzzard]

Just make a scratch file, import whatever you like there, finish your proofs and then move them into the mathlib file.

[Patrick Massot]

You can also import the file defining the tactics.

[Kevin Buzzard]

But you might want to remove the import when you're done, if you do it that way. Right click on the tactic in a scratch file to find out where it's defined.

[Newell Jensen]

I am able to access tactics such as apply? in other Mathlib files and was surprised not to see them in this file, which led to the import attempt. How is it that this file doesn't have apply? but say Mathlib.GroupTheory.PresentedGroup does? I would suspect that this is set somewhere.

[Richard Copley]

Take a look at Mathlib.Tactic.Common, and the comment at the top near the bottom of it.

[Patrick Massot]

You can go to a file where a tactic work and Ctrl-click the tactic name.