unrelated build failure in !4#4831

Stream: mathlib4

[Eric Wieser]

This PR, !4#4831, (about tensor products) is causing a build failure (about proving sqrt 5 ≠ 0 in the context of the golden ratio). Is this a cache collision somehow? Is simp being non-deterministic in some way?

[Eric Wieser]

Ah, this was caused by a import Mathlib.Tactic being removed

[Eric Wieser]

Should we have a lint rule that forbids import Mathlib.Tactic?

[Alex J. Best]

Made !4#4991 for that

[Eric Wieser]

LGTM, let's wait for a third opinion that we want to forbid that import

[Kevin Buzzard]

I wrote the file Mathlib.Tactic for teaching purposes and it's serving its purpose well. In Lean 4 import Mathlib is ridiculously quick but it feels a bit dirty.

[Alex J. Best]

Yeah my thinking was that we had this linter rule in mathlib 3, then when mathlib 4 started there was no "import tactic" until Kevin came along and made it which is very useful, but hopefully having the same linter as we had in mathlib 3 should be uncontroversial, but its of course good to have the discussion