awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this_1 : Fact (Irreducible (M := F[X]) (minpoly F α))
this : toSubfield F⟮α⟯ ≤ (RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange
x : ↥F⟮α⟯
obtain :
  ∀ (y : AdjoinRoot (minpoly F α))
    (hy : (RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f : (a : AdjoinRoot (minpoly F α)) → E) y = (↑x : E)),
    ∃ (a : AdjoinRoot (minpoly F α)),
      ((AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯ :
              AlgHom.{u_1, u_1, u_2} F (AdjoinRoot (minpoly F α)) ↥F⟮α⟯) :
            (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯)
          a =
        x
⊢ ∃ (a : AdjoinRoot (minpoly F α)),
    ((AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯ :
            AlgHom.{u_1, u_1, u_2} F (AdjoinRoot (minpoly F α)) ↥F⟮α⟯) :
          (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯)
        a =
      x

Tactic:
obtain ⟨y, hy⟩ := this (Subtype.mem x)

Premises used: Subtype.mem
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this_1 : Fact (Irreducible (M := F[X]) (minpoly F α))
this : toSubfield F⟮α⟯ ≤ (RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange
x : ↥F⟮α⟯
y : AdjoinRoot (minpoly F α)
hy : (RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f : (a : AdjoinRoot (minpoly F α)) → E) y = (↑x : E)
⊢ ∃ (a : AdjoinRoot (minpoly F α)),
    ((AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯ :
            AlgHom.{u_1, u_1, u_2} F (AdjoinRoot (minpoly F α)) ↥F⟮α⟯) :
          (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯)
        a =
      x

Tactic:
⟨y, Subtype.ext hy⟩

Premises used: Exists.intro, Subtype.ext
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this_1 : Fact (Irreducible (M := F[X]) (minpoly F α))
this : toSubfield F⟮α⟯ ≤ (RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange
x : ↥F⟮α⟯
y : AdjoinRoot (minpoly F α)
hy : (RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f : (a : AdjoinRoot (minpoly F α)) → E) y = (↑x : E)
⊢ ∃ (a : AdjoinRoot (minpoly F α)),
    ((AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯ :
            AlgHom.{u_1, u_1, u_2} F (AdjoinRoot (minpoly F α)) ↥F⟮α⟯) :
          (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯)
        a =
      x

Tactic:
exact ⟨y, Subtype.ext hy⟩
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
right : toSubfield F⟮α⟯ ≤ (RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := AdjoinRoot (minpoly F α)) (β := ↥F⟮α⟯)
    (⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯) :
      (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯)

Tactic:
suffices F⟮α⟯.toSubfield ≤ RingHom.fieldRange (F⟮α⟯.toSubfield.subtype.comp f) by
          intro x
          obtain ⟨y, hy⟩ := this (Subtype.mem x)
          exact ⟨y, Subtype.ext hy⟩
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
⊢ toSubfield F⟮α⟯ ≤ (RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange

Tactic:
Subfield.closure_le.mpr (Set.union_subset (fun x hx => ?_) ?_)

Premises used: Iff.mpr, Subfield.closure_le, Set.Mem, Set.union_subset
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
right :
  ∀ (x : E) (hx : Membership.mem (γ := Set E) (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) x),
    x ∈ (↑(RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange : Set E)
right₁ : {α} ⊆ (↑(RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange : Set E)
⊢ toSubfield F⟮α⟯ ≤ (RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange

Tactic:
refine Subfield.closure_le.mpr (Set.union_subset (fun x hx => ?_) ?_)

Premises used: Iff.mpr, Subfield.closure_le, Set.union_subset
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
x : E
hx : Membership.mem (γ := Set E) (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) x
right :
  ∀ (y : F) (hy : (algebraMap F E : (a : F) → E) y = x),
    x ∈ (↑(RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange : Set E)
⊢ x ∈ (↑(RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange : Set E)

Tactic:
obtain ⟨y, hy⟩ := hx
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
x : E
y : F
hy : (algebraMap F E : (a : F) → E) y = x
⊢ x ∈ (↑(RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange : Set E)

Tactic:
⟨y, ?_⟩

Premises used: Set.Mem, setOf, minpoly, Exists.intro, Set.range, AdjoinRoot.of, DFunLike.coe
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
x : E
y : F
hy : (algebraMap F E : (a : F) → E) y = x
right :
  (RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f : (a : AdjoinRoot (minpoly F α)) → E)
      ((AdjoinRoot.of (minpoly F α) : (a : F) → AdjoinRoot (minpoly F α)) y : AdjoinRoot (minpoly F α)) =
    x
⊢ x ∈ (↑(RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange : Set E)

Tactic:
refine ⟨y, ?_⟩
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
x : E
y : F
hy : (algebraMap F E : (a : F) → E) y = x
right :
  (Subfield.subtype (toSubfield F⟮α⟯) : (a : ↥F⟮α⟯.toSubfield) → E)
      ((f : (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯.toSubfield)
          ((AdjoinRoot.of (minpoly F α) : (a : F) → AdjoinRoot (minpoly F α)) y) :
        ↥(toSubfield F⟮α⟯)) =
    x
⊢ (RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f : (a : AdjoinRoot (minpoly F α)) → E)
      ((AdjoinRoot.of (minpoly F α) : (a : F) → AdjoinRoot (minpoly F α)) y : AdjoinRoot (minpoly F α)) =
    x

Tactic:
rw [RingHom.comp_apply]

Premises used: RingHom.comp_apply
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
x : E
y : F
hy : (algebraMap F E : (a : F) → E) y = x
right :
  (Subfield.subtype (toSubfield F⟮α⟯) : (a : ↥F⟮α⟯) → E)
      ((f : (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯)
          ((AdjoinRoot.of (minpoly F α) : (a : F) → AdjoinRoot (minpoly F α)) y) :
        ↥F⟮α⟯) =
    x
⊢ (Subfield.subtype (toSubfield F⟮α⟯) : (a : ↥F⟮α⟯.toSubfield) → E)
      ((f : (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯.toSubfield)
          ((AdjoinRoot.of (minpoly F α) : (a : F) → AdjoinRoot (minpoly F α)) y) :
        ↥(toSubfield F⟮α⟯)) =
    x

Tactic:
dsimp only [coe_type_toSubfield]

Premises used: IntermediateField.coe_type_toSubfield
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
x : E
y : F
hy : (algebraMap F E : (a : F) → E) y = x
right :
  (Subfield.subtype (toSubfield F⟮α⟯) : (a : ↥F⟮α⟯) → E)
      ((((↑(Algebra.ofId F ↥F⟮α⟯) : RingHom.{u_1, u_2} F ↥F⟮α⟯) : RingHom.{u_1, u_2} F ↥F⟮α⟯) : (a : F) → ↥F⟮α⟯) y :
        ↥F⟮α⟯) =
    x
⊢ (Subfield.subtype (toSubfield F⟮α⟯) : (a : ↥F⟮α⟯) → E)
      ((f : (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯)
          ((AdjoinRoot.of (minpoly F α) : (a : F) → AdjoinRoot (minpoly F α)) y) :
        ↥F⟮α⟯) =
    x

Tactic:
rw [AdjoinRoot.lift_of (aeval_gen_minpoly F α)]

Premises used: IntermediateField.aeval_gen_minpoly, AdjoinRoot.lift_of
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
x : E
y : F
hy : (algebraMap F E : (a : F) → E) y = x
⊢ (Subfield.subtype (toSubfield F⟮α⟯) : (a : ↥F⟮α⟯) → E)
      ((((↑(Algebra.ofId F ↥F⟮α⟯) : RingHom.{u_1, u_2} F ↥F⟮α⟯) : RingHom.{u_1, u_2} F ↥F⟮α⟯) : (a : F) → ↥F⟮α⟯) y :
        ↥F⟮α⟯) =
    x

Tactic:
hy
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
x : E
y : F
hy : (algebraMap F E : (a : F) → E) y = x
⊢ (Subfield.subtype (toSubfield F⟮α⟯) : (a : ↥F⟮α⟯) → E)
      ((((↑(Algebra.ofId F ↥F⟮α⟯) : RingHom.{u_1, u_2} F ↥F⟮α⟯) : RingHom.{u_1, u_2} F ↥F⟮α⟯) : (a : F) → ↥F⟮α⟯) y :
        ↥F⟮α⟯) =
    x

Tactic:
exact hy
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
⊢ {α} ⊆ (↑(RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange : Set E)

Tactic:
Set.singleton_subset_iff.mpr ⟨AdjoinRoot.root (minpoly F α), ?_⟩

Premises used: Iff.mpr, Set.singleton_subset_iff, minpoly, AdjoinRoot.root, Exists.intro
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
right :
  (RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f : (a : AdjoinRoot (minpoly F α)) → E)
      (AdjoinRoot.root (minpoly F α)) =
    α
⊢ {α} ⊆ (↑(RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange : Set E)

Tactic:
refine Set.singleton_subset_iff.mpr ⟨AdjoinRoot.root (minpoly F α), ?_⟩
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
right :
  (Subfield.subtype (toSubfield F⟮α⟯) : (a : ↥F⟮α⟯.toSubfield) → E)
      ((f : (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯.toSubfield) (AdjoinRoot.root (minpoly F α)) : ↥(toSubfield F⟮α⟯)) =
    α
⊢ (RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f : (a : AdjoinRoot (minpoly F α)) → E)
      (AdjoinRoot.root (minpoly F α)) =
    α

Tactic:
rw [RingHom.comp_apply]

Premises used: RingHom.comp_apply
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
right :
  (Subfield.subtype (toSubfield F⟮α⟯) : (a : ↥F⟮α⟯) → E)
      ((f : (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯) (AdjoinRoot.root (minpoly F α)) : ↥F⟮α⟯) =
    α
⊢ (Subfield.subtype (toSubfield F⟮α⟯) : (a : ↥F⟮α⟯.toSubfield) → E)
      ((f : (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯.toSubfield) (AdjoinRoot.root (minpoly F α)) : ↥(toSubfield F⟮α⟯)) =
    α

Tactic:
dsimp only [coe_type_toSubfield]

Premises used: IntermediateField.coe_type_toSubfield
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
right : (Subfield.subtype (toSubfield F⟮α⟯) : (a : ↥F⟮α⟯) → E) (AdjoinSimple.gen F α) = α
⊢ (Subfield.subtype (toSubfield F⟮α⟯) : (a : ↥F⟮α⟯) → E)
      ((f : (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯) (AdjoinRoot.root (minpoly F α)) : ↥F⟮α⟯) =
    α

Tactic:
rw [AdjoinRoot.lift_root (aeval_gen_minpoly F α)]

Premises used: IntermediateField.aeval_gen_minpoly, AdjoinRoot.lift_root
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
⊢ (Subfield.subtype (toSubfield F⟮α⟯) : (a : ↥F⟮α⟯) → E) (AdjoinSimple.gen F α) = α

Tactic:
rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
h : IsIntegral F α
⊢ Eq.{u_2 + 1} (α := ↥F⟮α⟯)
    ((adjoinRootEquivAdjoin F h : (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯) (AdjoinRoot.root (minpoly F α)) : ↥F⟮α⟯)
    (AdjoinSimple.gen F α : ↥F⟮α⟯)

Tactic:
AdjoinRoot.lift_root (aeval_gen_minpoly F α)

Premises used: IntermediateField.aeval_gen_minpoly, Quotient.liftOn', Set.Mem, AddCon.liftOn, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, RingHom.codRestrict, AdjoinRoot.lift_root
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
h : IsIntegral F α
rw :
  Eq (α := ↥F⟮α⟯) (AdjoinSimple.gen F α)
    ((adjoinRootEquivAdjoin F h : (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯) (AdjoinRoot.root (minpoly F α)))
rw₁ rw₂ : Eq (α := ↥F⟮α⟯) (AdjoinSimple.gen F α) (AdjoinSimple.gen F α)
⊢ Eq.{u_1 + 1} (α := AdjoinRoot (minpoly F α))
    (((adjoinRootEquivAdjoin F h).symm : (a : ↥F⟮α⟯) → AdjoinRoot (minpoly F α)) (AdjoinSimple.gen F α) :
      AdjoinRoot (minpoly F α))
    (AdjoinRoot.root (minpoly F α) : AdjoinRoot (minpoly F α))

Tactic:
rw [AlgEquiv.symm_apply_eq, adjoinRootEquivAdjoin_apply_root]

Premises used: AlgEquiv.symm_apply_eq, IntermediateField.adjoinRootEquivAdjoin_apply_root
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
p : K[X]
inst_1 : Fact (Irreducible p)
⊢ Eq (α := IntermediateField K (AdjoinRoot p)) K⟮AdjoinRoot.root p⟯ ⊤

Tactic:
(eq_adjoin_of_eq_algebra_adjoin K _ ⊤ (AdjoinRoot.adjoinRoot_eq_top (f := p)).symm).symm

Premises used: AdjoinRoot.adjoinRoot_eq_top, Top.top, Eq.symm, IntermediateField.eq_adjoin_of_eq_algebra_adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
x : L
hx : IsIntegral K x
⊢ FiniteDimensional.{u, u_3} K ↥K⟮x⟯

Tactic:
(adjoin.powerBasis hx).finite

Premises used: Set.Mem, IntermediateField.adjoin, PowerBasis.finite, IntermediateField.adjoin.powerBasis
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
x : L
hx : IsIntegral K x
⊢ Algebra.IsAlgebraic.{u, u_3} K ↥K⟮x⟯

Tactic:
have := adjoin.finiteDimensional hx; Algebra.IsAlgebraic.of_finite K K⟮x⟯

Premises used: Algebra.IsAlgebraic.of_finite, Membership.mem, Subtype, IntermediateField.adjoin, IntermediateField.adjoin.finiteDimensional, Singleton.singleton
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
x : L
hx : IsIntegral K x
rw : (powerBasis hx).dim = natDegree (minpoly K x)
⊢ Module.finrank.{u, u_3} K ↥K⟮x⟯ = natDegree (minpoly K x)

Tactic:
rw [PowerBasis.finrank (adjoin.powerBasis hx :)]

Premises used: PowerBasis.finrank, IntermediateField.adjoin.powerBasis
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
x : L
hx : IsIntegral K x
⊢ (powerBasis hx).dim = natDegree (minpoly K x)

Tactic:
rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
S : Set K
hprim : Eq (α := IntermediateField F K) (adjoin F S) ⊤
rw : Eq (α := IntermediateField F K) (restrictScalars F (adjoin E S)) ⊤
rw₁ : LE.le (α := IntermediateField F K) ⊤ (restrictScalars F (adjoin E S))
rw₂ : LE.le (α := IntermediateField F K) (adjoin F S) (restrictScalars F (adjoin E S))
rw₃ : S ⊆ (↑(restrictScalars F (adjoin E S)) : Set K)
rw₄ : S ⊆ (↑(adjoin E S) : Set K)
rw₅ rw₆ : LE.le (α := IntermediateField E K) (adjoin E S) (adjoin E S)
⊢ Eq (α := IntermediateField F K) (restrictScalars F (adjoin E S)) (restrictScalars.{u_1, u, u_2} F (L' := E) ⊤)

Tactic:
rw [restrictScalars_top, ← top_le_iff, ← hprim, adjoin_le_iff,
      coe_restrictScalars, ← adjoin_le_iff]

Premises used: IntermediateField.adjoin_le_iff, IntermediateField.restrictScalars_top, IntermediateField.coe_restrictScalars, top_le_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K : IntermediateField F E
set :
  let g : E[X] := Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α);
  adjoin F (↑g.coeffs : Set E) = K
⊢ adjoin F (↑(coeffs (Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α))) : Set E) = K

Tactic:
set g := (minpoly K α).map (algebraMap K E)

Premises used: Algebra.algebraMap, Membership.mem, Subtype, minpoly, Polynomial.map
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)
set :
  let K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E);
  K' = K
⊢ adjoin F (↑g.coeffs : Set E) = K

Tactic:
set K' : IntermediateField F E := adjoin F g.coeffs

Premises used: IntermediateField, IntermediateField.adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E)
⊢ K' ≤ K

Tactic:
adjoin_le_iff.mpr fun x ↦ ?_

Premises used: Iff.mpr, Set.Mem, IntermediateField.adjoin_le_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E)
refine : ∀ x ∈ (↑g.coeffs : Set E), x ∈ (↑K : Set E)
⊢ K' ≤ K

Tactic:
refine adjoin_le_iff.mpr fun x ↦ ?_

Premises used: Iff.mpr, IntermediateField.adjoin_le_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E)
x : E
rw : (∃ n ∈ g.support, x = g.coeff n) → x ∈ (↑K : Set E)
⊢ x ∈ (↑g.coeffs : Set E) → x ∈ (↑K : Set E)

Tactic:
rw [Finset.mem_coe, mem_coeffs_iff]

Premises used: Polynomial.mem_coeffs_iff, Finset.mem_coe