∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (A : Subring K)
  [IsIntegrallyClosed ↥A] [IsFractionRing (↥A) K] (x : ↥(integralClosure (↥A) L)),
  Polynomial.map (algebraMap (↥A) K) (minpoly (↥A) x) = minpoly K ↑x