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
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
key₂ :
  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)
trans :
  finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx =
    natDegree (R := ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)
      (minpoly (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) (root p))
trans₁ :
  natDegree (R := ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)
      (minpoly (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) (root p)) =
    g.natDegree
⊢ finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx = g.natDegree

Tactic:
trans natDegree (minpoly K⟮aeval (root p) g⟯ (root p))

Premises used: Membership.mem, Subtype, minpoly, IntermediateField.adjoin, AdjoinRoot.root, Polynomial.aeval, Polynomial.natDegree, Singleton.singleton, DFunLike.coe
-- 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
key₂ :
  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)
a :
  Eq (α := IntermediateField K (AdjoinRoot p))
    (restrictScalars K (L' := ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)
      (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)⟮root p⟯)
    (restrictScalars K (L' := ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) ⊤)
⊢ Eq (α := IntermediateField (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) (AdjoinRoot p))
    (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)⟮root p⟯ ⊤

Tactic:
apply restrictScalars_injective K

Premises used: IntermediateField.restrictScalars_injective
-- 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
key₂ :
  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)
a :
  Eq (α := IntermediateField K (AdjoinRoot p))
    (adjoin K
      ((↑⊤ : Set (AdjoinRoot p)) ∪
        singleton (α := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)))
    ⊤
⊢ Eq (α := IntermediateField K (AdjoinRoot p))
    (restrictScalars K (L' := ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)
      (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)⟮root p⟯)
    (restrictScalars K (L' := ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) ⊤)

Tactic:
rw [restrictScalars_top, adjoin_adjoin_left, Set.union_comm, ← adjoin_adjoin_left,
          adjoin_root_eq_top p, restrictScalars_adjoin]

Premises used: IntermediateField.restrictScalars_top, IntermediateField.adjoin_root_eq_top, Set.union_comm, IntermediateField.adjoin_adjoin_left, IntermediateField.restrictScalars_adjoin
-- 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
key₂ :
  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)
⊢ Eq (α := IntermediateField K (AdjoinRoot p))
    (adjoin K
      ((↑⊤ : Set (AdjoinRoot p)) ∪
        singleton (α := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)))
    ⊤

Tactic:
simp
-- 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
key₂ :
  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)
⊢ Eq (α := IntermediateField (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) (AdjoinRoot p))
    (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)⟮root p⟯ ⊤

Tactic:
have : K⟮aeval (root p) g⟯⟮root p⟯ = ⊤ := by
        apply restrictScalars_injective K
        rw [restrictScalars_top, adjoin_adjoin_left, Set.union_comm, ← adjoin_adjoin_left,
          adjoin_root_eq_top p, restrictScalars_adjoin]
        simp
-- 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_2 : 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
key₂ :
  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)
this :
  Eq (α := IntermediateField (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) (AdjoinRoot p))
    (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)⟮root p⟯ ⊤
rw : IsIntegral (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) (root p)
⊢ finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx =
    natDegree (R := ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)
      (minpoly (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) (root p))

Tactic:
rw [← finrank_top', ← this, adjoin.finrank]

Premises used: IntermediateField.adjoin.finrank, IntermediateField.finrank_top'
-- 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_2 : 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
key₂ :
  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)
this :
  Eq (α := IntermediateField (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) (AdjoinRoot p))
    (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)⟮root p⟯ ⊤
⊢ IsIntegral (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) (root 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_2 : 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
key₂ :
  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)
this :
  Eq (α := IntermediateField (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) (AdjoinRoot p))
    (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)⟮root p⟯ ⊤
⊢ IsIntegral (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) (root 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)
key₁' : finrank K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯ = f.natDegree
key₂ :
  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)
⊢ natDegree (R := ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)
      (minpoly (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) (root p)) =
    g.natDegree

Tactic:
simp [← key₂]
-- 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
key₂ :
  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)
⊢ finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx = g.natDegree

Tactic:
have key₂' : finrank K⟮aeval (root p) g⟯ Kx = natDegree g := by
    trans natDegree (minpoly K⟮aeval (root p) g⟯ (root p))
    · have : K⟮aeval (root p) g⟯⟮root p⟯ = ⊤ := by
        apply restrictScalars_injective K
        rw [restrictScalars_top, adjoin_adjoin_left, Set.union_comm, ← adjoin_adjoin_left,
          adjoin_root_eq_top p, restrictScalars_adjoin]
        simp
      rw [← finrank_top', ← this, adjoin.finrank]
      exact IsIntegral.of_finite _ _
    · simp [← key₂]
-- 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
key₂ :
  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)
key₂' : finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx = g.natDegree
⊢ finrank K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯ *
      finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx =
    finrank K Kx

Tactic:
have := Module.finrank_mul_finrank K K⟮aeval (root p) g⟯ Kx