Maths_in_lean book example.

Stream: new members

[Manoj Kummini]

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]

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]

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

[Kevin Buzzard]

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

[Manoj Kummini]

Thank you!