!4#5071 FieldTheory.PrimitiveElement

Stream: mathlib4

[Jeremy Tan]

!4#5071 right, how do I fix the last error in this file? There's a subtype I can't get rid of

rw [← eq_X_sub_C_of_separable_of_root_eq h_sep h_root h_splits h_roots]
  trans EuclideanDomain.gcd (?_ : E[X]) (?_ : E[X])
  · dsimp only
    convert (gcd_map (algebraMap F⟮γ⟯ E)).symm
  · simp [map_comp, Polynomial.map_map, ← IsScalarTower.algebraMap_eq] -- here

⊢ EuclideanDomain.gcd
    (Polynomial.map (algebraMap { x // x ∈ F⟮γ⟯ } E)
      (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮α + c • β⟯ }) (minpoly F α))
        (↑C (AdjoinSimple.gen F (α + c • β)) -
          ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮α + c • β⟯) } * X)))
    (Polynomial.map (algebraMap { x // x ∈ F⟮γ⟯ } E)
      (Polynomial.map (algebraMap F { x // x ∈ F⟮α + c • β⟯ }) (minpoly F β))) =
  h

[Eric Wieser]

Maybe try squeezing the simp in mathlib3/mathlib4 and seeing what's different?

[Damiano Testa]

I was going to take a look, but it is green now and marked as help-wanted: is it ready for review, instead?

[Scott Morrison]

I've hit merge.

[Anne Baanen]

This PR depends on SplittingField.Construction which is receiving forward ports at the moment, and that thread suggests not merging it yet: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234891.20.20FieldTheory.2ESplittingField/near/366437263