∀ {K : Type v} {L : Type w} [inst : Field K] [inst_1 : Field L] (i : K →+* L) {f : Polynomial K}
  (hf : (Polynomial.map i f).Splits) (hfd : (Polynomial.map i f).degree ≠ 0),
  Polynomial.rootOfSplits hf hfd = Polynomial.rootOfSplits hf ⋯