deterministic craziness

Stream: general

[Johan Commelin]

Consider the following example:

import ring_theory.adjoin_root
import ring_theory.integral_closure

open algebra
variables {k : Type*} [discrete_field k]
variables {L : Type*} [discrete_field L] [algebra k L]
variables (L_alg : ∀ x : L, is_integral k x)
variables (f : polynomial L) (hif : irreducible f)

instance : algebra L (adjoin_root f) :=
algebra.of_ring_hom coe $ by apply_instance

include L_alg --hif

lemma alg_trans (x : comap k L (adjoin_root f)) : is_integral k x :=
_

If you remove the -- in the include statement, you get a timeout.

[Johan Commelin]

I have zero understanding of why. Adding the assumption that f is irreducible seems completely harmless.

[Johan Commelin]

@Sebastian Ullrich Why can the mere adding of an assumption cause timeouts?

[Chris Hughes]

The instance saying adjoin_root is a field depends on irreducible f

[Johan Commelin]

But why would that matter?

[Johan Commelin]

I don't need that instance

[Chris Hughes]

You need a ring or comm_ring instance presumably, and that instance would provide a path.