## Stream: new members

### Topic: fact?

#### Damiano Testa (Mar 25 2021 at 14:06):

Dear All,

I am trying to fix a now broken proof and I am stuck with proving the lemma below: how do I extract the fact from the fact?

Thanks!

import data.nat.prime

lemma obvious (p : ℕ) [fact (nat.prime p)] :
nat.prime p :=
begin
sorry
end


#### Adam Topaz (Mar 25 2021 at 14:09):

assumption will work here, I suppose

#### Damiano Testa (Mar 25 2021 at 14:09):

I tried it:

assumption tactic failed
state:
p : ℕ,
_inst_1 : fact (nat.prime p)
⊢ nat.prime p


#### Adam Topaz (Mar 25 2021 at 14:09):

Or you can name the fact [ h : fact ... ]

Hmmmm....

#### Ruben Van de Velde (Mar 25 2021 at 14:10):

apply fact.out seems to work

#### Damiano Testa (Mar 25 2021 at 14:10):

This gives:

lemma obvious (p : ℕ) [h : fact (nat.prime p)] :
nat.prime p :=
begin
exact h,
-- invalid type ascription, term has type
--   fact (nat.prime p)
-- but is expected to have type
--   nat.prime p
end


#### Adam Topaz (Mar 25 2021 at 14:11):

Oh did fact change?

#### Ruben Van de Velde (Mar 25 2021 at 14:13):

Also apply fact.elim, assumption or apply fact.elim, apply_instance. Not sure what's the intended approach

#### Damiano Testa (Mar 25 2021 at 14:14):

For the record, this works:

lemma obvious (p : ℕ) [h : fact (nat.prime p)] :
nat.prime p :=
fact.out _


and also

lemma obvious (p : ℕ) [h : fact (nat.prime p)] :
nat.prime p :=
fact.elim h


Thanks Ruben!

#### Eric Wieser (Mar 25 2021 at 14:28):

Yes, fact changed

#### Eric Wieser (Mar 25 2021 at 14:28):

Because @[class] def isn't allowed by one of mathport and lean4

#### Mario Carneiro (Mar 25 2021 at 16:56):

You can also use h.1

#### Damiano Testa (Mar 25 2021 at 17:22):

Thanks, Mario! I was convinced that I had tried to project, but... apparently not!

#### Manuel Candales (Apr 01 2021 at 23:56):

How can I do the opposite? Get a fact from a hypothesis. For example, I have h : nat.prime p. How do I use that in a theorem like zmod.exists_pow_two_eq_neg_one_iff_mod_four_ne_three?

#### Alex J. Best (Apr 02 2021 at 00:01):

In tactic mode you should be able to do haveI := fact.mk h (untested)

#### Manuel Candales (Apr 02 2021 at 00:08):

wow, thanks! yeah that works

#### Johan Commelin (Apr 02 2021 at 04:43):

If fact foo is your goal, then you can also write \<h\>, where \< and \> are the things you type into VScode to get the funny angle brackets.

Last updated: May 11 2021 at 00:31 UTC