-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
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)))
      ⊤
⊢ Eq (α := Subalgebra K (SplittingFieldAux n.succ f)) (Algebra.adjoin K (f.rootSet (SplittingFieldAux n.succ f))) ⊤
have 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))))
    ⊤
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]
Cleared hypotheses: hmf0