class instance in hypothesis

Stream: Is there code for X?

[Chase Norman]

Is it possible to have the lean type system recognize class instances in hypotheses? In tactic mode I have the following error:

failed to synthesize type class instance for
V X : Type,
a : fintype X,
b : nonempty X,
c : fintype V,
d : nonempty V,
P : Profile V X
⊢ nonempty V

Clearly, the hypothesis d has the required information. How can I make it accessible via tactic mode? Variables a through d were achieved through intros on a Pi type. Thanks!

[Eric Wieser]

apply_instance will close that goal, as I think will assumption

[Chase Norman]

Unfortunately, this is not a goal. It is an error that arises when I attempt to use a function that requires a nonempty fintype as input.

[Chase Norman]

is there a way that I can have it surface these errors as a goal instead of failing?

[Eric Wieser]

Can you give a #mwe?

[Eric Wieser]

(at a guess, you're looking for tactic#resetI)

[Bryan Gin-ge Chen]

You might be able to use @ in front of that function and supply the instance manually.

[Chase Norman]

introsI was exactly what I was looking for, thanks!

[Kevin Buzzard]

In general, the type class system knows about everything "before the colon" (in a theorem statement) but doesn't know about things which appear after the colon, or which show up later. The ...I tactics are a way of inserting stuff which shows up in other ways, into the type class system.