splitting field timeout

Stream: general

[Johan Commelin]

What's going on?

import field_theory.splitting_field

variables {K : Type*} [field K] {f : polynomial K}

noncomputable theory

example : algebra K f.splitting_field := by apply_instance

/-- The canonical isomorphism between
the splitting field of a polynomial that splits and the base field. -/
def equiv_of_splits (h : polynomial.splits (ring_hom.id K) f) :
  f.splitting_field ≃ₐ[K] K := -- deterministic timeout
sorry

[Johan Commelin]

@Mario Carneiro @Gabriel Ebner Can we somehow improve the diagnostics?

[Johan Commelin]

It would be very helpful if lean could give me a bit more hints about what is timing out.

[Johan Commelin]

This seems to work. But as soon as I uncomment the final tc search, it blows up.

/-- The canonical isomorphism between
the splitting field of a polynomial that splits and the base field. -/
def equiv_of_splits (h : polynomial.splits (ring_hom.id K) f) :
  @alg_equiv K f.splitting_field K
  (by { apply_instance })
  (by { /- apply_instance -/ })
  (by { apply_instance })
  (by { apply_instance })
  (by { apply_instance })
   := -- deterministic timeout
sorry

[Kenny Lau]

what is it searching?