# Zulip Chat Archive

## Stream: maths

### Topic: Use instances with local hypothesis

#### Filippo A. E. Nuccio (Mar 05 2021 at 13:22):

I am trying to understand how instances work and I ran across the following examples.

```
lemma one {S : Type*} (hs : integral_domain S) : comm_cancel_monoid_with_zero S := by apply_instance
```

is OK, while

```
lemma two {S : Type*} [ring S] (f : ℤ ≃+* S) : comm_cancel_monoid_with_zero S :=
begin
have hs : integral_domain S, sorry,
apply_instance
end
```

is not OK (a part from the fact that I can prove `hs`

using `f`

, but I've sorried it to be short). So I understand that when Lean looks for assumptions that would match instances, it looks in the hypothesis of the statement, but not on "new" ones. Is it really so? If yes, I have two questions:

1) What is the difference between an "assumed" hypothesis and one which has been "constructed" along the way?

2) How to `apply_instance`

if the needed assumption was not part of the hypothesis, as in my `lemma two`

?

#### Riccardo Brasca (Mar 05 2021 at 13:25):

For question 2, `haveI`

or `letI`

makes `hs`

an instance, meaning that the system then finds it like it was written `[...]`

in the statement.

#### Kevin Buzzard (Mar 05 2021 at 13:25):

The "system" which makes `apply_instance`

work is called the type class inference system. It is initialised at the beginning of a proof in the following way: Lean looks at everything before the colon which is a term of a typeclass (like your first `hs`

) and puts it into the system. Then, by default, it never puts anything else into the system.

To make your lemma 2 work you need to put `haveI : integral_domain S`

(or probably `letI : integral_domain S`

because I think it's data) -- this tactic specifically is designed to change the system.

#### Filippo A. E. Nuccio (Mar 05 2021 at 13:26):

Wow, perfect! Thanks (indeed, it works): the nice caveat is that it does not accept my sorry, the docs says

The syntax is the same as have, but the proof-omitted version is not supported. For this one must write have : t, { <proof> }, resetI, <proof>.

#### Kevin Buzzard (Mar 05 2021 at 13:27):

Note that, as Patrick reminded us yesterday (and Mario told me about a year ago), you don't need hs to be in square brackets in lemma 1 -- Lean just looks at everything before the colon. The reason you should put `[integral_domain S]`

in square brackets instead is for people who want to *use* your lemma, not to help you prove it yourself.

#### Filippo A. E. Nuccio (Mar 05 2021 at 13:28):

Meaning it could be in curly ones? (You can also simply point at Patrick's chat)

#### Kevin Buzzard (Mar 05 2021 at 19:40):

Yes, any terms of type `C`

where `C`

is in a class, if they're defined before the colon, will end up in the instance cache. It doesn't matter what brackets are being used, I believe...

Last updated: May 14 2021 at 18:28 UTC