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
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
simp_rw [rootSet, Finset.mem_coe, Multiset.mem_toFinset] at hF
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)
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
rw [splits_iff_exists_multiset]
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)))
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)
refine' ⟨Multiset.pmap Subtype.mk _ hF, map_injective _ (algebraMap F L).injective _⟩
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)))
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)))
conv_lhs =>
  rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq, eq_prod_roots_of_splits h, ←
    Multiset.pmap_eq_map _ _ _ hF]
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)
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)))
simp_rw [Polynomial.map_mul, Polynomial.map_multiset_prod, Multiset.map_pmap, Polynomial.map_sub,
  map_C, map_X]
no goals
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)
rfl