awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f g : K[X]
h : f = 0 ∧ g = 0
refine_1 :
  Eq.{v + 1} (α := K) ((aeval 0 : (a : K[X]) → K) 0 : K) (0 : K) ∧
    Eq (α := K) ((aeval 0 : (a : K[X]) → K) g : K) (0 : K)
refine_1₁ :
  Eq.{v + 1} (α := K) ((aeval 0 : (a : K[X]) → K) 0 : K) (0 : K) ∧
    Eq.{v + 1} (α := K) ((aeval 0 : (a : K[X]) → K) 0 : K) (0 : K)
refine_1₂ : Eq.{v + 1} (α := K) 0 0 ∧ Eq.{v + 1} (α := K) 0 0
refine_1₃ refine_1₄ : Eq.{v + 1} (α := K) 0 0
⊢ Eq (α := K) ((aeval 0 : (a : K[X]) → K) f : K) (0 : K) ∧ Eq (α := K) ((aeval 0 : (a : K[X]) → K) g : K) (0 : K)

Tactic:
rw [h.left, h.right, map_zero, and_self]

Premises used: and_self, map_zero, And.right, And.left
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
x : K[X]
hx : Membership.mem (γ := Set K[X]) (nonunits K[X]) x
h_1 : x ≠ 0
w w_1 : K[X]
h :
  ∀ {A : Type v} [inst_1 : CommRing A] [IsDomain A] [inst_3 : Algebra K A] (a : A),
    Ne (α := A) ((aeval a : (a : K[X]) → A) (x * w) : A) (0 : A) ∨
      Ne (α := A) ((aeval a : (a : K[X]) → A) (x * w_1) : A) (0 : A)
⊢ ¬(Eq (α := AdjoinRoot x.factor)
        ((aeval (AdjoinRoot.root x.factor) : (a : K[X]) → AdjoinRoot x.factor) (x * w) : AdjoinRoot x.factor)
        (0 : AdjoinRoot x.factor) ∧
      Eq (α := AdjoinRoot x.factor)
        ((aeval (AdjoinRoot.root x.factor) : (a : K[X]) → AdjoinRoot x.factor) (x * w_1) : AdjoinRoot x.factor)
        (0 : AdjoinRoot x.factor))

Tactic:
replace h := not_and_or.mpr <| h <| AdjoinRoot.root x.factor
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
x : K[X]
hx : Membership.mem (γ := Set K[X]) (nonunits K[X]) x
h_1 : x ≠ 0
w w_1 : K[X]
h :
  ¬(Eq (α := AdjoinRoot x.factor)
        ((aeval (AdjoinRoot.root x.factor) : (a : K[X]) → AdjoinRoot x.factor) (x * w) : AdjoinRoot x.factor)
        (0 : AdjoinRoot x.factor) ∧
      Eq (α := AdjoinRoot x.factor)
        ((aeval (AdjoinRoot.root x.factor) : (a : K[X]) → AdjoinRoot x.factor) (x * w_1) : AdjoinRoot x.factor)
        (0 : AdjoinRoot x.factor))
⊢ False

Tactic:
simp only [AdjoinRoot.aeval_eq, AdjoinRoot.mk_eq_zero,
      dvd_mul_of_dvd_left <| factor_dvd_of_not_isUnit hx, true_and, not_true] at h

Premises used: dvd_mul_of_dvd_left, AdjoinRoot.mk_eq_zero, Polynomial.factor_dvd_of_not_isUnit, not_true, AdjoinRoot.aeval_eq, true_and
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f : K[X]
hf : f.natDegree ≠ 0
let :
  ∀ (g : K[X]) (hg : f = f.factor * g),
    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 =
      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]) *
      f.removeFactor =
    map (AdjoinRoot.of f.factor) f

Tactic:
let ⟨g, hg⟩ := factor_dvd_of_natDegree_ne_zero hf
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f : K[X]
hf : f.natDegree ≠ 0
g : K[X]
hg : f = f.factor * g
apply : (map (AdjoinRoot.of f.factor) f).IsRoot (AdjoinRoot.root f.factor)
⊢ 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 =
    map (AdjoinRoot.of f.factor) f

Tactic:
apply (mul_divByMonic_eq_iff_isRoot
    (R := AdjoinRoot f.factor) (a := AdjoinRoot.root f.factor)).mpr

Premises used: Iff.mpr, Polynomial.mul_divByMonic_eq_iff_isRoot
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f : K[X]
hf : f.natDegree ≠ 0
g : K[X]
hg : f = f.factor * g
rw : eval (AdjoinRoot.root f.factor) (map (AdjoinRoot.of f.factor) f) = 0
rw₁ : eval₂ (AdjoinRoot.of f.factor) (AdjoinRoot.root f.factor) f = 0
rw₂ : eval₂ (AdjoinRoot.of (f.factor * g).factor) (AdjoinRoot.root (f.factor * g).factor) (f.factor * g) = 0
rw₃ :
  eval₂ (AdjoinRoot.of (f.factor * g).factor) (AdjoinRoot.root (f.factor * g).factor) f.factor *
      eval₂ (AdjoinRoot.of (f.factor * g).factor) (AdjoinRoot.root (f.factor * g).factor) g =
    0
rw₄ :
  eval₂ (AdjoinRoot.of f.factor) (AdjoinRoot.root f.factor) f.factor *
      eval₂ (AdjoinRoot.of f.factor) (AdjoinRoot.root f.factor) g =
    0
rw₅ : 0 * eval₂ (AdjoinRoot.of f.factor) (AdjoinRoot.root f.factor) g = 0
rw₆ rw₇ : Eq.{v + 1} (α := AdjoinRoot f.factor) 0 0
⊢ (map (AdjoinRoot.of f.factor) f).IsRoot (AdjoinRoot.root f.factor)

Tactic:
rw [IsRoot.def, eval_map, hg, eval₂_mul, ← hg, AdjoinRoot.eval₂_root, zero_mul]

Premises used: Polynomial.eval_map, MulZeroClass.zero_mul, Polynomial.IsRoot.def, Polynomial.eval₂_mul, AdjoinRoot.eval₂_root
-- Module: Mathlib.FieldTheory.SplittingField.Construction
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
rw₃ rw₄ : f.natDegree - 1 = f.natDegree - 1
⊢ f.removeFactor.natDegree = f.natDegree - 1

Tactic:
rw [removeFactor, natDegree_divByMonic _ (monic_X_sub_C _), natDegree_map, natDegree_X_sub_C]

Premises used: Polynomial.monic_X_sub_C, Polynomial.natDegree_divByMonic, Polynomial.natDegree_map, Polynomial.natDegree_X_sub_C, Polynomial.removeFactor
-- Module: Mathlib.FieldTheory.SplittingField.Construction
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
rw₂ rw₃ : n = n
⊢ f.removeFactor.natDegree = n

Tactic:
rw [natDegree_removeFactor, hfn, n.add_sub_cancel]

Premises used: Polynomial.natDegree_removeFactor, Nat.add_sub_cancel
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
n : ℕ
f : K[X]
⊢ SplittingFieldAux (n + 1) f = SplittingFieldAux n f.removeFactor

Tactic:
rfl

Premises used: AdjoinRoot, Polynomial.SplittingFieldAux, Quotient, rfl
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
F : Type u
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
inst_2 : Field F
n : ℕ
f : K[X]
⊢ IsScalarTower K (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)

Tactic:
IsScalarTower.of_algebraMap_eq fun _ => rfl

Premises used: IsScalarTower.of_algebraMap_eq, rfl
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
n : ℕ
f : K[X]
⊢ Eq (α := K →+* SplittingFieldAux (n + 1) f) (algebraMap K (SplittingFieldAux (n + 1) f))
    (RingHom.comp (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (AdjoinRoot.of f.factor))

Tactic:
rfl

Premises used: Polynomial.SplittingFieldAux, rfl
-- 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),
        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
⊢ 0 = n.succ

Tactic:
rw [h] at hf
-- 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),
        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
hf₁ : 0 = n.succ
⊢ f.natDegree = 0

Tactic:
rw [h] at hf
-- 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),
        Splits (R := SplittingFieldAux n f) (map (algebraMap K (SplittingFieldAux n f)) f))
    n
K : Type u
x : Field K
f : K[X]
hf : 0 = n.succ
h : f.natDegree = 0
⊢ False

Tactic:
cases hf
-- 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),
        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
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))
⊢ Splits (R := SplittingFieldAux n.succ f) (map (algebraMap K (SplittingFieldAux n.succ f)) f)

Tactic:
rw [algebraMap_succ, ← map_map,
      ← X_sub_C_mul_removeFactor f fun h => by rw [h] at hf; cases hf]

Premises used: Polynomial.SplittingFieldAux.algebraMap_succ, Polynomial.X_sub_C_mul_removeFactor, Polynomial.map_map
-- 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),
        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
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
⊢ 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 [Polynomial.map_mul]

Premises used: Polynomial.map_mul
-- 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),
        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
⊢ (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:
Splits.mul ((Splits.X_sub_C _).map _) (ih _ (natDegree_removeFactor' hf))

Premises used: Polynomial.natDegree_removeFactor', Polynomial.Splits.X_sub_C, Polynomial.Splits.map, Polynomial.Splits.mul
-- 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),
        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
⊢ (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:
exact Splits.mul ((Splits.X_sub_C _).map _) (ih _ (natDegree_removeFactor' hf))

Premises used: Polynomial.natDegree_removeFactor', Polynomial.Splits.X_sub_C, Polynomial.Splits.map, Polynomial.Splits.mul
-- 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
h : f.natDegree = 0
⊢ 0 = n.succ

Tactic:
rw [h] at hfn
-- 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
h : f.natDegree = 0
hfn₁ : 0 = n.succ
⊢ f.natDegree = 0

Tactic:
rw [h] at hfn
-- 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 : 0 = n.succ
h : f.natDegree = 0
⊢ False

Tactic:
cases hfn
-- 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
⊢ f.natDegree ≠ 0

Tactic:
have hndf : f.natDegree ≠ 0 := by intro h; rw [h] at hfn; cases hfn
-- 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
h : f = 0
⊢ natDegree.{u} (R := K) 0 ≠ 0

Tactic:
rw [h] at hndf
-- 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
h : f = 0
hndf₁ : natDegree.{u} (R := K) 0 ≠ 0
⊢ f = 0

Tactic:
rw [h] at hndf
-- 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 : natDegree.{u} (R := K) 0 ≠ 0
h : f = 0
⊢ False

Tactic:
hndf rfl

Premises used: rfl
-- 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 : natDegree.{u} (R := K) 0 ≠ 0
h : f = 0
⊢ False

Tactic:
exact hndf rfl

Premises used: rfl
-- 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
⊢ f ≠ 0

Tactic:
have hfn0 : f ≠ 0 := by intro h; rw [h] at hndf; exact hndf rfl
-- 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
⊢ 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
-- 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 :
  ∀
    (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
      (↑(Multiset.toFinset (roots (map (algebraMap K (SplittingFieldAux n.succ f)) f))) :
        Set (SplittingFieldAux n.succ f)))
    ⊤

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

Premises used: Polynomial.map_mul, Polynomial.SplittingFieldAux.algebraMap_succ, Polynomial.X_sub_C_mul_removeFactor, Polynomial.map_map
-- 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 :
  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.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))))
    ⊤
⊢ 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 [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]

Premises used: Finset.coe_singleton, Set.image_singleton, Multiset.toFinset_add, Polynomial.map_X, Polynomial.roots_X_sub_C, Polynomial.roots_mul, Polynomial.map_sub, Polynomial.map_C, Multiset.toFinset_singleton, Finset.coe_union