awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
L : IntermediateField F E
f : AlgHom.{u_1, u_2, u_3} F (↥L) K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
φ : Lifts F E K
hfφ : { carrier := L, emb := f : Lifts F E K } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this_1 : Algebra ↥{ carrier := L, emb := f : Lifts F E K }.carrier ↥φ.carrier :=
  RingHom.toAlgebra (AlgHom.toRingHom (inclusion ⋯))
this_2 : SMul ↥L ↥φ.carrier :=
  @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring { carrier := L, emb := f : Lifts F E K }.carrier)
    CommSemiring.toSemiring _
this : IsScalarTower (↥L) (↥φ.carrier) E
y : Lifts F E K
h1 : φ ≤ y
h2 : s ∈ y.carrier
⊢ s ∈ (↑(extendScalars (E := φ.carrier) ⋯) : Set E)

Tactic:
exact (hφ h1).1 h2
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
L : IntermediateField F E
f : AlgHom.{u_1, u_2, u_3} F (↥L) K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
φ : Lifts F E K
hfφ : { carrier := L, emb := f : Lifts F E K } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this_1 : Algebra ↥{ carrier := L, emb := f : Lifts F E K }.carrier ↥φ.carrier :=
  RingHom.toAlgebra (AlgHom.toRingHom (inclusion ⋯))
this_2 : SMul ↥L ↥φ.carrier :=
  @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring { carrier := L, emb := f : Lifts F E K }.carrier)
    CommSemiring.toSemiring _
this : IsScalarTower (↥L) (↥φ.carrier) E
⊢ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits

Tactic:
(hK s h).2

Premises used: And.right
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
L : IntermediateField F E
f : AlgHom.{u_1, u_2, u_3} F (↥L) K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
φ : Lifts F E K
hfφ : { carrier := L, emb := f : Lifts F E K } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this_1 : Algebra ↥{ carrier := L, emb := f : Lifts F E K }.carrier ↥φ.carrier :=
  RingHom.toAlgebra (AlgHom.toRingHom (inclusion ⋯))
this_2 : SMul ↥L ↥φ.carrier :=
  @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring { carrier := L, emb := f : Lifts F E K }.carrier)
    CommSemiring.toSemiring _
this : IsScalarTower (↥L) (↥φ.carrier) E
h₁ :
  Eq.{u_2 + 1} (α := Semiring ↥L) CommSemiring.toSemiring DivisionSemiring.toSemiring →
    φ.emb.comp (algebraMap ↥L ↥φ.carrier) = f.toRingHom
⊢ (Polynomial.map (R := ↥L) (φ.emb.comp (algebraMap ↥L ↥φ.carrier)) (minpoly (↥L) s)).Splits

Tactic:
convert! (hK s h).2

Premises used: And.right
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
L : IntermediateField F E
f : AlgHom.{u_1, u_2, u_3} F (↥L) K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
φ : Lifts F E K
hfφ : { carrier := L, emb := f : Lifts F E K } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this_1 : Algebra ↥{ carrier := L, emb := f : Lifts F E K }.carrier ↥φ.carrier :=
  RingHom.toAlgebra (AlgHom.toRingHom (inclusion ⋯))
this_2 : SMul ↥L ↥φ.carrier :=
  @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring { carrier := L, emb := f : Lifts F E K }.carrier)
    CommSemiring.toSemiring _
this : IsScalarTower (↥L) (↥φ.carrier) E
e_3 : Eq.{u_2 + 1} (α := Semiring ↥L) CommSemiring.toSemiring DivisionSemiring.toSemiring
h₁ :
  ∀ (x : ↥L),
    Eq.{u_3 + 1} (α := K) ((φ.emb.comp (algebraMap ↥L ↥φ.carrier) : (a : ↥L) → K) x : K)
      ((f.toRingHom : (a : ↥L) → K) x : K)
⊢ φ.emb.comp (algebraMap ↥L ↥φ.carrier) = f.toRingHom

Tactic:
ext
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
L : IntermediateField F E
f : AlgHom.{u_1, u_2, u_3} F (↥L) K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
φ : Lifts F E K
hfφ : { carrier := L, emb := f : Lifts F E K } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this_1 : Algebra ↥{ carrier := L, emb := f : Lifts F E K }.carrier ↥φ.carrier :=
  RingHom.toAlgebra (AlgHom.toRingHom (inclusion ⋯))
this_2 : SMul ↥L ↥φ.carrier :=
  @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring { carrier := L, emb := f : Lifts F E K }.carrier)
    CommSemiring.toSemiring _
this : IsScalarTower (↥L) (↥φ.carrier) E
e_3 : Eq.{u_2 + 1} (α := Semiring ↥L) CommSemiring.toSemiring DivisionSemiring.toSemiring
x : ↥L
⊢ Eq.{u_3 + 1} (α := K) ((φ.emb.comp (algebraMap ↥L ↥φ.carrier) : (a : ↥L) → K) x : K)
    ((f.toRingHom : (a : ↥L) → K) x : K)

Tactic:
apply hfφ.2
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
L : Type u_4
inst_5 : Field L
inst_6 : Algebra F L
inst_7 : Algebra L E
inst_8 : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits
hS : Eq (α := IntermediateField L E) (adjoin L S) ⊤
⊢ ∃ (φ : E →ₐ[F] K), AlgHom.restrictDomain L φ = f

Tactic:
have ⟨φ, hφ⟩ := exists_algHom_adjoin_of_splits' f hK
  ⟨φ.comp (((equivOfEq hS).trans topEquiv).symm.toAlgHom.restrictScalars F), hφ⟩

Premises used: AlgEquiv.toAlgHom, AlgEquiv.symm, Exists, IntermediateField.equivOfEq, AlgHom.restrictScalars, AlgEquiv.trans, IntermediateField.exists_algHom_adjoin_of_splits', Exists.intro, AlgHom.restrictDomain, AlgHom.comp, Eq, _private.0.IntermediateField.exists_algHom_of_adjoin_splits'.match_1, IntermediateField.topEquiv
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
L : Type u_4
inst_5 : Field L
inst_6 : Algebra F L
inst_7 : Algebra L E
inst_8 : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ (s : E), IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits
⊢ ∃ (φ : E →ₐ[F] K), AlgHom.restrictDomain L φ = f

Tactic:
exists_algHom_of_adjoin_splits' f (fun x _ ↦ hK x) (adjoin_univ L E)

Premises used: IntermediateField.exists_algHom_of_adjoin_splits', IntermediateField.adjoin_univ
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (Polynomial.map (algebraMap F K) (minpoly F s))
L : IntermediateField F E
f : AlgHom.{u_1, u_2, u_3} F (↥L) K
hL : L ≤ adjoin F S
obtain :
  ∀ (φ : Lifts F E K) (hfφ : { carrier := L, emb := f : Lifts F E K } ≤ φ) (hφ : IsMax φ),
    ∃ (φ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F S)) K), φ.comp (inclusion hL) = f
⊢ ∃ (φ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F S)) K), φ.comp (inclusion hL) = f

Tactic:
obtain ⟨φ, hfφ, hφ⟩ := zorn_le_nonempty_Ici₀ _
    (fun c _ hc _ _ ↦ Lifts.exists_upper_bound c hc) ⟨L, f⟩ le_rfl

Premises used: le_rfl, zorn_le_nonempty_Ici₀, IntermediateField.Lifts.exists_upper_bound, IntermediateField.Lifts.mk
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (Polynomial.map (algebraMap F K) (minpoly F s))
L : IntermediateField F E
f : AlgHom.{u_1, u_2, u_3} F (↥L) K
hL : L ≤ adjoin F S
φ : Lifts F E K
hfφ : { carrier := L, emb := f : Lifts F E K } ≤ φ
hφ : IsMax φ
⊢ ∃ (φ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F S)) K), φ.comp (inclusion hL) = f

Tactic:
⟨φ.emb.comp (inclusion <| adjoin_le_iff.mpr fun s hs ↦ ?_), ?_⟩

Premises used: Iff.mpr, IntermediateField.adjoin_le_iff, IntermediateField.Lifts.emb, Exists.intro, IntermediateField.inclusion, AlgHom.comp
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (Polynomial.map (algebraMap F K) (minpoly F s))
L : IntermediateField F E
f : AlgHom.{u_1, u_2, u_3} F (↥L) K
hL : L ≤ adjoin F S
φ : Lifts F E K
hfφ : { carrier := L, emb := f : Lifts F E K } ≤ φ
hφ : IsMax φ
refine_1 : ∀ (s : E) (hs : s ∈ S), s ∈ (↑φ.carrier : Set E)
refine_2 : AlgHom.comp (φ.emb.comp (inclusion ⋯)) (inclusion hL) = f
⊢ ∃ (φ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F S)) K), φ.comp (inclusion hL) = f

Tactic:
refine ⟨φ.emb.comp (inclusion <| adjoin_le_iff.mpr fun s hs ↦ ?_), ?_⟩
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (Polynomial.map (algebraMap F K) (minpoly F s))
L : IntermediateField F E
f : AlgHom.{u_1, u_2, u_3} F (↥L) K
hL : L ≤ adjoin F S
φ : Lifts F E K
hfφ : { carrier := L, emb := f : Lifts F E K } ≤ φ
hφ : IsMax φ
s : E
hs : s ∈ S
refine_1 : ∀ (y : Lifts F E K) (h1 : φ ≤ y) (h2 : s ∈ y.carrier), s ∈ (↑φ.carrier : Set E)
⊢ s ∈ (↑φ.carrier : Set E)

Tactic:
rcases φ.exists_lift_of_splits (hK s hs).1 (hK s hs).2 with ⟨y, h1, h2⟩

Premises used: And.right, And.left, IntermediateField.Lifts.exists_lift_of_splits
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (Polynomial.map (algebraMap F K) (minpoly F s))
L : IntermediateField F E
f : AlgHom.{u_1, u_2, u_3} F (↥L) K
hL : L ≤ adjoin F S
φ : Lifts F E K
hfφ : { carrier := L, emb := f : Lifts F E K } ≤ φ
hφ : IsMax φ
s : E
hs : s ∈ S
y : Lifts F E K
h1 : φ ≤ y
h2 : s ∈ y.carrier
⊢ s ∈ (↑φ.carrier : Set E)

Tactic:
(hφ h1).1 h2
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (Polynomial.map (algebraMap F K) (minpoly F s))
L : IntermediateField F E
f : AlgHom.{u_1, u_2, u_3} F (↥L) K
hL : L ≤ adjoin F S
φ : Lifts F E K
hfφ : { carrier := L, emb := f : Lifts F E K } ≤ φ
hφ : IsMax φ
s : E
hs : s ∈ S
y : Lifts F E K
h1 : φ ≤ y
h2 : s ∈ y.carrier
⊢ s ∈ (↑φ.carrier : Set E)

Tactic:
exact (hφ h1).1 h2
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (Polynomial.map (algebraMap F K) (minpoly F s))
L : IntermediateField F E
f : AlgHom.{u_1, u_2, u_3} F (↥L) K
hL : L ≤ adjoin F S
φ : Lifts F E K
hfφ : { carrier := L, emb := f : Lifts F E K } ≤ φ
hφ : IsMax φ
refine_2 :
  ∀ (x : ↥L),
    Eq.{u_3 + 1} (α := K) ((AlgHom.comp (φ.emb.comp (inclusion ⋯)) (inclusion hL) : (a : ↥L) → K) x : K)
      ((f : (a : ↥L) → K) x : K)
⊢ AlgHom.comp (φ.emb.comp (inclusion ⋯)) (inclusion hL) = f

Tactic:
ext
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (Polynomial.map (algebraMap F K) (minpoly F s))
L : IntermediateField F E
f : AlgHom.{u_1, u_2, u_3} F (↥L) K
hL : L ≤ adjoin F S
φ : Lifts F E K
hfφ : { carrier := L, emb := f : Lifts F E K } ≤ φ
hφ : IsMax φ
x : ↥L
⊢ Eq.{u_3 + 1} (α := K) ((AlgHom.comp (φ.emb.comp (inclusion ⋯)) (inclusion hL) : (a : ↥L) → K) x : K)
    ((f : (a : ↥L) → K) x : K)

Tactic:
apply hfφ.2
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (Polynomial.map (algebraMap F K) (minpoly F s))
⊢ Nonempty (AlgHom.{u_1, u_2, u_3} F (↥(adjoin F S)) K)

Tactic:
have ⟨φ, _⟩ := exists_algHom_adjoin_of_splits hK (⊥ : Lifts F E K).emb bot_le; ⟨φ⟩

Premises used: IntermediateField.exists_algHom_adjoin_of_splits, AlgHom, Membership.mem, Subtype, Bot.bot, Nonempty.intro, IntermediateField.Lifts.emb, IntermediateField.adjoin, Nonempty, _private.0.IntermediateField.nonempty_algHom_adjoin_of_splits.match_1, bot_le
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (Polynomial.map (algebraMap F K) (minpoly F s))
L : IntermediateField F E
f : AlgHom.{u_1, u_2, u_3} F (↥L) K
hS : Eq (α := IntermediateField F E) (adjoin F S) ⊤
⊢ ∃ (φ : E →ₐ[F] K), φ.comp L.val = f

Tactic:
have ⟨φ, hφ⟩ := exists_algHom_adjoin_of_splits hK f (hS.symm ▸ le_top)
  ⟨φ.comp ((equivOfEq hS).trans topEquiv).symm.toAlgHom, hφ⟩

Premises used: IntermediateField.exists_algHom_adjoin_of_splits, AlgEquiv.toAlgHom, AlgEquiv.symm, Exists, Eq.rec, IntermediateField.equivOfEq, AlgEquiv.trans, le_top, Exists.intro, _private.0.IntermediateField.exists_algHom_of_adjoin_splits.match_1, IntermediateField.val, AlgHom.comp, Eq.symm, Eq, IntermediateField.topEquiv
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (Polynomial.map (algebraMap F K) (minpoly F s))
hS : Eq (α := IntermediateField F E) (adjoin F S) ⊤
⊢ Nonempty (E →ₐ[F] K)

Tactic:
have ⟨φ, _⟩ := exists_algHom_of_adjoin_splits hK (⊥ : Lifts F E K).emb hS; ⟨φ⟩

Premises used: IntermediateField.exists_algHom_of_adjoin_splits, AlgHom, Bot.bot, Nonempty.intro, _private.0.IntermediateField.nonempty_algHom_of_adjoin_splits.match_1, IntermediateField.Lifts.emb, Nonempty
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (Polynomial.map (algebraMap F K) (minpoly F s))
x : E
y : K
hx : Membership.mem (γ := IntermediateField F E) (adjoin F S) x
hy : Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
⊢ Algebra.IsAlgebraic.{u_1, u_2} F ↥(adjoin F S)

Tactic:
have := isAlgebraic_adjoin (fun s hs ↦ (hK s hs).1)
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (Polynomial.map (algebraMap F K) (minpoly F s))
x : E
y : K
hx : Membership.mem (γ := IntermediateField F E) (adjoin F S) x
hy : Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
this : Algebra.IsAlgebraic.{u_1, u_2} F ↥(adjoin F S)
⊢ IsAlgebraic F (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F S) x) x hx)

Tactic:
have ix : IsAlgebraic F _ := Algebra.IsAlgebraic.isAlgebraic (⟨x, hx⟩ : adjoin F S)
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (Polynomial.map (algebraMap F K) (minpoly F s))
x : E
y : K
hx : Membership.mem (γ := IntermediateField F E) (adjoin F S) x
hy : Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
this : Algebra.IsAlgebraic.{u_1, u_2} F ↥(adjoin F S)
ix : IsAlgebraic F (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F S) x) x hx)
⊢ IsIntegral F (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F S) x) x hx) : E)

Tactic:
rw [isAlgebraic_iff_isIntegral, isIntegral_iff] at ix

Premises used: isAlgebraic_iff_isIntegral, IntermediateField.isIntegral_iff
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (Polynomial.map (algebraMap F K) (minpoly F s))
x : E
y : K
hx : Membership.mem (γ := IntermediateField F E) (adjoin F S) x
hy : Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
this : Algebra.IsAlgebraic.{u_1, u_2} F ↥(adjoin F S)
ix :
  IsIntegral F (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F S) x) x hx) : E)
obtain :
  ∀ (φ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F S)) K)
    (hφ :
      φ.comp (inclusion ⋯) =
        (Equiv.symm (algHomAdjoinIntegralEquiv F ix) :
            (a : { x_1 : K // x_1 ∈ (minpoly F (↑⟨x, hx⟩ : E)).aroots K }) → ↥F⟮(↑⟨x, hx⟩ : E)⟯ →ₐ[F] K)
          (Subtype.mk (p := fun (x_1 : K) ↦
            x_1 ∈
              aroots
                (minpoly F
                  (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F S) x) x hx) :
                    E))
                K)
            y ⋯)),
    ∃ (φ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F S)) K),
      (φ : (a : ↥(adjoin F S)) → K)
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F S) x) x hx) =
        y
⊢ ∃ (φ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F S)) K),
    (φ : (a : ↥(adjoin F S)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F S) x) x hx) =
      y

Tactic:
obtain ⟨φ, hφ⟩ := exists_algHom_adjoin_of_splits hK ((algHomAdjoinIntegralEquiv F ix).symm
    ⟨y, mem_aroots.mpr ⟨minpoly.ne_zero ix, hy⟩⟩) (adjoin_simple_le_iff.mpr hx)

Premises used: Iff.mpr, IntermediateField.exists_algHom_adjoin_of_splits, IntermediateField.adjoin_simple_le_iff, Subtype.mk, And.intro, Polynomial.mem_aroots, Equiv.symm, IntermediateField.algHomAdjoinIntegralEquiv, DFunLike.coe, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (Polynomial.map (algebraMap F K) (minpoly F s))
x : E
y : K
hx : Membership.mem (γ := IntermediateField F E) (adjoin F S) x
hy : Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
this : Algebra.IsAlgebraic.{u_1, u_2} F ↥(adjoin F S)
ix :
  IsIntegral F (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F S) x) x hx) : E)
φ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F S)) K
hφ :
  φ.comp (inclusion ⋯) =
    (Equiv.symm (algHomAdjoinIntegralEquiv F ix) :
        (a : { x_1 : K // x_1 ∈ (minpoly F (↑⟨x, hx⟩ : E)).aroots K }) → ↥F⟮(↑⟨x, hx⟩ : E)⟯ →ₐ[F] K)
      (Subtype.mk (p := fun (x_1 : K) ↦
        x_1 ∈
          aroots
            (minpoly F
              (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F S) x) x hx) : E))
            K)
        y ⋯)
⊢ ∃ (φ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F S)) K),
    (φ : (a : ↥(adjoin F S)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F S) x) x hx) =
      y

Tactic:
⟨φ, (DFunLike.congr_fun hφ <| AdjoinSimple.gen F x).trans <|
    algHomAdjoinIntegralEquiv_symm_apply_gen F ix _⟩

Premises used: DFunLike.congr_fun, IntermediateField.AdjoinSimple.gen, IntermediateField.algHomAdjoinIntegralEquiv_symm_apply_gen, Exists.intro, Eq.trans
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (Polynomial.map (algebraMap F K) (minpoly F s))
x : E
y : K
hx : Membership.mem (γ := IntermediateField F E) (adjoin F S) x
hy : Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
this : Algebra.IsAlgebraic.{u_1, u_2} F ↥(adjoin F S)
ix :
  IsIntegral F (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F S) x) x hx) : E)
φ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F S)) K
hφ :
  φ.comp (inclusion ⋯) =
    (Equiv.symm (algHomAdjoinIntegralEquiv F ix) :
        (a : { x_1 : K // x_1 ∈ (minpoly F (↑⟨x, hx⟩ : E)).aroots K }) → ↥F⟮(↑⟨x, hx⟩ : E)⟯ →ₐ[F] K)
      (Subtype.mk (p := fun (x_1 : K) ↦
        x_1 ∈
          aroots
            (minpoly F
              (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F S) x) x hx) : E))
            K)
        y ⋯)
⊢ ∃ (φ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F S)) K),
    (φ : (a : ↥(adjoin F S)) → K)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F S) x) x hx) =
      y

Tactic:
exact ⟨φ, (DFunLike.congr_fun hφ <| AdjoinSimple.gen F x).trans <|
    algHomAdjoinIntegralEquiv_symm_apply_gen F ix _⟩
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (Polynomial.map (algebraMap F K) (minpoly F s))
x : E
y : K
hS : Eq (α := IntermediateField F E) (adjoin F S) ⊤
hy : Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
⊢ ∃ (φ : E →ₐ[F] K), (φ : (a : E) → K) x = y

Tactic:
have ⟨φ, hφ⟩ := exists_algHom_adjoin_of_splits_of_aeval hK (hS ▸ mem_top) hy
  ⟨φ.comp ((equivOfEq hS).trans topEquiv).symm.toAlgHom, hφ⟩

Premises used: AlgEquiv.toAlgHom, AlgEquiv.symm, _private.0.IntermediateField.exists_algHom_of_adjoin_splits_of_aeval.match_1, Exists, IntermediateField.exists_algHom_adjoin_of_splits_of_aeval, IntermediateField.equivOfEq, AlgEquiv.trans, Exists.intro, AlgHom.comp, Eq, DFunLike.coe, IntermediateField.topEquiv
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
hK' : ∀ (s : E), IsIntegral F s ∧ Splits (Polynomial.map (algebraMap F K) (minpoly F s))
L : IntermediateField F E
f : AlgHom.{u_1, u_2, u_3} F (↥L) K
⊢ ∃ (φ : E →ₐ[F] K), φ.comp L.val = f

Tactic:
exists_algHom_of_adjoin_splits (fun x _ ↦ hK' x) f (adjoin_univ F E)

Premises used: IntermediateField.exists_algHom_of_adjoin_splits, IntermediateField.adjoin_univ
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
hK' : ∀ (s : E), IsIntegral F s ∧ Splits (Polynomial.map (algebraMap F K) (minpoly F s))
⊢ Nonempty (E →ₐ[F] K)

Tactic:
nonempty_algHom_of_adjoin_splits (fun x _ ↦ hK' x) (adjoin_univ F E)

Premises used: IntermediateField.adjoin_univ, IntermediateField.nonempty_algHom_of_adjoin_splits
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
hK' : ∀ (s : E), IsIntegral F s ∧ Splits (Polynomial.map (algebraMap F K) (minpoly F s))
x : E
y : K
hy : Eq.{u_3 + 1} (α := K) ((aeval y : (a : F[X]) → K) (minpoly F x) : K) (0 : K)
⊢ ∃ (φ : E →ₐ[F] K), (φ : (a : E) → K) x = y

Tactic:
exists_algHom_of_adjoin_splits_of_aeval (fun x _ ↦ hK' x) (adjoin_univ F E) hy

Premises used: IntermediateField.exists_algHom_of_adjoin_splits_of_aeval, IntermediateField.adjoin_univ
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F L
inst_4 : Algebra F K
hA : ∀ (x : K), Splits (map (algebraMap F L) (minpoly F x))
inst_5 : Algebra.IsAlgebraic F K
x : K
h :
  ∀ (a : L),
    Membership.mem (γ := Set L) (Set.range fun (ψ : K →ₐ[F] L) ↦ (ψ : (a : K) → L) x) a ↔ a ∈ rootSet (minpoly F x) L
⊢ (Set.range fun (ψ : K →ₐ[F] L) ↦ (ψ : (a : K) → L) x) = rootSet (minpoly F x) L

Tactic:
ext a