-- Mathlib/FieldTheory/SplittingField/Construction.lean
theorem adjoin_rootSet (n : ℕ) :
    ∀ {K : Type u} [Field K],
      ∀ (f : K[X]) (_hfn : f.natDegree = n),
        Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤ :=
  Nat.recOn (motive := fun n =>
    ∀ {K : Type u} [Field K],
      ∀ (f : K[X]) (_hfn : f.natDegree = n),
        Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤)
    n (fun {_} _ _ _hf => Algebra.eq_top_iff.2 fun x => Subalgebra.range_le _ ⟨x, rfl⟩)
    fun n ih {K} _ f hfn => by
    have hndf : f.natDegree ≠ 0

Proof state:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        f.natDegree = n → 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 : map (algebraMap K (SplittingFieldAux n.succ f)) f ≠ 0
⊢ Algebra.adjoin K ↑(map (algebraMap K (SplittingFieldAux n.succ f)) f).roots.toFinset = ⊤

Tactic:
rw [algebraMap_succ, ← map_map, ← X_sub_C_mul_removeFactor _ hndf, Polynomial.map_mul] at hmf0 ⊢

Result:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        f.natDegree = n → 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 :
  map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (X - C (AdjoinRoot.root f.factor)) *
      map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor ≠
    0
⊢ Algebra.adjoin K
      ↑(map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (X - C (AdjoinRoot.root f.factor)) *
              map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
                f.removeFactor).roots.toFinset =
    ⊤

Proof state:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : f.natDegree = n.succ
⊢ Algebra.adjoin K (f.rootSet (SplittingFieldAux n.succ f)) = ⊤

Tactic:
have hndf : f.natDegree ≠ 0 := by intro h; rw [h] at hfn; cases hfn

Result:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        f.natDegree = n → 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
⊢ Algebra.adjoin K (f.rootSet (SplittingFieldAux n.succ f)) = ⊤

Proof state:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : 0 = n.succ
h : f.natDegree = 0
⊢ False

Tactic:
cases hfn

Result:
no goals

Proof state:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : f.natDegree = n.succ
h : f.natDegree = 0
⊢ False

Tactic:
rw [h] at hfn

Result:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]),
        f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤)
    n
K : Type u
x✝ : Field K
f : K[X]
hfn : 0 = n.succ
h : f.natDegree = 0
⊢ False