Surprising timeout

Stream: general

[Anne Baanen]

Quiz question: if you take commit 2cfba3dd and add the following declaration before the last line of src/intermediate_field/adjoin.lean, which one will work and which one will time out? (Note that docs#intermediate_field.adjoin.power_basis has one explicit argument, namely is_integral).

:a:

noncomputable def power_basis_of_finite_of_separable
  [finite_dimensional F E] (F_sep : is_separable F E) :
  power_basis F E :=
let α := (exists_primitive_element F_sep).some in
have e : F⟮α⟯ = ⊤ := (exists_primitive_element F_sep).some_spec,
power_basis.map (@adjoin.power_basis _ _ _ _ _ _ (F_sep.is_integral α))
  ((intermediate_field.equiv_of_eq e).trans intermediate_field.top_equiv)

or :b:

noncomputable def power_basis_of_finite_of_separable
  [finite_dimensional F E] (F_sep : is_separable F E) :
  power_basis F E :=
let α := (exists_primitive_element F_sep).some in
have e : F⟮α⟯ = ⊤ := (exists_primitive_element F_sep).some_spec,
power_basis.map (adjoin.power_basis (F_sep.is_integral α))
  ((intermediate_field.equiv_of_eq e).trans intermediate_field.top_equiv)

Spoiler

[Anne Baanen]

Spoiler 2: I ended up going with this