[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : F[X]
inst✝ : IsSplittingField F L f
⊢ Splits (algebraMap K L) (Polynomial.map (algebraMap F K) f)
[PROOFSTEP]
rw [splits_map_iff, ← IsScalarTower.algebraMap_eq]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : F[X]
inst✝ : IsSplittingField F L f
⊢ Splits (algebraMap F L) f
[PROOFSTEP]
exact splits L f
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : F[X]
inst✝ : IsSplittingField F L f
⊢ Subalgebra.restrictScalars F (Algebra.adjoin K (rootSet (Polynomial.map (algebraMap F K) f) L)) =
    Subalgebra.restrictScalars F ⊤
[PROOFSTEP]
rw [rootSet, map_map, ← IsScalarTower.algebraMap_eq, Subalgebra.restrictScalars_top, eq_top_iff, ← adjoin_rootSet L f,
  Algebra.adjoin_le_iff]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : F[X]
inst✝ : IsSplittingField F L f
⊢ rootSet f L ⊆
    ↑(Subalgebra.restrictScalars F (Algebra.adjoin K ↑(Multiset.toFinset (roots (Polynomial.map (algebraMap F L) f)))))
[PROOFSTEP]
exact fun x hx => @Algebra.subset_adjoin K _ _ _ _ _ _ hx
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
⊢ ⊤ = ⊥
[PROOFSTEP]
rw [eq_bot_iff, ← adjoin_rootSet L f, rootSet, roots_map (algebraMap K L) h, Algebra.adjoin_le_iff]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
⊢ ↑(Multiset.toFinset (Multiset.map (↑(algebraMap K L)) (roots f))) ⊆ ↑⊥
[PROOFSTEP]
intro y hy
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
hy : y ∈ ↑(Multiset.toFinset (Multiset.map (↑(algebraMap K L)) (roots f)))
⊢ y ∈ ↑⊥
[PROOFSTEP]
rw [Multiset.toFinset_map, Finset.mem_coe, Finset.mem_image] at hy 
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
hy✝ : y ∈ ↑(Multiset.toFinset (Multiset.map (↑(algebraMap K L)) (roots f)))
hy : ∃ a, a ∈ Multiset.toFinset (roots f) ∧ ↑(algebraMap K L) a = y
⊢ y ∈ ↑⊥
[PROOFSTEP]
obtain ⟨x : K, -, hxy : algebraMap K L x = y⟩ := hy
[GOAL]
case intro.intro
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
hy : y ∈ ↑(Multiset.toFinset (Multiset.map (↑(algebraMap K L)) (roots f)))
x : K
hxy : ↑(algebraMap K L) x = y
⊢ y ∈ ↑⊥
[PROOFSTEP]
rw [← hxy]
[GOAL]
case intro.intro
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
hy : y ∈ ↑(Multiset.toFinset (Multiset.map (↑(algebraMap K L)) (roots f)))
x : K
hxy : ↑(algebraMap K L) x = y
⊢ ↑(algebraMap K L) x ∈ ↑⊥
[PROOFSTEP]
exact SetLike.mem_coe.2 <| Subalgebra.algebraMap_mem _ _
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : ⊤ = ⊥
⊢ Splits
    (RingEquiv.toRingHom
      (RingEquiv.trans (RingEquiv.ofBijective (algebraMap K L) (_ : Function.Bijective ↑(algebraMap K L)))
        (RingEquiv.symm (RingEquiv.ofBijective (algebraMap K L) (_ : Function.Bijective ↑(algebraMap K L))))))
    f
[PROOFSTEP]
rw [RingEquiv.toRingHom_trans]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : ⊤ = ⊥
⊢ Splits
    (RingHom.comp
      (RingEquiv.toRingHom
        (RingEquiv.symm (RingEquiv.ofBijective (algebraMap K L) (_ : Function.Bijective ↑(algebraMap K L)))))
      (RingEquiv.toRingHom (RingEquiv.ofBijective (algebraMap K L) (_ : Function.Bijective ↑(algebraMap K L)))))
    f
[PROOFSTEP]
exact splits_comp_of_splits _ _ (splits L f)
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Algebra.adjoin F (rootSet (f * g) L) = ⊤
[PROOFSTEP]
rw [rootSet, Polynomial.map_mul, roots_mul (mul_ne_zero (map_ne_zero hf : f.map (algebraMap F L) ≠ 0) (map_ne_zero hg)),
  Multiset.toFinset_add, Finset.coe_union, Algebra.adjoin_union_eq_adjoin_adjoin, IsScalarTower.algebraMap_eq F K L, ←
  map_map, roots_map (algebraMap K L) ((splits_id_iff_splits <| algebraMap F K).2 <| splits K f), Multiset.toFinset_map,
  Finset.coe_image, Algebra.adjoin_algebraMap, ← rootSet, adjoin_rootSet, Algebra.map_top,
  IsScalarTower.adjoin_range_toAlgHom, ← map_map, ← rootSet, adjoin_rootSet, Subalgebra.restrictScalars_top]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
f : K[X]
inst✝ : IsSplittingField K L f
hf : Splits (algebraMap K F) f
hf0 : f = 0
⊢ L →ₐ[K] { x // x ∈ ⊥ }
[PROOFSTEP]
rw [← (splits_iff L f).1 (show f.Splits (RingHom.id K) from hf0.symm ▸ splits_zero _)]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
f : K[X]
inst✝ : IsSplittingField K L f
hf : Splits (algebraMap K F) f
hf0 : f = 0
⊢ L →ₐ[K] { x // x ∈ ⊤ }
[PROOFSTEP]
exact Algebra.toTop
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
f : K[X]
inst✝ : IsSplittingField K L f
hf : Splits (algebraMap K F) f
hf0 : ¬f = 0
⊢ { x // x ∈ ⊤ } →ₐ[K] F
[PROOFSTEP]
rw [← adjoin_rootSet L f]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
f : K[X]
inst✝ : IsSplittingField K L f
hf : Splits (algebraMap K F) f
hf0 : ¬f = 0
⊢ { x // x ∈ Algebra.adjoin K (rootSet f L) } →ₐ[K] F
[PROOFSTEP]
exact
  Classical.choice
    (lift_of_splits _ fun y hy =>
      have : aeval y f = 0 :=
        (eval₂_eq_eval_map _).trans <| (mem_roots <| map_ne_zero hf0).1 (Multiset.mem_toFinset.mp hy)
      ⟨isAlgebraic_iff_isIntegral.1 ⟨f, hf0, this⟩, splits_of_splits_of_dvd _ hf0 hf <| minpoly.dvd _ _ this⟩)
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
y : L
hy : y ∈ rootSet f L
hf : f = 0
⊢ IsIntegral K y
[PROOFSTEP]
rw [hf, rootSet_zero] at hy 
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
y : L
hy : y ∈ ∅
hf : f = 0
⊢ IsIntegral K y
[PROOFSTEP]
cases hy
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ IsSplittingField K L p
[PROOFSTEP]
constructor
[GOAL]
case splits'
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ Splits (algebraMap K L) p
[PROOFSTEP]
rw [← f.toAlgHom.comp_algebraMap]
[GOAL]
case splits'
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ Splits (RingHom.comp (↑↑f) (algebraMap K F)) p
[PROOFSTEP]
exact splits_comp_of_splits _ _ (splits F p)
[GOAL]
case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
p : K[X]
f : F ≃ₐ[K] L
inst✝ : IsSplittingField K F p
⊢ Algebra.adjoin K (rootSet p L) = ⊤
[PROOFSTEP]
rw [← (Algebra.range_top_iff_surjective f.toAlgHom).mpr f.surjective, adjoin_rootSet_eq_range (splits F p),
  adjoin_rootSet F p]
[GOAL]
F✝ : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : ∀ (x : L), x ∈ rootSet p L → x ∈ F
⊢ Splits (algebraMap K { x // x ∈ F }) p
[PROOFSTEP]
simp_rw [rootSet_def, Finset.mem_coe, Multiset.mem_toFinset] at hF 
[GOAL]
F✝ : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : ∀ (x : L), x ∈ roots (Polynomial.map (algebraMap K L) p) → x ∈ F
⊢ Splits (algebraMap K { x // x ∈ F }) p
[PROOFSTEP]
rw [splits_iff_exists_multiset]
[GOAL]
F✝ : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : ∀ (x : L), x ∈ roots (Polynomial.map (algebraMap K L) p) → x ∈ F
⊢ ∃ s,
    Polynomial.map (algebraMap K { x // x ∈ F }) p =
      ↑C (↑(algebraMap K { x // x ∈ F }) (leadingCoeff p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
[PROOFSTEP]
refine' ⟨Multiset.pmap Subtype.mk _ hF, map_injective _ (algebraMap F L).injective _⟩
[GOAL]
F✝ : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : ∀ (x : L), x ∈ roots (Polynomial.map (algebraMap K L) p) → x ∈ F
⊢ Polynomial.map (algebraMap { x // x ∈ F } L) (Polynomial.map (algebraMap K { x // x ∈ F }) p) =
    Polynomial.map (algebraMap { x // x ∈ F } L)
      (↑C (↑(algebraMap K { x // x ∈ F }) (leadingCoeff p)) *
        Multiset.prod
          (Multiset.map (fun a => X - ↑C a) (Multiset.pmap Subtype.mk (roots (Polynomial.map (algebraMap K L) p)) hF)))
[PROOFSTEP]
conv_lhs =>
  rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq, eq_prod_roots_of_splits h, ← Multiset.pmap_eq_map _ _ _ hF]
[GOAL]
F✝ : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : ∀ (x : L), x ∈ roots (Polynomial.map (algebraMap K L) p) → x ∈ F
| Polynomial.map (algebraMap { x // x ∈ F } L) (Polynomial.map (algebraMap K { x // x ∈ F }) p)
[PROOFSTEP]
rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq, eq_prod_roots_of_splits h, ← Multiset.pmap_eq_map _ _ _ hF]
[GOAL]
F✝ : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : ∀ (x : L), x ∈ roots (Polynomial.map (algebraMap K L) p) → x ∈ F
| Polynomial.map (algebraMap { x // x ∈ F } L) (Polynomial.map (algebraMap K { x // x ∈ F }) p)
[PROOFSTEP]
rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq, eq_prod_roots_of_splits h, ← Multiset.pmap_eq_map _ _ _ hF]
[GOAL]
F✝ : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : ∀ (x : L), x ∈ roots (Polynomial.map (algebraMap K L) p) → x ∈ F
| Polynomial.map (algebraMap { x // x ∈ F } L) (Polynomial.map (algebraMap K { x // x ∈ F }) p)
[PROOFSTEP]
rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq, eq_prod_roots_of_splits h, ← Multiset.pmap_eq_map _ _ _ hF]
[GOAL]
F✝ : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : ∀ (x : L), x ∈ roots (Polynomial.map (algebraMap K L) p) → x ∈ F
⊢ ↑C (↑(algebraMap K L) (leadingCoeff p)) *
      Multiset.prod (Multiset.pmap (fun a x => X - ↑C a) (roots (Polynomial.map (algebraMap K L) p)) hF) =
    Polynomial.map (algebraMap { x // x ∈ F } L)
      (↑C (↑(algebraMap K { x // x ∈ F }) (leadingCoeff p)) *
        Multiset.prod
          (Multiset.map (fun a => X - ↑C a) (Multiset.pmap Subtype.mk (roots (Polynomial.map (algebraMap K L) p)) hF)))
[PROOFSTEP]
simp_rw [Polynomial.map_mul, Polynomial.map_multiset_prod, Multiset.map_pmap, Polynomial.map_sub, map_C, map_X]
[GOAL]
F✝ : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : ∀ (x : L), x ∈ roots (Polynomial.map (algebraMap K L) p) → x ∈ F
⊢ ↑C (↑(algebraMap K L) (leadingCoeff p)) *
      Multiset.prod (Multiset.pmap (fun a x => X - ↑C a) (roots (Polynomial.map (algebraMap K L) p)) hF) =
    ↑C (↑(algebraMap { x // x ∈ F } L) (↑(algebraMap K { x // x ∈ F }) (leadingCoeff p))) *
      Multiset.prod
        (Multiset.pmap (fun a h => X - ↑C (↑(algebraMap { x // x ∈ F } L) { val := a, property := h }))
          (roots (Polynomial.map (algebraMap K L) p)) hF)
[PROOFSTEP]
rfl
