## Stream: new members

### Topic: chained ors

#### Anas Himmi (Apr 10 2020 at 16:09):

is it possible to express something like this?

∀ a n:ℕ, a < n → a = 0 ∨ a = 1 ∨ ... ∨ a = n


#### Kenny Lau (Apr 10 2020 at 16:11):

it's a meta theorem known as... fin_cases?

thank you

#### Kevin Buzzard (Apr 10 2020 at 16:28):

If you go to the tactic docs page and click on "filter by tag" in the top left and then "case bashing" you'll see that it's interval_cases, and you'll see how to work it too :-)

#### Anas Himmi (Apr 10 2020 at 16:32):

Exactly what i was looking for, thank you

#### Kevin Buzzard (Apr 10 2020 at 16:33):

We're trying to figure out how to make the docs brilliant. Any comments welcome.

#### Anas Himmi (Apr 10 2020 at 16:52):

I will try thinking about it too

#### Patrick Massot (Apr 10 2020 at 17:00):

Anas, are you interested in a specific value of n, or the general statements? Both are expressible of course, but their uses are pretty different.

#### Anas Himmi (Apr 10 2020 at 18:35):

What i want is, for every particular n, i can decompose the goal into subgoal.

#### Anas Himmi (Apr 11 2020 at 17:33):

when I import tactic.interval_cases, I get the error

invalid import: tactic.interval_cases
could not resolve import: tactic.interval_cases


Is it because I have an old version of mathlib?

#### Johan Commelin (Apr 11 2020 at 17:36):

Which version do you have?

#### Johan Commelin (Apr 11 2020 at 17:36):

Can you run git log?

#### Johan Commelin (Apr 11 2020 at 17:36):

(I don't know what system you are on. But if you can find a terminal, and run git log in your mathlib directory, then you will see when the latest commit was.)

i am on ubuntu

#### Anas Himmi (Apr 11 2020 at 17:37):

where can i found it?

#### Anas Himmi (Apr 11 2020 at 17:37):

it gives me an error saying it does not contain any commit

#### Anas Himmi (Apr 11 2020 at 17:39):

in mathlib/leanpkg.toml

[package]
name = "mathlib"
version = "0.1"
lean_version = "3.4.2"
path = "src"

[dependencies]


#### Kevin Buzzard (Apr 11 2020 at 17:46):

Are you running Lean in a project?

#### Kevin Buzzard (Apr 11 2020 at 17:47):

Is your project equal to mathlib, or do you have another project with mathlib as a dependency?

#### Anas Himmi (Apr 11 2020 at 17:51):

i installed lean from here https://github.com/leanprover-community/mathlib/blob/master/docs/install/debian.md, and am putting my files in Lean/my_project/src

Ok great.

#### Bryan Gin-ge Chen (Apr 11 2020 at 17:52):

Did you follow the instructions on setting up a Lean project here?

#### Kevin Buzzard (Apr 11 2020 at 17:52):

What happens if you change directory to Lean/my_project and then type leanproject up?

#### Kevin Buzzard (Apr 11 2020 at 17:53):

Do you have a leanpkg.toml in Lean/my_project?

#### Kevin Buzzard (Apr 11 2020 at 17:53):

Does leanproject up fix the problem? Wait until it terminates and then restart Lean in VS Code with Ctrl-Shift P

I do

#### Kevin Buzzard (Apr 11 2020 at 17:57):

Try source ~/.profile

#### Kevin Buzzard (Apr 11 2020 at 17:57):

and then see if leanproject works

#### Anas Himmi (Apr 11 2020 at 17:57):

i get the same error

#### Kevin Buzzard (Apr 11 2020 at 17:58):

You did this crazy wget -q https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile line?

#### Kevin Buzzard (Apr 11 2020 at 17:58):

The one in the page you linked to?

#### Kevin Buzzard (Apr 11 2020 at 17:58):

Installation should be easy on Ubuntu.

#### Anas Himmi (Apr 11 2020 at 17:58):

yes that's what i did

#### Kevin Buzzard (Apr 11 2020 at 17:59):

Did it work or did you get errors?

#### Anas Himmi (Apr 11 2020 at 17:59):

i don't remember getting errors

#### Kevin Buzzard (Apr 11 2020 at 17:59):

This should install leanproject. Without that, things are much harder.

#### Kevin Buzzard (Apr 11 2020 at 18:02):

Do you have a leanproject file in ~/.local/bin?

#### Kevin Buzzard (Apr 11 2020 at 18:02):

\$ ls ~/.local/bin/leanproject
/home/buzzard/.local/bin/leanproject


#### Kevin Buzzard (Apr 11 2020 at 18:02):

Do you get something like that?

i don't

#### Kevin Buzzard (Apr 11 2020 at 18:05):

Then let's start again. Try typing that crazy wget command, because it didn't finish the job it was supposed to do.

ok

#### Kevin Buzzard (Apr 11 2020 at 18:06):

Are you logged in as a user who can run sudo?

#### Kevin Buzzard (Apr 11 2020 at 18:06):

Maybe a better idea is to go though the detailed instructions so we can find out exactly what is failing.

#### Kevin Buzzard (Apr 11 2020 at 18:07):

But I guess there's no harm in trying the one-liner one more time.

#### Anas Himmi (Apr 11 2020 at 18:08):

now the leanproject up command works

#### Anas Himmi (Apr 11 2020 at 18:08):

i'm waiting it finishes

#### Kevin Buzzard (Apr 11 2020 at 18:08):

After it has finished, close and open VS Code, and see if the import works.

#### Kevin Buzzard (Apr 11 2020 at 18:09):

I usually open VS Code by typing code . when I am in the root directory of my project.

#### Kevin Buzzard (Apr 11 2020 at 18:09):

This way VS Code is guaranteed to open the right directory.

#### Anas Himmi (Apr 11 2020 at 18:09):

now the import works!!

thank you!!

#### Anas Himmi (Apr 11 2020 at 18:10):

:grinning_face_with_smiling_eyes:

#### Kevin Buzzard (Apr 11 2020 at 18:10):

No problem! Now go and do some maths :-)

#### Anas Himmi (Apr 11 2020 at 18:12):

yeay

Last updated: May 16 2021 at 05:21 UTC