-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
n_1 : ℕ
K_1 : Type u
inst : Field K_1
n : ℕ
ih :
  (fun (n : ℕ) ↦
      ∀ {K : Type u} [inst : Field K] (f : K[X]) (_hfn : f.natDegree = n),
        Eq (α := Subalgebra K (SplittingFieldAux n f)) (Algebra.adjoin K (f.rootSet (SplittingFieldAux n f))) ⊤)
    n
K : Type u
x : Field K
f : K[X]
hfn : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
hfn0 : f ≠ 0
hmf0 : Ne (α := (SplittingFieldAux n.succ f)[X]) (map (algebraMap K (SplittingFieldAux n.succ f)) f) 0
rw :
  Eq (α := Subalgebra K (SplittingFieldAux n.succ f))
    (Algebra.adjoin K (↑(Multiset.toFinset (f.aroots (SplittingFieldAux n.succ f))) : Set (SplittingFieldAux n.succ f)))
    ⊤
rw₁ rw₂ rw₃ :
  Eq (α := Subalgebra K (SplittingFieldAux n.succ f))
    (Algebra.adjoin K
      (↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n.succ f)) f))) :
        Set (SplittingFieldAux n.succ f)))
    ⊤
rw₄ :
  ∀
    (hmf0 :
      HMul.hMul (α := (SplittingFieldAux n.succ f)[X])
          (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
            (HSub.hSub (α := (AdjoinRoot f.factor)[X]) (β := (AdjoinRoot f.factor)[X]) X
              ((C : (a : AdjoinRoot f.factor) → (AdjoinRoot f.factor)[X]) (AdjoinRoot.root f.factor) :
                (AdjoinRoot f.factor)[X])))
          (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor) ≠
        0),
    Eq (α := Subalgebra K (SplittingFieldAux n.succ f))
      (Algebra.adjoin K
        (↑(HMul.hMul (α := (SplittingFieldAux n.succ f)[X])
                  (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
                    (HSub.hSub (α := (AdjoinRoot f.factor)[X]) (β := (AdjoinRoot f.factor)[X]) X
                      ((C : (a : AdjoinRoot f.factor) → (AdjoinRoot f.factor)[X]) (AdjoinRoot.root f.factor) :
                        (AdjoinRoot f.factor)[X])))
                  (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
                    f.removeFactor)).roots.toFinset :
          Set (SplittingFieldAux n.succ f)))
      ⊤
rw₅ :
  ∀
    (hmf0 :
      HMul.hMul (α := (SplittingFieldAux n.succ f)[X])
          (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
            (HSub.hSub (α := (AdjoinRoot f.factor)[X]) (β := (AdjoinRoot f.factor)[X]) X
              ((C : (a : AdjoinRoot f.factor) → (AdjoinRoot f.factor)[X]) (AdjoinRoot.root f.factor) :
                (AdjoinRoot f.factor)[X])))
          (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor) ≠
        0),
    Eq (α := Subalgebra K (SplittingFieldAux n.succ f))
      (Algebra.adjoin K
        (Set.image (α := AdjoinRoot f.factor)
            (⇑(algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) :
              (a : AdjoinRoot f.factor) → SplittingFieldAux n.succ f)
            {AdjoinRoot.root f.factor} ∪
          (↑(Multiset.toFinset
                (roots (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor))) :
            Set (SplittingFieldAux n.succ f))))
      ⊤
rw₆ :
  ∀
    (hmf0 :
      HMul.hMul (α := (SplittingFieldAux n.succ f)[X])
          (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
            (HSub.hSub (α := (AdjoinRoot f.factor)[X]) (β := (AdjoinRoot f.factor)[X]) X
              ((C : (a : AdjoinRoot f.factor) → (AdjoinRoot f.factor)[X]) (AdjoinRoot.root f.factor) :
                (AdjoinRoot f.factor)[X])))
          (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor) ≠
        0),
    Eq (α := Subalgebra K (SplittingFieldAux n f.removeFactor))
      (Algebra.adjoin K
        ((fun (a : AdjoinRoot f.factor) ↦
              (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor) :
                  (a : AdjoinRoot f.factor) → SplittingFieldAux n f.removeFactor)
                a) ''
            {AdjoinRoot.root f.factor} ∪
          (↑(Multiset.toFinset
                (roots (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor))) :
            Set (SplittingFieldAux n f.removeFactor))))
      ⊤
⊢ Eq (α := Subalgebra K (SplittingFieldAux n.succ f)) (Algebra.adjoin K (f.rootSet (SplittingFieldAux n.succ f))) ⊤

Tactic:
classical
    rw [rootSet_def, aroots_def]
    rw [algebraMap_succ, ← map_map, ← X_sub_C_mul_removeFactor _ hndf, Polynomial.map_mul] at hmf0 ⊢
    rw [roots_mul hmf0, Polynomial.map_sub, map_X, map_C, roots_X_sub_C, Multiset.toFinset_add,
      Finset.coe_union, Multiset.toFinset_singleton, Finset.coe_singleton, ← Set.image_singleton]
    simp only [SplittingFieldAux.succ]
    rw [← Algebra.adjoin_eq_adjoin_union K {AdjoinRoot.root f.factor}
      ((map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
        f.removeFactor).roots.toFinset : Set (SplittingFieldAux n f.removeFactor))
      AdjoinRoot.adjoinRoot_eq_top, ← rootSet_def, ih _ (natDegree_removeFactor' hfn),
      Subalgebra.restrictScalars_top]

Premises used: Polynomial.map_mul, Finset.coe_singleton, Polynomial.SplittingFieldAux.succ, Polynomial.SplittingFieldAux.algebraMap_succ, Set.image_singleton, Multiset.toFinset_add, Polynomial.map_X, Polynomial.roots_X_sub_C, Polynomial.rootSet_def, Polynomial.natDegree_removeFactor', Polynomial.roots_mul, Polynomial.map_sub, Polynomial.X_sub_C_mul_removeFactor, Polynomial.map_C, Polynomial.map_map, Subalgebra.restrictScalars_top, Polynomial.aroots_def, Multiset.toFinset_singleton, Finset.coe_union