-- Mathlib/Algebra/Polynomial/Splits.lean
theorem splits_of_comp (j : L →+* F) {f : K[X]} (h : Splits (j.comp i) f)
    (roots_mem_range : ∀ a ∈ (f.map (j.comp i)).roots, a ∈ j.range) : Splits i f

Proof state:
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
j : L →+* F
f : K[X]
h : Splits (j.comp i) f
lift : (a : F) → a ∈ (map (j.comp i) f).roots → L
lift_eq : ∀ (a : F) (a_1 : a ∈ (map (j.comp i) f).roots), j (lift a a_1) = a
⊢ map j (map i f) =
    map j
      (C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) (Multiset.pmap lift (map (j.comp i) f).roots ⋯)).prod)

Tactic:
conv_lhs => rw [Polynomial.map_map, eq_prod_roots_of_splits h]

Result:
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
j : L →+* F
f : K[X]
h : Splits (j.comp i) f
lift : (a : F) → a ∈ (map (j.comp i) f).roots → L
lift_eq : ∀ (a : F) (a_1 : a ∈ (map (j.comp i) f).roots), j (lift a a_1) = a
⊢ C ((j.comp i) f.leadingCoeff) * (Multiset.map (fun a => X - C a) (map (j.comp i) f).roots).prod =
    map j
      (C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) (Multiset.pmap lift (map (j.comp i) f).roots ⋯)).prod)

Proof state:
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
j : L →+* F
f : K[X]
h : Splits (j.comp i) f
lift : (a : F) → a ∈ (map (j.comp i) f).roots → L
lift_eq : ∀ (a : F) (a_1 : a ∈ (map (j.comp i) f).roots), j (lift a a_1) = a
⊢ C ((j.comp i) f.leadingCoeff) * (Multiset.map (fun a => X - C a) (map (j.comp i) f).roots).prod =
    C (j (i f.leadingCoeff)) * (Multiset.map (fun a => X - C a) (map (j.comp i) f).roots).prod

Tactic:
rfl

Result:
no goals

Proof state:
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
j : L →+* F
f : K[X]
h : Splits (j.comp i) f
lift : (a : F) → a ∈ (map (j.comp i) f).roots → L
lift_eq : ∀ (a : F) (a_1 : a ∈ (map (j.comp i) f).roots), j (lift a a_1) = a
⊢ Splits i f

Tactic:
rw [splits_iff_exists_multiset]

Result:
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
j : L →+* F
f : K[X]
h : Splits (j.comp i) f
lift : (a : F) → a ∈ (map (j.comp i) f).roots → L
lift_eq : ∀ (a : F) (a_1 : a ∈ (map (j.comp i) f).roots), j (lift a a_1) = a
⊢ ∃ s, map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod

Proof state:
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
j : L →+* F
f : K[X]
h : Splits (j.comp i) f
lift : (a : F) → a ∈ (map (j.comp i) f).roots → L
lift_eq : ∀ (a : F) (a_1 : a ∈ (map (j.comp i) f).roots), j (lift a a_1) = a
⊢ C ((j.comp i) f.leadingCoeff) * (Multiset.map (fun a => X - C a) (map (j.comp i) f).roots).prod =
    map j
      (C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) (Multiset.pmap lift (map (j.comp i) f).roots ⋯)).prod)

Tactic:
simp_rw [Polynomial.map_mul, Polynomial.map_multiset_prod, Multiset.map_pmap, Polynomial.map_sub,
  map_C, map_X, lift_eq, Multiset.pmap_eq_map]

Result:
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
j : L →+* F
f : K[X]
h : Splits (j.comp i) f
lift : (a : F) → a ∈ (map (j.comp i) f).roots → L
lift_eq : ∀ (a : F) (a_1 : a ∈ (map (j.comp i) f).roots), j (lift a a_1) = a
⊢ C ((j.comp i) f.leadingCoeff) * (Multiset.map (fun a => X - C a) (map (j.comp i) f).roots).prod =
    C (j (i f.leadingCoeff)) * (Multiset.map (fun a => X - C a) (map (j.comp i) f).roots).prod

Proof state:
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
j : L →+* F
f : K[X]
h : Splits (j.comp i) f
roots_mem_range : ∀ a ∈ (map (j.comp i) f).roots, a ∈ j.range
⊢ Splits i f

Tactic:
choose lift lift_eq using roots_mem_range

Result:
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
j : L →+* F
f : K[X]
h : Splits (j.comp i) f
lift : (a : F) → a ∈ (map (j.comp i) f).roots → L
lift_eq : ∀ (a : F) (a_1 : a ∈ (map (j.comp i) f).roots), j (lift a a_1) = a
⊢ Splits i f

Proof state:
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
j : L →+* F
f : K[X]
h : Splits (j.comp i) f
lift : (a : F) → a ∈ (map (j.comp i) f).roots → L
lift_eq : ∀ (a : F) (a_1 : a ∈ (map (j.comp i) f).roots), j (lift a a_1) = a
⊢ ∃ s, map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod

Tactic:
refine ⟨(f.map (j.comp i)).roots.pmap lift fun _ ↦ id, map_injective _ j.injective ?_⟩

Result:
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
j : L →+* F
f : K[X]
h : Splits (j.comp i) f
lift : (a : F) → a ∈ (map (j.comp i) f).roots → L
lift_eq : ∀ (a : F) (a_1 : a ∈ (map (j.comp i) f).roots), j (lift a a_1) = a
⊢ map j (map i f) =
    map j
      (C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) (Multiset.pmap lift (map (j.comp i) f).roots ⋯)).prod)