awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pb : PowerBasis R S
I : Ideal R
x : R
rw :
  Eq (α := Ideal (AdjoinRoot (minpoly R pb.gen)))
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I)
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen))
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(equiv' (minpoly R pb.gen) pb ⋯ ⋯).symm.toRingEquiv : S →+* AdjoinRoot (minpoly R pb.gen)) (algebraMap R S))
      I)
rw₁ :
  Eq (α := Ideal (AdjoinRoot (minpoly R pb.gen)))
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I)
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen))
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(↑(equiv' (minpoly R pb.gen) pb ⋯ ⋯).symm : S →ₐ[R] AdjoinRoot (minpoly R pb.gen)) :
          S →+* AdjoinRoot (minpoly R pb.gen))
        (algebraMap R S))
      I)
rw₂ :
  Eq (α := Ideal (AdjoinRoot (minpoly R pb.gen)))
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (algebraMap R (AdjoinRoot (minpoly R pb.gen))) I)
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen))
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(↑(equiv' (minpoly R pb.gen) pb ⋯ ⋯).symm : S →ₐ[R] AdjoinRoot (minpoly R pb.gen)) :
          S →+* AdjoinRoot (minpoly R pb.gen))
        (algebraMap R S))
      I)
rw₃ rw₄ :
  Eq (α := Ideal (AdjoinRoot (minpoly R pb.gen)))
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (algebraMap R (AdjoinRoot (minpoly R pb.gen))) I)
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (algebraMap R (AdjoinRoot (minpoly R pb.gen))) I)
⊢ Eq (α := Ideal (AdjoinRoot (minpoly R pb.gen)))
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I)
    (Ideal.map (R := S) (F := RingHom.{u_2, u_1} S (AdjoinRoot (minpoly R pb.gen)))
      (↑(equiv' (minpoly R pb.gen) pb ⋯ ⋯).symm.toRingEquiv : S →+* AdjoinRoot (minpoly R pb.gen))
      (Ideal.map (F := R →+* S) (algebraMap R S) I))

Tactic:
rw [Ideal.map_map,
                      ← AlgEquiv.coe_ringHom_commutes, ← AdjoinRoot.algebraMap_eq,
                      AlgHom.comp_algebraMap]

Premises used: AlgHom.comp_algebraMap, AdjoinRoot.algebraMap_eq, Ideal.map_map, AlgEquiv.coe_ringHom_commutes
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pb : PowerBasis R S
I : Ideal R
g : R[X]
⊢ Eq.{u_2 + 1} (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (((pb.quotientEquivQuotientMinpolyMap I).symm :
          (a : (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}) →
            S ⧸ Ideal.map (algebraMap R S) I)
        ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}) :
            (a : (R ⧸ I)[X]) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)})
          (Polynomial.map (Ideal.Quotient.mk I) g)) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
        ((aeval pb.gen : (a : R[X]) → S) g) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))

Tactic:
simp [quotientEquivQuotientMinpolyMap, aeval_def]

Premises used: Polynomial.aeval_def, PowerBasis.quotientEquivQuotientMinpolyMap
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_6
L : Type u_7
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra.IsIntegral K L
f : L[X]
hf : Irreducible f
⊢ Fact (Irreducible f)

Tactic:
haveI := Fact.mk hf
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_6
L : Type u_7
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra.IsIntegral K L
f : L[X]
hf : Irreducible f
this : Fact (Irreducible f)
⊢ f ≠ 0

Tactic:
have h := hf.ne_zero
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_6
L : Type u_7
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra.IsIntegral K L
f : L[X]
hf : Irreducible f
this : Fact (Irreducible f)
h : f ≠ 0
⊢ IsIntegral K (AdjoinRoot.root f)

Tactic:
have h2 := isIntegral_trans (R := K) _ (AdjoinRoot.isIntegral_root h)
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_6
L : Type u_7
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra.IsIntegral K L
f : L[X]
hf : Irreducible f
this : Fact (Irreducible f)
h : f ≠ 0
h2 : IsIntegral K (AdjoinRoot.root f)
⊢ HMul.hMul (β := L[X]) f ((C : (a : L) → L[X]) f.leadingCoeff⁻¹ : L[X]) ∣
    Polynomial.map (algebraMap K L) (minpoly K (AdjoinRoot.root f))

Tactic:
have h3 := (AdjoinRoot.minpoly_root h) ▸ minpoly.dvd_map_of_isScalarTower K L (AdjoinRoot.root f)
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_6
L : Type u_7
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra.IsIntegral K L
f : L[X]
hf : Irreducible f
this : Fact (Irreducible f)
h : f ≠ 0
h2 : IsIntegral K (AdjoinRoot.root f)
h3 :
  HMul.hMul (β := L[X]) f ((C : (a : L) → L[X]) f.leadingCoeff⁻¹ : L[X]) ∣
    Polynomial.map (algebraMap K L) (minpoly K (AdjoinRoot.root f))
⊢ ∃ (g : K[X]), g.Monic ∧ Irreducible g ∧ f ∣ Polynomial.map (algebraMap K L) g

Tactic:
⟨_, minpoly.monic h2, minpoly.irreducible h2, dvd_of_mul_right_dvd h3⟩

Premises used: minpoly.monic, dvd_of_mul_right_dvd, And.intro, Exists.intro, minpoly.irreducible
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_6
L : Type u_7
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra.IsIntegral K L
f : L[X]
hf : Irreducible f
this : Fact (Irreducible f)
h : f ≠ 0
h2 : IsIntegral K (AdjoinRoot.root f)
h3 :
  HMul.hMul (β := L[X]) f ((C : (a : L) → L[X]) f.leadingCoeff⁻¹ : L[X]) ∣
    Polynomial.map (algebraMap K L) (minpoly K (AdjoinRoot.root f))
⊢ ∃ (g : K[X]), g.Monic ∧ Irreducible g ∧ f ∣ Polynomial.map (algebraMap K L) g

Tactic:
exact ⟨_, minpoly.monic h2, minpoly.irreducible h2, dvd_of_mul_right_dvd h3⟩
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
pos :
  ∀ (hpu : IsUnit p),
    ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
      (Polynomial.map (algebraMap R S) p).Splits
neg :
  ∀ (hpu : ¬IsUnit p),
    ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
      (Polynomial.map (algebraMap R S) p).Splits
⊢ ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
    (Polynomial.map (algebraMap R S) p).Splits

Tactic:
by_cases hpu : IsUnit p

Premises used: IsUnit
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : IsUnit p
pos :
  ∀ (hp : Monic.{u} (R := R) 1) (hn : natDegree.{u} (R := R) 1 = n) (hpu : IsUnit.{u} (M := R[X]) 1),
    ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
      (Polynomial.map (algebraMap R S) 1).Splits
⊢ ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
    (Polynomial.map (algebraMap R S) p).Splits

Tactic:
obtain rfl := hp.eq_one_of_isUnit hpu

Premises used: Polynomial.Monic.eq_one_of_isUnit, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
hp : Monic.{u} (R := R) 1
hn : natDegree.{u} (R := R) 1 = n
hpu : IsUnit.{u} (M := R[X]) 1
⊢ Splits (Polynomial.map (algebraMap R R) 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
hp : Monic.{u} (R := R) 1
hn : natDegree.{u} (R := R) 1 = n
hpu : IsUnit.{u} (M := R[X]) 1
⊢ ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
    (Polynomial.map (algebraMap R S) 1).Splits

Tactic:
exact ⟨R, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance, by simp⟩
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
⊢ HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
      ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X]) ∣
    Polynomial.map (algebraMap R (AdjoinRoot p)) p

Tactic:
simp [dvd_iff_isRoot, -AdjoinRoot.algebraMap_eq]

Premises used: AdjoinRoot.algebraMap_eq, Polynomial.dvd_iff_isRoot
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
neg :
  ∀ (q : (AdjoinRoot p)[X])
    (hq :
      Polynomial.map (algebraMap R (AdjoinRoot p)) p =
        HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
            ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X]) *
          q),
    ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
      (Polynomial.map (algebraMap R S) p).Splits
⊢ ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
    (Polynomial.map (algebraMap R S) p).Splits

Tactic:
obtain ⟨q, hq⟩ : X - C (AdjoinRoot.root p) ∣ p.map (algebraMap _ _) := by
    simp [dvd_iff_isRoot, -AdjoinRoot.algebraMap_eq]

Premises used: Polynomial.C, Algebra.algebraMap, AdjoinRoot.root, Polynomial.map, Polynomial.X, DFunLike.coe
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq :
  Polynomial.map (algebraMap R (AdjoinRoot p)) p =
    HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
        ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X]) *
      q
⊢ q.Monic

Tactic:
have hqm : q.Monic := .of_mul_monic_left (monic_X_sub_C (.root _)) (hq ▸ hp.map _)
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq :
  Polynomial.map (algebraMap R (AdjoinRoot p)) p =
    HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
        ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X]) *
      q
hqm : q.Monic
⊢ Free R (AdjoinRoot p)

Tactic:
have := hp.free_adjoinRoot
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq :
  Polynomial.map (algebraMap R (AdjoinRoot p)) p =
    HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
        ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X]) *
      q
hqm : q.Monic
this : Free R (AdjoinRoot p)
⊢ Module.Finite R (AdjoinRoot p)

Tactic:
have := hp.finite_adjoinRoot
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq :
  Polynomial.map (algebraMap R (AdjoinRoot p)) p =
    HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
        ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X]) *
      q
hqm : q.Monic
this_1 : Free R (AdjoinRoot p)
this : Module.Finite R (AdjoinRoot p)
⊢ Ne (α := Ideal R[X]) (span {p}) ⊤

Tactic:
simpa
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq :
  Polynomial.map (algebraMap R (AdjoinRoot p)) p =
    HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
        ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X]) *
      q
hqm : q.Monic
this_1 : Free R (AdjoinRoot p)
this : Module.Finite R (AdjoinRoot p)
⊢ Nontrivial.{u} (AdjoinRoot p)

Tactic:
have : Nontrivial (AdjoinRoot p) := Ideal.Quotient.nontrivial_iff.mpr (by simpa)
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq :
  Polynomial.map (algebraMap R (AdjoinRoot p)) p =
    HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
        ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X]) *
      q
hqm : q.Monic
this_1 : Free R (AdjoinRoot p)
this_2 : Module.Finite R (AdjoinRoot p)
this : Nontrivial.{u} (AdjoinRoot p)
rw :
  q.natDegree <
    (HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
          ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X])).natDegree +
      q.natDegree
⊢ q.natDegree < n

Tactic:
rw [← hn, ← hp.natDegree_map (algebraMap R (AdjoinRoot p)), hq,
      Monic.natDegree_mul (monic_X_sub_C _) hqm]

Premises used: Polynomial.monic_X_sub_C, AdjoinRoot, Algebra.algebraMap, Polynomial.Monic.natDegree_map, Polynomial.Monic.natDegree_mul
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq :
  Polynomial.map (algebraMap R (AdjoinRoot p)) p =
    HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
        ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X]) *
      q
hqm : q.Monic
this_1 : Free R (AdjoinRoot p)
this_2 : Module.Finite R (AdjoinRoot p)
this : Nontrivial.{u} (AdjoinRoot p)
⊢ q.natDegree <
    (HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
          ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X])).natDegree +
      q.natDegree

Tactic:
simp
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq :
  Polynomial.map (algebraMap R (AdjoinRoot p)) p =
    HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
        ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X]) *
      q
hqm : q.Monic
this_1 : Free R (AdjoinRoot p)
this_2 : Module.Finite R (AdjoinRoot p)
this : Nontrivial.{u} (AdjoinRoot p)
neg :
  ∀ (S : Type u) (w : CommRing S) (w_1 : Algebra (AdjoinRoot p) S),
    Module.Finite (AdjoinRoot p) S →
      Free (AdjoinRoot p) S →
        Nontrivial S →
          ∀ (hS : (Polynomial.map (algebraMap (AdjoinRoot p) S) q).Splits),
            ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ :
              Nontrivial S), (Polynomial.map (algebraMap R S) p).Splits
⊢ ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
    (Polynomial.map (algebraMap R S) p).Splits

Tactic:
obtain ⟨S, _, _, _, _, _, hS⟩ := IH _
    (by rw [← hn, ← hp.natDegree_map (algebraMap R (AdjoinRoot p)), hq,
      Monic.natDegree_mul (monic_X_sub_C _) hqm]; simp) hqm rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq :
  Polynomial.map (algebraMap R (AdjoinRoot p)) p =
    HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
        ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X]) *
      q
hqm : q.Monic
this_1 : Free R (AdjoinRoot p)
this_2 : Module.Finite R (AdjoinRoot p)
this : Nontrivial.{u} (AdjoinRoot p)
S : Type u
w : CommRing S
w_1 : Algebra (AdjoinRoot p) S
w_2 : Module.Finite (AdjoinRoot p) S
w_3 : Free (AdjoinRoot p) S
w_4 : Nontrivial S
hS : Splits (Polynomial.map (algebraMap (AdjoinRoot p) S) q)
algInst : Algebra R S :=
  RingHom.toAlgebra
    (@RingHom.comp _ (AdjoinRoot p) _ _ Semiring.toNonAssocSemiring _ (algebraMap (AdjoinRoot p) S)
      (algebraMap R (AdjoinRoot p)))
scalarTowerInst : IsScalarTower R (AdjoinRoot p) S := ⋯
⊢ ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
    (Polynomial.map (algebraMap R S) p).Splits

Tactic:
⟨S, ‹_›, ‹_›, .trans (AdjoinRoot p) _, .trans (S := AdjoinRoot p), ‹_›, ?_⟩

Premises used: AdjoinRoot, Module.Finite.trans, Exists.intro, Module.Free.trans
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq :
  Polynomial.map (algebraMap R (AdjoinRoot p)) p =
    HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
        ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X]) *
      q
hqm : q.Monic
this_1 : Free R (AdjoinRoot p)
this_2 : Module.Finite R (AdjoinRoot p)
this : Nontrivial.{u} (AdjoinRoot p)
S : Type u
w : CommRing S
w_1 : Algebra (AdjoinRoot p) S
w_2 : Module.Finite (AdjoinRoot p) S
w_3 : Free (AdjoinRoot p) S
w_4 : Nontrivial S
hS : Splits (Polynomial.map (algebraMap (AdjoinRoot p) S) q)
algInst : Algebra R S :=
  RingHom.toAlgebra
    (@RingHom.comp _ (AdjoinRoot p) _ _ Semiring.toNonAssocSemiring _ (algebraMap (AdjoinRoot p) S)
      (algebraMap R (AdjoinRoot p)))
scalarTowerInst : IsScalarTower R (AdjoinRoot p) S := ⋯
neg : Splits (Polynomial.map (algebraMap R S) p)
⊢ ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
    (Polynomial.map (algebraMap R S) p).Splits

Tactic:
refine ⟨S, ‹_›, ‹_›, .trans (AdjoinRoot p) _, .trans (S := AdjoinRoot p), ‹_›, ?_⟩