no goals
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 ↑(Multiset.toFinset (roots (Polynomial.map (algebraMap F L) (f * g)))) = ⊤
rw [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, adjoin_roots,
  Algebra.map_top, IsScalarTower.adjoin_range_toAlgHom, ← map_map, adjoin_roots,
  Subalgebra.restrictScalars_top]