awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
this : Fact (Irreducible f)
e : g.natDegree = 0
rw :
  Irreducible
    (HSub.hSub (α := (↥K⟮root f⟯)[X]) (β := (↥K⟮root f⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮root f⟯) g)
      ((C : (a : ↥K⟮root f⟯) → (↥K⟮root f⟯)[X]) (AdjoinSimple.gen K (root f)) : (↥K⟮root f⟯)[X]))
⊢ Irreducible (M := (↥K⟮root f⟯)[X])
    ((C : (a : ↥K⟮root f⟯) → (↥K⟮root f⟯)[X])
        (HSub.hSub (α := ↥K⟮root f⟯) (coeff (Polynomial.map (algebraMap K ↥K⟮root f⟯) g) 0)
          (AdjoinSimple.gen K (root f))) :
      (↥K⟮root f⟯)[X])

Tactic:
rw [RingHom.map_sub, coeff_map, ← map_C, ← eq_C_of_natDegree_eq_zero e]

Premises used: Polynomial.coeff_map, Polynomial.eq_C_of_natDegree_eq_zero, RingHom.map_sub, Polynomial.map_C
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
this : Fact (Irreducible f)
e : g.natDegree = 0
x : minpoly K (root f) = f
⊢ Irreducible
    (HSub.hSub (α := (↥K⟮root f⟯)[X]) (β := (↥K⟮root f⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮root f⟯) g)
      ((C : (a : ↥K⟮root f⟯) → (↥K⟮root f⟯)[X]) (AdjoinSimple.gen K (root f)) : (↥K⟮root f⟯)[X]))

Tactic:
apply hg (AdjoinRoot f)

Premises used: AdjoinRoot
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
this : Fact (Irreducible f)
e : g.natDegree = 0
x : HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) = f
x₁ : f * (C : (a : K) → K[X]) 1⁻¹ = f
x₂ : f * (C : (a : K) → K[X]) 1 = f
x₃ : f * 1 = f
x₄ x₅ : f = f
⊢ minpoly K (root f) = f

Tactic:
rw [AdjoinRoot.minpoly_root hf.ne_zero, hfm, inv_one, map_one, mul_one]

Premises used: AdjoinRoot.minpoly_root, inv_one, map_one, Irreducible.ne_zero, mul_one
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
⊢ g.natDegree ≠ 0

Tactic:
have hg' : natDegree g ≠ 0 := by
    have := Fact.mk hf
    intro e
    apply not_irreducible_C ((g.map (algebraMap _ _)).coeff 0 - AdjoinSimple.gen K (root f))
    -- Needed to specialize `map_sub` to avoid a timeout https://github.com/leanprover-community/mathlib4/pull/8386
    rw [RingHom.map_sub, coeff_map, ← map_C, ← eq_C_of_natDegree_eq_zero e]
    apply hg (AdjoinRoot f)
    rw [AdjoinRoot.minpoly_root hf.ne_zero, hfm, inv_one, map_one, mul_one]
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
h : f.comp g = 0
⊢ False

Tactic:
simpa [hf', hg', natDegree_comp] using congr_arg natDegree h

Premises used: Polynomial.natDegree_comp, congr_arg, Polynomial.natDegree
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
⊢ f.comp g ≠ 0

Tactic:
have H₁ : f.comp g ≠ 0 := fun h ↦ by simpa [hf', hg', natDegree_comp] using congr_arg natDegree h
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
h : IsUnit (f.comp g)
⊢ False

Tactic:
simpa [hf', hg', natDegree_comp] using natDegree_eq_zero_of_isUnit h

Premises used: Polynomial.natDegree_comp, Polynomial.natDegree_eq_zero_of_isUnit
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
⊢ ¬IsUnit (f.comp g)

Tactic:
have H₂ : ¬ IsUnit (f.comp g) := fun h ↦
    by simpa [hf', hg', natDegree_comp] using natDegree_eq_zero_of_isUnit h
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
have : ∀ (p : K[X]) (hp₁ : Irreducible p) (hp₂ : p ∣ f.comp g), Irreducible (f.comp g)
⊢ Irreducible (f.comp g)

Tactic:
have ⟨p, hp₁, hp₂⟩ := WfDvdMonoid.exists_irreducible_factor H₂ H₁
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
suffices : p.natDegree = f.natDegree * g.natDegree
⊢ Irreducible (f.comp g)

Tactic:
suffices natDegree p = natDegree f * natDegree g from (associated_of_dvd_of_natDegree_le hp₂ H₁
    (this.trans natDegree_comp.symm).ge).irreducible hp₁
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
⊢ Fact (Irreducible p)

Tactic:
have := Fact.mk hp₁
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this_1 : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := ⋯
⊢ f = minpoly K (B := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)

Tactic:
minpoly.eq_of_irreducible_of_monic hf ?_ hfm

Premises used: minpoly.eq_of_irreducible_of_monic
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this_1 : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := ⋯
refine :
  Eq (α := AdjoinRoot p)
    (((aeval ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g) : K[X] →ₐ[K] AdjoinRoot p) : (a : K[X]) → AdjoinRoot p)
        f :
      AdjoinRoot p)
    (0 : AdjoinRoot p)
⊢ f = minpoly K (B := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)

Tactic:
refine minpoly.eq_of_irreducible_of_monic hf ?_ hfm

Premises used: minpoly.eq_of_irreducible_of_monic
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this_1 : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := ⋯
rw : Eq (α := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) (f.comp g) : AdjoinRoot p) (0 : AdjoinRoot p)
⊢ Eq (α := AdjoinRoot p)
    (((aeval ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g) : K[X] →ₐ[K] AdjoinRoot p) : (a : K[X]) → AdjoinRoot p)
        f :
      AdjoinRoot p)
    (0 : AdjoinRoot p)

Tactic:
rw [← aeval_comp]

Premises used: Polynomial.aeval_comp
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this_1 : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := ⋯
⊢ Eq (α := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) (f.comp g) : AdjoinRoot p) (0 : AdjoinRoot p)

Tactic:
aeval_eq_zero_of_dvd_aeval_eq_zero hp₂ (AdjoinRoot.eval₂_root p)

Premises used: AdjoinRoot.eval₂_root, Polynomial.aeval_eq_zero_of_dvd_aeval_eq_zero
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this_1 : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := ⋯
⊢ Eq (α := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) (f.comp g) : AdjoinRoot p) (0 : AdjoinRoot p)

Tactic:
exact aeval_eq_zero_of_dvd_aeval_eq_zero hp₂ (AdjoinRoot.eval₂_root p)

Premises used: AdjoinRoot.eval₂_root, Polynomial.aeval_eq_zero_of_dvd_aeval_eq_zero
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this_1 : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := ⋯
⊢ f = minpoly K (B := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)

Tactic:
have key₁ : f = minpoly K (aeval (root p) g) := by
    refine minpoly.eq_of_irreducible_of_monic hf ?_ hfm
    rw [← aeval_comp]
    exact aeval_eq_zero_of_dvd_aeval_eq_zero hp₂ (AdjoinRoot.eval₂_root p)
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this_1 : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := ⋯
key₁ : f = minpoly K (B := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)
rw : IsIntegral K (A := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)
⊢ finrank K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯ = f.natDegree

Tactic:
rw [adjoin.finrank, ← key₁]

Premises used: IntermediateField.adjoin.finrank
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this_1 : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := ⋯
key₁ : f = minpoly K (B := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)
⊢ IsIntegral K (A := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)

Tactic:
IsIntegral.of_finite _ _

Premises used: IsIntegral.of_finite
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this_1 : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := ⋯
key₁ : f = minpoly K (B := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)
⊢ IsIntegral K (A := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)

Tactic:
exact IsIntegral.of_finite _ _

Premises used: IsIntegral.of_finite
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this_1 : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := ⋯
key₁ : f = minpoly K (B := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)
⊢ finrank K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯ = f.natDegree

Tactic:
have key₁' : finrank K K⟮aeval (root p) g⟯ = natDegree f := by
    rw [adjoin.finrank, ← key₁]
    exact IsIntegral.of_finite _ _
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this_1 : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := ⋯
key₁ : f = minpoly K (B := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)
key₁' : finrank K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯ = f.natDegree
⊢ Eq (α := AdjoinRoot p)
    ((aeval (root p) : (a : (↥K⟮(aeval (root p) : (a : K[X]) → AdjoinRoot p) g⟯)[X]) → AdjoinRoot p)
        (HSub.hSub (α := (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)[X]) (β :=
          (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)[X])
          (Polynomial.map (algebraMap K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) g)
          ((C :
                (a : ↥K⟮(aeval (root p) : (a : K[X]) → AdjoinRoot p) g⟯) →
                  (↥K⟮(aeval (root p) : (a : K[X]) → AdjoinRoot p) g⟯)[X])
              (AdjoinSimple.gen K ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g)) :
            (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)[X])) :
      AdjoinRoot p)
    (0 : AdjoinRoot p)

Tactic:
simp [AdjoinSimple.gen]

Premises used: IntermediateField.AdjoinSimple.gen
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this_1 : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := ⋯
key₁ : f = minpoly K (B := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)
key₁' : finrank K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯ = f.natDegree
⊢ natDegree.{u} (R := ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)
      ((C :
          (a : ↥K⟮(aeval (root p) : (a : K[X]) → AdjoinRoot p) g⟯) →
            (↥K⟮(aeval (root p) : (a : K[X]) → AdjoinRoot p) g⟯)[X])
        (AdjoinSimple.gen K ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g))) <
    natDegree (R := ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)
      (Polynomial.map (algebraMap K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) g)

Tactic:
simpa [Nat.pos_iff_ne_zero] using hg'

Premises used: Nat.pos_iff_ne_zero
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this_1 : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := ⋯
key₁ : f = minpoly K (B := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)
key₁' : finrank K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯ = f.natDegree
⊢ HSub.hSub (α := (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)[X]) (β :=
      (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)[X])
      (Polynomial.map (algebraMap K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) g)
      ((C :
            (a : ↥K⟮(aeval (root p) : (a : K[X]) → AdjoinRoot p) g⟯) →
              (↥K⟮(aeval (root p) : (a : K[X]) → AdjoinRoot p) g⟯)[X])
          (AdjoinSimple.gen K ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g)) :
        (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)[X]) =
    minpoly (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) (root p)

Tactic:
have key₂ : g.map (algebraMap _ _) - C (AdjoinSimple.gen K (aeval (root p) g)) =
      minpoly K⟮aeval (root p) g⟯ (root p) :=
    minpoly.eq_of_irreducible_of_monic (hg _ _ key₁.symm) (by simp [AdjoinSimple.gen])
      (Monic.sub_of_left (hgm.map _) (degree_lt_degree (by simpa [Nat.pos_iff_ne_zero] using hg')))