## Stream: new members

### Topic: Maths_in_lean book example.

#### Manoj Kummini (Sep 24 2020 at 20:49):

Dear all,

I am trying to learn lean and mathlib, and am working through the book mathematics_in_lean. In Section 2.1, there is an example of a typical proof state', which I am trying to set up and solve as follows:

import data.nat.parity data.nat.prime tactic
open nat

example (x y : nat) : (prime x) /\ not (even x) /\ (y > x) -> (y >= 4) :=
begin
intros h,
have h1,
exact (h.left),
have h23,
exact (h.right),
have h2,
exact (h23.left),
have h3,
exact(h23.right),
clear h h23,
-- now I have a proof state as given in the book!
-- I now tried
have x_ge_two,
apply prime.two_le h1


which got me x_ge_two : 2 <= x. After this, I am unable to use the the remaining hypothesis (h2 and h3). Any hint would be appreciated! Thanks.

#### Kevin Buzzard (Sep 24 2020 at 21:12):

import data.nat.parity data.nat.prime tactic
open nat

example (x y : nat) : (prime x) /\ not (even x) /\ (x < y) -> (4 ≤ y) :=
begin
intros h,
have h1,
exact (h.left),
have h23,
exact (h.right),
have h2,
exact (h23.left),
have h3,
exact(h23.right),
clear h h23,
-- now I have a proof state as given in the book!
-- I now tried
have x_ge_two,
apply prime.two_le h1,
-- 2 ≤ x ↔ 2 < x or 2 = x
rw le_iff_lt_or_eq at x_ge_two,
cases x_ge_two,
{ -- 2 < x case
-- use lemma saying a < b ↔ a+1 ≤ b
rw [←succ_le_iff, succ_eq_add_one] at x_ge_two h3,
-- now it's easy
linarith,
},
{ -- 2 = x case
-- proof by contradiction
exfalso,
apply h2,
rw ←x_ge_two,
simp,
}

end


#### Kevin Buzzard (Sep 24 2020 at 21:15):

It's a bit annoying that I couldn't finish it off more quickly

#### Kevin Buzzard (Sep 24 2020 at 21:15):

Maybe I'm missing a tactic. Actually does tidy` do it?

#### Manoj Kummini (Sep 25 2020 at 01:19):

Thank you!

Last updated: May 16 2021 at 21:11 UTC