-- 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
⊢ Algebra.adjoin K (f.rootSet (SplittingFieldAux n.succ f)) = ⊤

Tactic:
have hfn0 : f ≠ 0 := by intro h; rw [h] at hndf; exact hndf rfl

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
⊢ 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 : 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
this :
  Subalgebra.restrictScalars K
      (Algebra.adjoin (↥(IsScalarTower.toAlgHom K (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)).range)
        (f.removeFactor.rootSet (SplittingFieldAux n f.removeFactor))) =
    Subalgebra.restrictScalars K
      (Algebra.adjoin (AdjoinRoot f.factor) (f.removeFactor.rootSet (SplittingFieldAux n f.removeFactor)))
⊢ Subalgebra.restrictScalars K
      (Algebra.adjoin (AdjoinRoot f.factor) (f.removeFactor.rootSet (SplittingFieldAux n f.removeFactor))) =
    ⊤

Tactic:
rw [ih _ (natDegree_removeFactor' hfn), Subalgebra.restrictScalars_top]

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
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
this :
  Subalgebra.restrictScalars K
      (Algebra.adjoin (↥(IsScalarTower.toAlgHom K (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)).range)
        (f.removeFactor.rootSet (SplittingFieldAux n f.removeFactor))) =
    Subalgebra.restrictScalars K
      (Algebra.adjoin (AdjoinRoot f.factor) (f.removeFactor.rootSet (SplittingFieldAux n f.removeFactor)))
⊢ Subalgebra.restrictScalars K
      (Algebra.adjoin ↥(IsScalarTower.toAlgHom K (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)).range
        ↑(map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor).roots.toFinset) =
    ⊤

Tactic:
refine this.trans ?_

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
this :
  Subalgebra.restrictScalars K
      (Algebra.adjoin (↥(IsScalarTower.toAlgHom K (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)).range)
        (f.removeFactor.rootSet (SplittingFieldAux n f.removeFactor))) =
    Subalgebra.restrictScalars K
      (Algebra.adjoin (AdjoinRoot f.factor) (f.removeFactor.rootSet (SplittingFieldAux n f.removeFactor)))
⊢ Subalgebra.restrictScalars K
      (Algebra.adjoin (AdjoinRoot f.factor) (f.removeFactor.rootSet (SplittingFieldAux n f.removeFactor))) =
    ⊤

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 (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 ⊢
erw [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,
  Algebra.adjoin_union_eq_adjoin_adjoin, ← Set.image_singleton,
  Algebra.adjoin_algebraMap K (SplittingFieldAux n f.removeFactor),
  AdjoinRoot.adjoinRoot_eq_top, Algebra.map_top]
have := IsScalarTower.adjoin_range_toAlgHom K (AdjoinRoot f.factor)
    (SplittingFieldAux n f.removeFactor)
    (f.removeFactor.rootSet (SplittingFieldAux n f.removeFactor))
refine this.trans ?_
rw [ih _ (natDegree_removeFactor' hfn), Subalgebra.restrictScalars_top]

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
hndf : f.natDegree ≠ 0
hfn0 : f ≠ 0
⊢ Algebra.adjoin K (f.rootSet (SplittingFieldAux n.succ f)) = ⊤

Tactic:
have hmf0 : map (algebraMap K (SplittingFieldAux n.succ f)) f ≠ 0 := map_ne_zero hfn0

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 K (SplittingFieldAux n.succ f)) f ≠ 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 : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
⊢ f ≠ 0

Tactic:
intro h

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
h : f = 0
⊢ False