Tactics import

Stream: new members

[David⚛️]

I tried using some tactics to close up a goal in LEAN 4 but it was flagged (underlined).
Let's say I want to use simp, ring, etc. How do I know what to import for the given tactics?

[Alex J. Best]

You should be able to do import Mathlib.Tactic if your project has mathlib4 as a dependency and you have a recent enough version