Lean doesn't recognize byContradiction / by_contra tactics

Stream: new members

[Michael Novak]

I opened in nvim a new lean file which I named testing.lean. Then I started writing a few simple exercises, which worked well without any problem. Now I wanted to prove something by contradiction so I started with open Classical, then I started the proof and everything worked until the moment I started the proof by contradiction part - I got error message unknown tactic - both for byContradiction and by_contra (what's the difference between the two by the way?).
I suspect that maybe I should import something, maybe mathlib? This is the first time I open a lean file by my self - until now I used the files of the Math in Lean textbook, so I'm not sure exactly how to import libraries like mathlib and weather that's even relevant in this case because I didn't get any error on line open Classical so I assume this doesn't require mathlib, right?

[David Renshaw]

The by_contra tactic is defined in Batteries: https://github.com/leanprover-community/batteries/blob/8da40b72fece29b7d3fe3d768bac4c8910ce9bee/Batteries/Tactic/Init.lean#L30-L46

[Michael Novak]

what are Batteries?

[Ruben Van de Velde]

It's a library that you can depend on from your lakefile

[Michael Novak]

what is my lakefile?

[Michael Novak]

I just created a file named testing. lean, so maybe I should have done more, but I just don't know what (I'm not using VS code).

[Ruben Van de Velde]

Oh, if you want to write anything more than the most trivial of code, you'd best create a project using lake, which will allow you to depend on other projects

[Kenny Lau]

@Michael Novak you might want to consider setting up mathlib4 as dependency

[Michael Novak]

O.k, I followed the instructions here for creating a new lean project and now everything works. Sorry for being stupid and wasting your time, that's just not explained in the math in lean textbook (at least not in the first 4 chapters that I read).

[Ruben Van de Velde]

No worries, we're here to help

[Kevin Buzzard]

(especially in this channel, which is precisely for "I'm getting started and am stuck at some point on the gigantic learning curve" questions)