awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f : K[X]
rw :
  (map (AdjoinRoot.of f.factor) f /ₘ
        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])).natDegree =
    f.natDegree - 1
⊢ f.removeFactor.natDegree = f.natDegree - 1
have rw₁ : (map (AdjoinRoot.of f.factor) f).natDegree -
    (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])).natDegree =
  f.natDegree - 1
Tactic: rw [removeFactor, natDegree_divByMonic _ (monic_X_sub_C _), natDegree_map, natDegree_X_sub_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f : K[X]
rw :
  (map (AdjoinRoot.of f.factor) f /ₘ
        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])).natDegree =
    f.natDegree - 1
rw₁ :
  (map (AdjoinRoot.of f.factor) f).natDegree -
      (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])).natDegree =
    f.natDegree - 1
⊢ f.removeFactor.natDegree = f.natDegree - 1
have rw₂ : f.natDegree -
    (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])).natDegree =
  f.natDegree - 1
Tactic: rw [removeFactor, natDegree_divByMonic _ (monic_X_sub_C _), natDegree_map, natDegree_X_sub_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f : K[X]
rw :
  (map (AdjoinRoot.of f.factor) f /ₘ
        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])).natDegree =
    f.natDegree - 1
rw₁ :
  (map (AdjoinRoot.of f.factor) f).natDegree -
      (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])).natDegree =
    f.natDegree - 1
rw₂ :
  f.natDegree -
      (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])).natDegree =
    f.natDegree - 1
⊢ f.removeFactor.natDegree = f.natDegree - 1
have rw₃ : f.natDegree - 1 = f.natDegree - 1
Tactic: rw [removeFactor, natDegree_divByMonic _ (monic_X_sub_C _), natDegree_map, natDegree_X_sub_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f : K[X]
n : ℕ
hfn : f.natDegree = n + 1
⊢ f.removeFactor.natDegree = n
have rw : f.natDegree - 1 = n
Tactic: rw [natDegree_removeFactor, hfn, n.add_sub_cancel]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f : K[X]
n : ℕ
hfn : f.natDegree = n + 1
rw : f.natDegree - 1 = n
⊢ f.removeFactor.natDegree = n
have rw₁ : n + 1 - 1 = n
Tactic: rw [natDegree_removeFactor, hfn, n.add_sub_cancel]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (goal)
Goal:
K : Type v
inst : Field K
f : K[X]
n : ℕ
hfn : f.natDegree = n + 1
rw : f.natDegree - 1 = n
rw₁ : n + 1 - 1 = n
⊢ f.removeFactor.natDegree = n
have rw₂ : n = n
Tactic: rw [natDegree_removeFactor, hfn, n.add_sub_cancel]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (hypothesis)
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),
        Splits (R := SplittingFieldAux n f) (map (algebraMap K (SplittingFieldAux n f)) f))
    n
K : Type u
x : Field K
f : K[X]
hf : f.natDegree = n.succ
h : f.natDegree = 0
⊢ False
have hf₁ : 0 = n.succ
Tactic: rw [h] at hf
Cleared hypotheses: hf, h
-- 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),
        Splits (R := SplittingFieldAux n f) (map (algebraMap K (SplittingFieldAux n f)) f))
    n
K : Type u
x : Field K
f : K[X]
hf : f.natDegree = n.succ
⊢ Splits (R := SplittingFieldAux n.succ f) (map (algebraMap K (SplittingFieldAux n.succ f)) f)
have rw : Splits (R := SplittingFieldAux n.succ f)
  (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]) *
      f.removeFactor))
Tactic: rw [algebraMap_succ, ← map_map,
      ← X_sub_C_mul_removeFactor f fun h => by rw [h] at hf; cases hf]
-- 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),
        Splits (R := SplittingFieldAux n f) (map (algebraMap K (SplittingFieldAux n f)) f))
    n
K : Type u
x : Field K
f : K[X]
hf : f.natDegree = n.succ
⊢ Splits (R := SplittingFieldAux n.succ f)
    (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]) *
        f.removeFactor))
have rw : (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)).Splits
Tactic: rw [Polynomial.map_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (hypothesis)
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
h : f.natDegree = 0
⊢ False
have hfn₁ : 0 = n.succ
Tactic: rw [h] at hfn
Cleared hypotheses: hfn, h
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (hypothesis)
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
⊢ Eq (α := Subalgebra K (SplittingFieldAux n.succ f)) (Algebra.adjoin K (f.rootSet (SplittingFieldAux n.succ f))) ⊤
have hndf : f.natDegree ≠ 0
Tactic: have hndf : f.natDegree ≠ 0 := by intro h; rw [h] at hfn; cases hfn
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (hypothesis)
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
h : f = 0
⊢ False
have hndf₁ : natDegree.{u} (R := K) 0 ≠ 0
Tactic: rw [h] at hndf
Cleared hypotheses: hndf, h
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (hypothesis)
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
⊢ Eq (α := Subalgebra K (SplittingFieldAux n.succ f)) (Algebra.adjoin K (f.rootSet (SplittingFieldAux n.succ f))) ⊤
have hfn0 : f ≠ 0
Tactic: have hfn0 : f ≠ 0 := by intro h; rw [h] at hndf; exact hndf rfl
-- Lean 4 proof step from Mathlib.FieldTheory.SplittingField.Construction (hypothesis)
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
⊢ Eq (α := Subalgebra K (SplittingFieldAux n.succ f)) (Algebra.adjoin K (f.rootSet (SplittingFieldAux n.succ f))) ⊤
have hmf0 : Ne (α := (SplittingFieldAux n.succ f)[X]) (map (algebraMap K (SplittingFieldAux n.succ f)) f) 0
Tactic: have hmf0 : map (algebraMap K (SplittingFieldAux n.succ f)) f ≠ 0 := map_ne_zero hfn0
-- 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
⊢ 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)))
    ⊤
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
      (↑(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)))
    ⊤
Tactic: rw [algebraMap_succ, ← map_map, ← X_sub_C_mul_removeFactor _ hndf, Polynomial.map_mul] at hmf0 ⊢
Cleared hypotheses: hmf0
-- 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 :
  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)))
    ⊤
have rw : 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: 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]
-- 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 :
  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))))
    ⊤
have simp : 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))))
  ⊤
Tactic: simp only [SplittingFieldAux.succ]
-- 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 :
  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))))
    ⊤
have rw : Eq (α := Subalgebra K (SplittingFieldAux n f.removeFactor))
  (Subalgebra.restrictScalars K (S := AdjoinRoot f.factor)
    (Algebra.adjoin (AdjoinRoot f.factor)
      (↑(Multiset.toFinset
            (roots (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor))) :
        Set (SplittingFieldAux n f.removeFactor))))
  ⊤
Tactic: 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]
-- 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 :
  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
rw :
  Eq (α := Subalgebra K (SplittingFieldAux n f.removeFactor))
    (Subalgebra.restrictScalars K (S := AdjoinRoot f.factor)
      (Algebra.adjoin (AdjoinRoot 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 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))))
    ⊤
have rw₁ : Eq (α := Subalgebra K (SplittingFieldAux n f.removeFactor))
  (Subalgebra.restrictScalars K (S := AdjoinRoot f.factor)
    (Algebra.adjoin (AdjoinRoot f.factor) (f.removeFactor.rootSet (SplittingFieldAux n f.removeFactor))))
  ⊤
Tactic: 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]
-- 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 :
  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
rw :
  Eq (α := Subalgebra K (SplittingFieldAux n f.removeFactor))
    (Subalgebra.restrictScalars K (S := AdjoinRoot f.factor)
      (Algebra.adjoin (AdjoinRoot f.factor)
        (↑(Multiset.toFinset
              (roots (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor))) :
          Set (SplittingFieldAux n f.removeFactor))))
    ⊤
rw₁ :
  Eq (α := Subalgebra K (SplittingFieldAux n f.removeFactor))
    (Subalgebra.restrictScalars K (S := AdjoinRoot f.factor)
      (Algebra.adjoin (AdjoinRoot f.factor) (f.removeFactor.rootSet (SplittingFieldAux n f.removeFactor))))
    ⊤
⊢ 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))))
    ⊤
have rw₂ : Eq (α := Subalgebra K (SplittingFieldAux n f.removeFactor)) (Subalgebra.restrictScalars K (S := AdjoinRoot f.factor) ⊤)
  ⊤
Tactic: 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]