# Zulip Chat Archive

## Stream: new members

### Topic: weird prime error

#### Mantas Baksys (Apr 15 2021 at 15:52):

I wanted to mess around with the prime numbers for a bit but quickly ran into this problem.

```
import tactic data.nat.prime topology.metric_space.basic
open_locale classical
open filter nat
noncomputable theory
def inv_prime : primes → ℝ := λ p, 1/p
instance primes.preorder: preorder primes := subtype.preorder _
instance primes.nonempty: nonempty primes := nonempty_of_inhabited
instance primes.semilattice_sup: semilattice_sup primes := order_dual.semilattice_sup {p // nat.prime p}
theorem test : tendsto inv_prime at_top (nhds (0: ℝ)) :=
begin
rw @metric.tendsto_at_top ℝ primes
real.pseudo_metric_space primes.nonempty primes.semilattice_sup inv_prime (0: ℝ),
end
```

As posted above I tried to supply all instances manually but it fails saying it can't find exactly what it's trying to find!

Also, `preorder primes`

was not automatic, is that intended (for the at_top part)? Thanks!

#### Kevin Buzzard (Apr 15 2021 at 15:56):

Lean seems to think there's two preorders on the primes, as you can see by `set_option pp.all true`

before the test. If you just comment out `instance primes.preorder`

it works.

#### Mantas Baksys (Apr 15 2021 at 16:01):

Thanks @Kevin Buzzard for the tool to check, will use that. So it turns out `preorder primes`

was automatic, how weird that I got an error about that before, sorry.

#### Kevin Buzzard (Apr 15 2021 at 16:03):

I'm pretty sure that the `semilattice_sup`

is giving you a preorder, and it might not be the preorder you want: what is this dual thing? You are ordering them twice in your code, with 2<=3 the first time and 3<=2 the second; this is why you were having problems.

#### Mantas Baksys (Apr 15 2021 at 16:38):

To be honest, I didn't look into it, I just looked at what the hypotheses were and then supplied them, just to check if I still got an error. I've now defined the correct `semilattice_sup`

via `subtype.semilattice_sup`

and I think I'll be good to go from here.

Anyways, isn't the idea here to not have to use `@`

before `metric.tendsto_at_top`

at all?

#### Alex J. Best (Apr 15 2021 at 17:43):

I think using a linear order is a cleaner setup that gives what you want.

```
import tactic data.nat.prime topology.metric_space.basic
open_locale classical
open filter nat
noncomputable theory
def inv_prime : primes → ℝ := λ p, 1/p
instance primes.linear_order : linear_order primes := subtype.linear_order _
theorem test : tendsto inv_prime at_top (nhds (0: ℝ)) :=
begin
rw metric.tendsto_at_top,
end
```

#### Alex J. Best (Apr 15 2021 at 17:44):

And yes, using that `@`

is sometimes a bad sign, as it means you are doing steps that the person who wrote the lemma thought should be automatic, sometimes it is necessary though.

#### Alex J. Best (Apr 15 2021 at 17:54):

One more thing: another approach is to make the definition of primes reducible locally, so that lean can see that it is just a subtype of nat, as most properties you need are just properties coming from the fact its a subtype of nat:

```
import tactic data.nat.prime topology.metric_space.basic
open_locale classical
open filter nat
noncomputable theory
def inv_prime : primes → ℝ := λ p, 1/p
local attribute [reducible] primes
theorem test : tendsto inv_prime at_top (nhds (0: ℝ)) :=
begin
rw metric.tendsto_at_top,
end
```

#### Mantas Baksys (Apr 15 2021 at 18:01):

Thanks @Alex J. Best , this is very useful and I'm sure will prevent a lot of future subtype headaches :smiley:. Just as a quick follow-up, how would one define 'the set of all primes less than p : primes' as a subset of primes? I can define it as `set ℕ`

but doing an equivalent thing for `primes`

gives a Type error.

I think I worked it out myself

```
import data.nat.prime
open_locale classical
open nat
noncomputable theory
local attribute [reducible] primes
def primes_le (p:primes) : set primes := λ q, q≤p
```

#### Alex J. Best (Apr 15 2021 at 18:34):

(deleted)

#### Scott Morrison (Apr 16 2021 at 00:17):

Better to write `{ q | q ≤ p }`

. One should pretend as much as possible that you don't know that "sets are just functions to Prop".

Last updated: May 11 2021 at 00:31 UTC