## Stream: new members

### Topic: Extracting from a forall

#### Dev-Indra (Apr 26 2020 at 17:22):

Suppose I am given ha: ∀ (n_1 : ℕ). How do I extract this n_1 for my proof? When we are given an existential statement we can uses cases h1 with u hu. Is there an analogous way for forall?

#### Dev-Indra (Apr 26 2020 at 17:23):

As an example here is my tactic state:

n : ℕ,
ge : n ≥ 2,
a : n ≥ 2 ∧ ∀ (n_1 : ℕ), dvd n_1 n → n_1 = 1 ∨ n_1 = n,
a1 b : ℕ,
hb : n = a1 * b ∧ a1 ≤ b ∧ b < n,
h1 : n = a1 * b,
temp : a1 ≤ b ∧ b < n,
h2 : a1 ≤ b,
h3 : b < n
⊢ false


#### Dev-Indra (Apr 26 2020 at 17:24):

and just in case def dvd (m n: ℕ): Prop := ∃ k, n = m * k

#### Jalex Stark (Apr 26 2020 at 17:34):

forall meant that you get the property for any n_1 whatsoever. You should be feeding it a witness, not the other way around!

#### Jalex Stark (Apr 26 2020 at 17:35):

code is generally preferred to tactic states by people trying to give help, since then we can recreate the tactic state in our own environment and figure out what works

#### Dev-Indra (Apr 26 2020 at 17:36):

So how do I feed in a witness?

it's a function

#### Jalex Stark (Apr 26 2020 at 17:37):

so for example a.right b : dvd b n → b = 1 ∨ b = n

#### Dev-Indra (Apr 26 2020 at 17:37):

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 composite_not_prime (n:ℕ ) (ge: n≥ 2): ( composite n ==> ¬ (prime n) ) :=
begin
intros h,
rw composite at h,
rw prime at a,

cases h with a1 ha1,
cases ha1 with b hb,

have h1: n = a1*b, from and.left hb,
have temp: a1 ≤ b ∧ b < n, from and.right hb,
have h2: a1 ≤ b, from and.left temp,
have h3: b < n, from and.right temp,
end


#### Dev-Indra (Apr 26 2020 at 17:38):

So how would I use this function in my code above?

#### Dev-Indra (Apr 26 2020 at 17:39):

I want to use by statement h1 in my tactic state previously to show that dvd n b I want to use b as my n_1.

#### Jalex Stark (Apr 26 2020 at 17:40):

Like I said before, a.right b should be a term whose type is interesting to you

#### Jalex Stark (Apr 26 2020 at 17:40):

you could write e.g. have hb := a.right b,

#### Dev-Indra (Apr 26 2020 at 17:42):

@Jalex Stark Thanks

#### Jalex Stark (Apr 26 2020 at 17:44):

what's the deal with this ==> arrow? it doesn't compile for me ant I had to replace it with →

#### Bryan Gin-ge Chen (Apr 26 2020 at 17:45):

The ASCII version of → should be ->.