which import statement(s) for beginners?

Stream: new members

[rzeta0]

As a beginner I'm working through the Mechanics of Proof - but i have found out it uses a modified dialect to make the journey easier. I agree with this approach if it helps beginners like me get past the initial barriers.

However, I'd like to start creating simple vanilla Lean 4 proofs - really simple ones. To do this I need to import a minimum set of libraries to enable me to use tactics such as ring, rw [hypothesis], gcongr,linarith and positivity.

What are the libraries I need to import? Are there several or just one? Should I import specific subsets of the library or import the whole massive mathlib? What is considered good practice?

[Kevin Buzzard]

import Mathlib.Tactic will give you all mathlib tactics.

[rzeta0]

Thanks Kevin.

The Mechanics of Proof courses uses Mathlib.Data.Real.Basic for its early code ... can I ask what it does? Does it complement import Mathlib.Tactic or is it a subset?

I have searched the web and can't find anything.

[Julian Berman]

docs#Mathlib/Data/Real/Basic

[Julian Berman]

(I give up.) It's https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Real/Basic.html

[Luigi Massacci]

That file contains a construction of the real numbers, and then some their basic properties, as you can see from its documentation page. You can still use (some) tactics just by importing it since imports are transitive, and that file in turn imports some tactics

[Luigi Massacci]

(deleted)

[Luigi Massacci]

Julian Berman said:

docs#Mathlib/Data/Real/Basic

I’m pretty sure you can’t link to the whole file with docs#, I always make the same mistake too… I think docs#Real is the best you can do

[Julian Berman]

(Yeah I rarely like using the linkifiers at all myself but seems looking now at the regex that you're right, if the pattern contains a dot it sends someone to /find, there's nothing that's just "take what I wrote literally and send someone there")

[Yaël Dillies]

Julian Berman said:

docs#Mathlib/Data/Real/Basic

The linkifier is file#Mathlib/Data/Real/Basic

[Julian Berman]

That takes you to GitHub though, not the docs.

[Yaël Dillies]

Oh, you want the docs...