Lean searching for subsingleton?

Stream: general

[Kenny Lau]

https://gist.github.com/kckennylau/2b5890b44f2f66196254a50e9fd6fa96#file-subsingleton-L727
What motivates Lean to use 10 second to search for a subsingleton instance?

[Kenny Lau]

The code was

theorem monic_X_sub_C' (x : α) : monic (X - C x) :=
by unfold monic leading_coeff nat_degree degree coeff

[Kenny Lau]

but I'm afraid one cannot reproduce this because I modified polynomials in some other ways

[Kenny Lau]

So unfortunately my link would have to suffice

[Kenny Lau]

Actually the subsingleton thing might not be related at all

[Kenny Lau]

I really don't know why Lean uses 10 seconds to elaborate the type

[Kenny Lau]

How will it scale when our library gets 2 times bigger?

[Kenny Lau]

Would we need a day to compile the mathlib?

[Kenny Lau]

We only have ~260 files now

[Kenny Lau]

also very strangely, if I go to my sandbox and import data.polynomial and do exactly the same thing, it compiles in a fraction in a second

[Kenny Lau]

despite the environment being the same

[Kevin Buzzard]

You have been posting some very hard-to-reproduce issues recently

[Mario Carneiro]

Usually searches for subsingleton instances are prompted by congr (also used inside simp), which will use subsingleton instances to avoid some subgoals

[Kenny Lau]

ok