no goals
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
i : K →+* L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
p : F[X]
h : Splits (algebraMap F K) p
f : K →ₐ[F] L
⊢ ↑f '' rootSet p K = rootSet p L
classical
  rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, ← f.coe_toRingHom,
    ← roots_map _ ((splits_id_iff_splits (algebraMap F K)).mpr h), map_map, f.comp_algebraMap,
    ← rootSet]
no goals
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
i : K →+* L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
p : F[X]
h : Splits (algebraMap F K) p
f : K →ₐ[F] L
⊢ ↑f '' rootSet p K = rootSet p L
rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, ← f.coe_toRingHom,
  ← roots_map _ ((splits_id_iff_splits (algebraMap F K)).mpr h), map_map, f.comp_algebraMap,
  ← rootSet]