## 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 ->.