minimal imports to have the goodies?

Stream: general

[Siyuan Yan]

new user of mathlib here, was trying something simple

open nat

example (q d : ℕ) (hqd: q ≥ 2 ∧ d ≥ 2) (a: ℤ) : int.gcd a d = 1 ∧ int.gcd a q = 1 ↔ int.gcd a q = 1 :=
begin
split,
-- ...
end

But then I find basic things like rintro, linarith and library_search missing. What's a sane default import to have those things?

[Adam Topaz]

import tactic

[Siyuan Yan]

that worked thanks

[Kevin Buzzard]

@Siyuan Yan if you posted in #new members then you wouldn't have to continually apologise for being a new user, it would be taken for granted :-) Please continue to ask questions, it's definitely the best way to learn :-)

[Siyuan Yan]

Thanks! I didn't know the channel existed
Kevin Buzzard said:

Siyuan Yan if you posted in #new members then you wouldn't have to continually apologise for being a new user, it would be taken for granted :-) Please continue to ask questions, it's definitely the best way to learn :-)

[Kevin Buzzard]

PS are you sure about your simple theorem? What if a=d=2 and q=3?

[Adam Topaz]

Kevin Buzzard said:

Siyuan Yan if you posted in #new members then you wouldn't have to continually apologise for being a new user, it would be taken for granted :-) Please continue to ask questions, it's definitely the best way to learn :-)

Yes, #new members is probably the best channel for questions like this, but let me reemphasize that you should continue to ask questions!