# Zulip Chat Archive

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

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

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?

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

Ruben, thanks! Your approach works!

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