## Stream: new members

### Topic: Either Prime or Composite

#### Dev-Indra (Apr 26 2020 at 15:55):

Here is the theorem (either prime or composite) that I am trying to prove (I also gave some helper lemmas that are already proven). I created a lemma called dvd_n_less_than_n but I cannot seem to apply it. I commented this near the end of my theorem. Please help.

def dvd (m n: ℕ): Prop := ∃ k, n = m * k
def prime (p : ℕ) : Prop := p ≥ 2 ∧ ∀ n, dvd n p → n = 1 ∨ n = p
def composite (d : ℕ): Prop:= ∃ (a b: ℕ), d = a*b ∧ a ≤ b ∧ b < d

lemma greater_than_not_zero (n : ℕ)(n ≥ 2): n ≠ 0:=
begin
exact lattice.ne_bot_of_gt H,
end

lemma dvd_n_less_than_n (u n : ℕ) (ha: dvd u n) (hb: u ≠ 1) (hc: u ≠ n) (hn : n ≠ 0) : u < n :=
begin
refine lt_of_le_of_ne _ hc,
rcases ha with ⟨k, rfl⟩,
simpa using nat.mul_le_mul_left _ (_:1≤_),
refine nat.pos_iff_ne_zero.2 (mt _ hn),
rintro rfl, refl,
end

lemma either_prime_or_composite (n:ℕ ) (ge: n≥ 2): (¬ (prime n) ↔ composite n) :=
begin
split,
{
intros h,
rw prime at h,
rw composite,

push_neg at h,

cases h,
{
linarith,
} ,
{
cases h with u hu,
let hu_left:= hu.1,
rw dvd at hu_left,
cases hu_left with k hk,

have u_g_k : (u≤ k)∨ (u>k),
{
--               by library_search,
exact le_or_lt u k,
},
cases u_g_k,
{
use u,
use k,
split,
exact hk,
split,
exact u_g_k,

let hu_mid:= hu.2.1,

have u_ge_1 : (u≥ 1),
{
have u_zero: u=0,
{
linarith,
},
have n_zero: n=0,
{
subst u_zero,
simp at hk,
exact hk,
},
linarith,
},
have u_ge_2 : (u≥ 2),
{
have u_less_2 : u<2,
{
linarith,
},
have u_eq_1: u=1,
{
linarith,
},
--                    by library_search,
exact hu_mid u_eq_1,
},

have k_ge_n: k≥ n,
{
linarith,
},
have uk_ge_2n: u*k≥ 2* n,
{
--                    by library_search,
exact canonically_ordered_semiring.mul_le_mul u_ge_2 k_ge_n,
},
have n_ge_2n: n≥ 2*n,
{
linarith,
},
have twon_gt_n: 2*n > n,
{
linarith,
},
linarith,

},
{
use k,
use u,
split,
rw mul_comm at hk,
exact hk,
split,
--exact u_g_k,

let hu_mid:= hu.2.1,

have u_ge_1 : (u≥ 1),
{
have u_zero: u=0,
{
linarith,
},
have n_zero: n=0,
{
subst u_zero,
simp at hk,
exact hk,
},
linarith,
},
have u_ge_2 : (u≥ 2),
{
have u_less_2 : u<2,
{
linarith,
},
have u_eq_1: u=1,
{
linarith,
},
--                    by library_search,
exact hu_mid u_eq_1,
},

have k_ge_n: k≥ n,
{
linarith,
},
have uk_ge_2n: u*k≥ 2* n,
{
--                    by library_search,
exact canonically_ordered_semiring.mul_le_mul u_ge_2 k_ge_n,
},
have n_ge_2n: n≥ 2*n,
{
linarith,
},
have twon_gt_n: 2*n > n,
{
linarith,
},
linarith,

have ha: dvd u n, from and.left hu,
have h2: u ≠ 1 ∧ u ≠ n, from and.right hu,
have hc: u ≠ n, from and.right h2,
have hb: u ≠ 1, from and.left h2,
have hn: n ≠ 0,
{
exact lattice.ne_bot_of_gt ge,
}

--apply dvd_n_less_than_n,-- I have the lemma proved above but can't use it

},

split,
exact hk,

split,

have h3: u ≠ 1, from and.left h2,
refl,

--apply dvd_n_less_than_n, I have the lemma proved above but can't use it

}

},
{

}
end


#### Reid Barton (Apr 26 2020 at 16:03):

Please supply the correct imports, especially if you are pasting 200 lines of code already :upside_down:

#### Reid Barton (Apr 26 2020 at 16:04):

You're missing a comma before the first commented-out apply

#### Reid Barton (Apr 26 2020 at 16:04):

however, in my opinion the main problem is that your proof is too big and inefficient

#### Reid Barton (Apr 26 2020 at 16:05):

I can't get Lean to show the tactic state after apply dvd_n_less_than_n, and I suspect the reason is that the proof uses linarith about 20 times.

#### Dev-Indra (Apr 26 2020 at 16:09):

Thanks, it was the comma that was messing things up.

Last updated: May 08 2021 at 09:11 UTC