Use instances with local hypothesis

Stream: maths

[Filippo A. E. Nuccio]

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]

For question 2, haveIor letI makes hs an instance, meaning that the system then finds it like it was written [...] in the statement.

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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