# Zulip Chat Archive

## Stream: new members

### Topic: Walking through an Irrationality Proof of Square Root of 2

#### Husnain Raza (Feb 07 2023 at 23:56):

Hey - I just picked up Lean a couple days ago and I'm working through a couple of classic proofs - would love some assistance as I make my way through some of them

```
import data.nat.basic
def coprime (p q : ℕ) : Prop := ( ∀ d : ℕ, ((∃ x y : ℕ, (p = d*x ∧ q = d*y)) → (d = 1)))
#eval coprime 5 6
#eval coprime 4 2
```

I've defined the following for determining if two numbers are coprime - however both of these return the same result; have I done something wrong?

#### Eric Wieser (Feb 08 2023 at 00:27):

The result for both is "I can't useful print this"

#### Eric Wieser (Feb 08 2023 at 00:29):

It's the same output as `#eval 2 + 2 = 4`

gives, right?

#### Eric Wieser (Feb 08 2023 at 00:29):

You need to ask lean to "decide" the proposition, which you can do by casting to `bool`

#### Husnain Raza (Feb 08 2023 at 22:06):

Im going to keep my questions in this thread as its the same proof that I am working on - I am currently trying to prove something similar to the following:

```
theorem test_theorem: (∃ x : ℕ, (2 * x = 10)) :=
begin
sorry,
end
```

what tactic(s) would i use in order to prove this? I should just be able to provide a solution (x=5), but not sure how to translate that into lean

#### David Renshaw (Feb 08 2023 at 22:07):

`use 5`

#### Husnain Raza (Feb 08 2023 at 22:09):

thanks!

#### Husnain Raza (Feb 08 2023 at 22:50):

is there an easy way to search for theorems besides scrolling through the mathlib docs? i vaguely know what i want to do (need something along the lines of x+1 = y+1 \implies x = y), but I'm not sure how to find such a theorem efficiently

#### David Renshaw (Feb 08 2023 at 22:53):

#### Husnain Raza (Feb 08 2023 at 23:06):

Thanks for the help! This proof is coming together, its like an intro proof class all over again :grinning_face_with_smiling_eyes:

#### Husnain Raza (Feb 08 2023 at 23:35):

```
lemma all_integers_even_or_odd {n : ℕ} : (even n) ∨ (odd n) :=
begin
induction n with j,
{
-- 0 is even as 0 = 2*0
rewrite even,
use 0,
ring,
},
{
rw odd, rw even, rw succ_eq_add_one,
rw odd at n_ih, rw even at n_ih,
cases n_ih, {
-- case that j is even
have h1 : (∃ l: ℕ, (j+1 = 2*l+1) ), by begin {
cases n_ih with l',
use l',
finish,
}
end,
finish,
},
{
-- case that j is odd
have h2 : (∃ l: ℕ, (j+1 = 2*l) ), by begin {
cases n_ih with l',
use l'+1,
finish,
}
end,
finish,
},
}
end
```

this was probably unnecessary but any feedback would be appreciated

#### Eric Wieser (Feb 09 2023 at 01:29):

A good next step would be to try to replace `finish`

with `simp`

, `ring`

or some other action; that way, you can learn the steps it's taking

#### Eric Wieser (Feb 09 2023 at 01:29):

`by begin { ... } end`

is better spelt `{ ... }`

!

#### Husnain Raza (Feb 09 2023 at 01:51):

that is better spelt

#### Husnain Raza (Feb 09 2023 at 01:52):

im almost done with implementing Euclid's proof of the irrationality of sqrt 2 - after that I'll go through and polish it up

#### Kevin Buzzard (Feb 10 2023 at 02:09):

`finish`

really slows your code down and makes the game less fun. Too many orange bars.

Last updated: Dec 20 2023 at 11:08 UTC