-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.IsSplittingField (goal)
Goal:
F : Type u
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
inst_4 : Algebra F K
inst_5 : Algebra F L
inst_6 : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst_7 : IsSplittingField F K f
inst_8 : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
adjoin_rootSet' : Eq (α := Subalgebra F L) (Algebra.adjoin F (↑((f * g).aroots L).toFinset : Set L)) ⊤
adjoin_rootSet'₁ : Eq (α := Subalgebra F L) (Algebra.adjoin F (↑(f.aroots L + g.aroots L).toFinset : Set L)) ⊤
adjoin_rootSet'₂ :
  Eq (α := Subalgebra F L) (Algebra.adjoin F (↑((f.aroots L).toFinset ∪ (g.aroots L).toFinset) : Set L)) ⊤
adjoin_rootSet'₃ :
  Eq (α := Subalgebra F L) (Algebra.adjoin F ((↑(f.aroots L).toFinset : Set L) ∪ (↑(g.aroots L).toFinset : Set L))) ⊤
adjoin_rootSet'₄ :
  Eq (α := Subalgebra F L)
    (Subalgebra.restrictScalars F (S := ↥(Algebra.adjoin F (↑(f.aroots L).toFinset : Set L)))
      (Algebra.adjoin ↥(Algebra.adjoin F (↑(f.aroots L).toFinset : Set L)) (↑(g.aroots L).toFinset : Set L)))
    ⊤
adjoin_rootSet'₅ :
  Eq (α := Subalgebra F L)
    (Subalgebra.restrictScalars F (S :=
      ↥(Algebra.adjoin F (↑(roots (Polynomial.map (algebraMap F L) f)).toFinset : Set L)))
      (Algebra.adjoin ↥(Algebra.adjoin F (↑(roots (Polynomial.map (algebraMap F L) f)).toFinset : Set L))
        (↑(g.aroots L).toFinset : Set L)))
    ⊤
adjoin_rootSet'₆ :
  Eq (α := Subalgebra F L)
    (Subalgebra.restrictScalars F (S :=
      ↥(Algebra.adjoin F (↑(roots (Polynomial.map (algebraMap F L) f)).toFinset : Set L)))
      (Algebra.adjoin ↥(Algebra.adjoin F (↑(roots (Polynomial.map (algebraMap F L) f)).toFinset : Set L))
        (↑(roots (Polynomial.map (algebraMap F L) g)).toFinset : Set L)))
    ⊤
adjoin_rootSet'₇ :
  Eq (α := Subalgebra F L)
    (Subalgebra.restrictScalars F (S :=
      ↥(Algebra.adjoin F
          (↑(roots
                  (Polynomial.map
                    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap F K))
                    f)).toFinset :
            Set L)))
      (Algebra.adjoin
        ↥(Algebra.adjoin F
            (↑(roots
                    (Polynomial.map
                      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap F K))
                      f)).toFinset :
              Set L))
        (↑(roots
                (Polynomial.map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap F K))
                  g)).toFinset :
          Set L)))
    ⊤
adjoin_rootSet'₈ :
  Eq (α := Subalgebra F L)
    (Subalgebra.restrictScalars F (S :=
      ↥(Algebra.adjoin F
          (↑(roots (Polynomial.map (algebraMap K L) (Polynomial.map (algebraMap F K) f))).toFinset : Set L)))
      (Algebra.adjoin
        ↥(Algebra.adjoin F
            (↑(roots (Polynomial.map (algebraMap K L) (Polynomial.map (algebraMap F K) f))).toFinset : Set L))
        (↑(roots
                (Polynomial.map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap F K))
                  g)).toFinset :
          Set L)))
    ⊤
adjoin_rootSet'₉ :
  Eq (α := Subalgebra F L)
    (Subalgebra.restrictScalars F (S :=
      ↥(Algebra.adjoin F
          (↑(Multiset.toFinset
                (Multiset.map (⇑(algebraMap K L) : (a : K) → L) (roots (Polynomial.map (algebraMap F K) f)))) :
            Set L)))
      (Algebra.adjoin
        ↥(Algebra.adjoin F
            (↑(Multiset.toFinset
                  (Multiset.map (⇑(algebraMap K L) : (a : K) → L) (roots (Polynomial.map (algebraMap F K) f)))) :
              Set L))
        (↑(roots
                (Polynomial.map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap F K))
                  g)).toFinset :
          Set L)))
    ⊤
adjoin_rootSet'₁₀ :
  Eq (α := Subalgebra F L)
    (Subalgebra.restrictScalars F (S :=
      ↥(Algebra.adjoin F
          (↑(Finset.image (⇑(algebraMap K L) : (a : K) → L) (roots (Polynomial.map (algebraMap F K) f)).toFinset) :
            Set L)))
      (Algebra.adjoin
        ↥(Algebra.adjoin F
            (↑(Finset.image (⇑(algebraMap K L) : (a : K) → L) (roots (Polynomial.map (algebraMap F K) f)).toFinset) :
              Set L))
        (↑(roots
                (Polynomial.map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap F K))
                  g)).toFinset :
          Set L)))
    ⊤
adjoin_rootSet'₁₁ :
  Eq (α := Subalgebra F L)
    (Subalgebra.restrictScalars F (S :=
      ↥(Algebra.adjoin F
          ((⇑(algebraMap K L) : (a : K) → L) '' (↑(roots (Polynomial.map (algebraMap F K) f)).toFinset : Set K))))
      (Algebra.adjoin
        ↥(Algebra.adjoin F
            ((⇑(algebraMap K L) : (a : K) → L) '' (↑(roots (Polynomial.map (algebraMap F K) f)).toFinset : Set K)))
        (↑(roots
                (Polynomial.map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap F K))
                  g)).toFinset :
          Set L)))
    ⊤
adjoin_rootSet'₁₂ :
  Eq (α := Subalgebra F L)
    (Subalgebra.restrictScalars F (S :=
      ↥(Subalgebra.map (IsScalarTower.toAlgHom F K L)
          (Algebra.adjoin F (↑(roots (Polynomial.map (algebraMap F K) f)).toFinset : Set K))))
      (Algebra.adjoin
        ↥(Subalgebra.map (IsScalarTower.toAlgHom F K L)
            (Algebra.adjoin F (↑(roots (Polynomial.map (algebraMap F K) f)).toFinset : Set K)))
        (↑(roots
                (Polynomial.map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap F K))
                  g)).toFinset :
          Set L)))
    ⊤
adjoin_rootSet'₁₃ :
  Eq (α := Subalgebra F L)
    (Subalgebra.restrictScalars F (S :=
      ↥(Subalgebra.map (IsScalarTower.toAlgHom F K L) (Algebra.adjoin F (f.rootSet K))))
      (Algebra.adjoin ↥(Subalgebra.map (IsScalarTower.toAlgHom F K L) (Algebra.adjoin F (f.rootSet K)))
        (↑(roots
                (Polynomial.map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap F K))
                  g)).toFinset :
          Set L)))
    ⊤
adjoin_rootSet'₁₄ :
  Eq (α := Subalgebra F L)
    (Subalgebra.restrictScalars F (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom F K L) ⊤))
      (Algebra.adjoin ↥(Subalgebra.map (IsScalarTower.toAlgHom F K L) ⊤)
        (↑(roots
                (Polynomial.map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap F K))
                  g)).toFinset :
          Set L)))
    ⊤
adjoin_rootSet'₁₅ :
  Eq (α := Subalgebra F L)
    (Subalgebra.restrictScalars F (S := ↥(AlgHom.range (IsScalarTower.toAlgHom F K L)))
      (Algebra.adjoin ↥(AlgHom.range (IsScalarTower.toAlgHom F K L))
        (↑(roots
                (Polynomial.map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap F K))
                  g)).toFinset :
          Set L)))
    ⊤
adjoin_rootSet'₁₆ :
  Eq (α := Subalgebra F L)
    (Subalgebra.restrictScalars F
      (Algebra.adjoin K
        (↑(roots
                (Polynomial.map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap F K))
                  g)).toFinset :
          Set L)))
    ⊤
⊢ Eq (α := Subalgebra F L) (Algebra.adjoin F ((f * g).rootSet L)) ⊤
have adjoin_rootSet'₁₇ : Eq (α := Subalgebra F L)
  (Subalgebra.restrictScalars F
    (Algebra.adjoin K
      (↑(roots (Polynomial.map (algebraMap K L) (Polynomial.map (algebraMap F K) g))).toFinset : Set L)))
  ⊤
Tactic: classical
    rw [rootSet, aroots_mul (mul_ne_zero hf hg),
      Multiset.toFinset_add, Finset.coe_union, Algebra.adjoin_union_eq_adjoin_adjoin,
      aroots_def, aroots_def, IsScalarTower.algebraMap_eq F K L, ← map_map, (splits K f).roots_map,
      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]