awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_1
inst : Field F
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra F R
x : R
P : F[X]
hP₁ :
  Eq.{u_2 + 1} (α := ↥F[x])
    (((Minpoly.toAdjoin F x : AlgHom.{u_1, u_1, u_2} F (AdjoinRoot (minpoly F x)) ↥F[x]) :
          (a : AdjoinRoot (minpoly F x)) → ↥F[x])
        ((AdjoinRoot.mk (minpoly F x) : (a : F[X]) → AdjoinRoot (minpoly F x)) P) :
      ↥F[x])
    (0 : ↥F[x])
⊢ Eq.{u_2 + 1} (α := R) ((aeval x : (a : F[X]) → R) P : R) (0 : R)

Tactic:
simpa [← Subalgebra.coe_eq_zero, ← aeval_def] using hP₁

Premises used: Polynomial.aeval_def, Subalgebra.coe_eq_zero
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_1
inst : Field F
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra F R
x : R
⊢ Eq (α := AlgHom.{u_1, u_1, u_2} F (AdjoinRoot (minpoly F x)) ↥F[x])
    (↑(symm (adjoinSingletonEquivAdjoinRootMinpoly F x)) : AdjoinRoot (minpoly F x) →ₐ[F] ↥F[x])
    (AdjoinRoot.Minpoly.toAdjoin F x)

Tactic:
rfl

Premises used: Subsemiring.mk', AdjoinRoot, AlgEquiv.toAlgHom, Quotient.liftOn', Subsemiring.closure, Set.Mem, AddCon.liftOn, setOf, AdjoinRoot.Minpoly.toAdjoin, AdjoinRoot.liftAlgHom, Ideal.Quotient.lift, Submodule.quotientRel, AddAction.orbitRel, AdjoinRoot.lift, AddCon.Quotient, rfl
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_1
inst : Field F
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra F R
x : R
⊢ Eq (α := (a : AdjoinRoot (minpoly F x)) → ↥F[x])
    (⇑(symm (adjoinSingletonEquivAdjoinRootMinpoly F x)) : (a : AdjoinRoot (minpoly F x)) → ↥F[x])
    (⇑(AdjoinRoot.Minpoly.toAdjoin F x) : (a : AdjoinRoot (minpoly F x)) → ↥F[x])

Tactic:
rfl

Premises used: AdjoinRoot, Quotient.liftOn', Set.Mem, AddCon.liftOn, Submodule.quotientRel, AddAction.orbitRel, AddCon.Quotient, rfl
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s : Finset K
⊢ (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)

Tactic:
Finset.induction_on s (fun _ ↦ ?_) fun a s _ ih H ↦ ?_

Premises used: Finset.induction_on
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s : Finset K
refine_1 :
  (∀ (x : K), Membership.mem (γ := Finset K) ∅ x → IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑∅ : Set K))) L)
refine_2 :
  ∀ (a : K) (s : Finset K),
    a ∉ s →
      ∀
        (ih :
          (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
            Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L))
        (H : ∀ x ∈ insert a s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))),
        Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)
⊢ (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)

Tactic:
refine Finset.induction_on s (fun _ ↦ ?_) fun a s _ ih H ↦ ?_
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s : Finset K
h : ∀ (x : K), Membership.mem (γ := Finset K) ∅ x → IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
refine_1 : Nonempty (AlgHom.{u_2, u_3, u_4} F (↥⊥) L)
⊢ Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑∅ : Set K))) L)

Tactic:
rw [coe_empty, Algebra.adjoin_empty]

Premises used: Finset.coe_empty, Algebra.adjoin_empty
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s : Finset K
h : ∀ (x : K), Membership.mem (γ := Finset K) ∅ x → IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
⊢ Nonempty (AlgHom.{u_2, u_3, u_4} F (↥⊥) L)

Tactic:
⟨(Algebra.ofId F L).comp (Algebra.botEquiv F K)⟩

Premises used: AlgEquiv.toAlgHom, Nonempty.intro, Algebra.ofId, Algebra.botEquiv, AlgHom.comp
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s : Finset K
h : ∀ (x : K), Membership.mem (γ := Finset K) ∅ x → IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
⊢ Nonempty (AlgHom.{u_2, u_3, u_4} F (↥⊥) L)

Tactic:
exact ⟨(Algebra.ofId F L).comp (Algebra.botEquiv F K)⟩
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
H : ∀ x ∈ insert a s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
⊢ (IsIntegral F a ∧ Splits (map (algebraMap F L) (minpoly F a))) ∧
    ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))

Tactic:
rw [forall_mem_insert] at H

Premises used: Finset.forall_mem_insert
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
H :
  (IsIntegral F a ∧ Splits (map (algebraMap F L) (minpoly F a))) ∧
    ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
⊢ ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))

Tactic:
rcases H with ⟨⟨H1, H2⟩, H3⟩
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
H :
  (IsIntegral F a ∧ Splits (map (algebraMap F L) (minpoly F a))) ∧
    ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
H3 : ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
⊢ IsIntegral F a

Tactic:
rcases H with ⟨⟨H1, H2⟩, H3⟩
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
H :
  (IsIntegral F a ∧ Splits (map (algebraMap F L) (minpoly F a))) ∧
    ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
H3 : ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
H1 : IsIntegral F a
⊢ Splits (map (algebraMap F L) (minpoly F a))

Tactic:
rcases H with ⟨⟨H1, H2⟩, H3⟩
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
H3 : ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
refine_2 :
  ∀ (f : AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L),
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)
⊢ Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)

Tactic:
obtain ⟨f⟩ := ih H3
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
H3 : ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
f : AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L
⊢ ∀ x ∈ s, IsIntegral F x

Tactic:
choose H3 _ using H3
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
H3 : ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
f : AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L
H3₁ : ∀ x ∈ s, IsIntegral F x
⊢ ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))

Tactic:
choose H3 _ using H3
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
f : AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
refine_2 :
  Nonempty
    (AlgHom.{u_2, u_3, u_4} F
      (↥(Subalgebra.restrictScalars F (S := ↥(Algebra.adjoin F (↑s : Set K))) (↥(Algebra.adjoin F (↑s : Set K)))[a])) L)
⊢ Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)

Tactic:
rw [coe_insert, Set.insert_eq, Set.union_comm, Algebra.adjoin_union_eq_adjoin_adjoin]

Premises used: Set.insert_eq, Set.union_comm, Algebra.adjoin_union_eq_adjoin_adjoin, Finset.coe_insert
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
f : AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
refine_2 :
  let Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K);
  ∀
    (ih :
      (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
        Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L))
    (f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L),
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Subalgebra.restrictScalars F (S := ↥Ks) (↥Ks)[a])) L)
⊢ Nonempty
    (AlgHom.{u_2, u_3, u_4} F
      (↥(Subalgebra.restrictScalars F (S := ↥(Algebra.adjoin F (↑s : Set K))) (↥(Algebra.adjoin F (↑s : Set K)))[a])) L)

Tactic:
set Ks := Algebra.adjoin F (s : Set K)

Premises used: Algebra.adjoin, SetLike.coe
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K)
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) → Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L)
f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L
⊢ FiniteDimensional.{u_2, u_3} F ↥Ks

Tactic:
haveI : FiniteDimensional F Ks := ((Submodule.fg_iff_finiteDimensional _).1
      (fg_adjoin_of_finite s.finite_toSet H3)).of_subalgebra_toSubmodule
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K)
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) → Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L)
f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L
this_1 : FiniteDimensional.{u_2, u_3} F ↥Ks
this_2 : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra.{u_3, u_4} (↥Ks) L := RingHom.toAlgebra (↑f : ↥Ks →+* L)
⊢ IsIntegral (↥Ks) a

Tactic:
have H5 : IsIntegral Ks a := H1.tower_top
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K)
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) → Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L)
f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L
this_1 : FiniteDimensional.{u_2, u_3} F ↥Ks
this_2 : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra.{u_3, u_4} (↥Ks) L := RingHom.toAlgebra (↑f : ↥Ks →+* L)
H5 : IsIntegral (↥Ks) a
⊢ Splits (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a))

Tactic:
Splits.of_dvd H2 (map_ne_zero (minpoly.ne_zero H1)) ?_

Premises used: Polynomial.Splits.of_dvd, Polynomial.map_ne_zero, minpoly.ne_zero
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K)
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) → Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L)
f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L
this_1 : FiniteDimensional.{u_2, u_3} F ↥Ks
this_2 : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra.{u_3, u_4} (↥Ks) L := RingHom.toAlgebra (↑f : ↥Ks →+* L)
H5 : IsIntegral (↥Ks) a
refine :
  Dvd.dvd (α := L[X]) (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a)) (map (algebraMap F L) (minpoly F a))
⊢ Splits (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a))

Tactic:
refine Splits.of_dvd H2 (map_ne_zero (minpoly.ne_zero H1)) ?_

Premises used: Polynomial.Splits.of_dvd, Polynomial.map_ne_zero, minpoly.ne_zero
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K)
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) → Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L)
f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L
this_1 : FiniteDimensional.{u_2, u_3} F ↥Ks
this_2 : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra.{u_3, u_4} (↥Ks) L := RingHom.toAlgebra (↑f : ↥Ks →+* L)
H5 : IsIntegral (↥Ks) a
rw : Dvd.dvd (α := (↥Ks)[X]) (minpoly (↥Ks) a) (map (algebraMap F ↥Ks) (minpoly F a))
⊢ Dvd.dvd (α := L[X]) (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a)) (map (algebraMap F L) (minpoly F a))

Tactic:
rw [IsScalarTower.algebraMap_eq F Ks L, ← map_map, map_dvd_map']

Premises used: Membership.mem, Subtype, IsScalarTower.algebraMap_eq, Polynomial.map_map, Polynomial.map_dvd_map'
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K)
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) → Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L)
f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L
this_1 : FiniteDimensional.{u_2, u_3} F ↥Ks
this_2 : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra.{u_3, u_4} (↥Ks) L := RingHom.toAlgebra (↑f : ↥Ks →+* L)
H5 : IsIntegral (↥Ks) a
⊢ Dvd.dvd (α := (↥Ks)[X]) (minpoly (↥Ks) a) (map (algebraMap F ↥Ks) (minpoly F a))

Tactic:
minpoly.dvd_map_of_isScalarTower F Ks a

Premises used: Subsemiring.mk', Subsemiring.closure, Set.Mem, Membership.mem, Subtype, minpoly.dvd_map_of_isScalarTower
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K)
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) → Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L)
f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L
this_1 : FiniteDimensional.{u_2, u_3} F ↥Ks
this_2 : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra.{u_3, u_4} (↥Ks) L := RingHom.toAlgebra (↑f : ↥Ks →+* L)
H5 : IsIntegral (↥Ks) a
⊢ Dvd.dvd (α := (↥Ks)[X]) (minpoly (↥Ks) a) (map (algebraMap F ↥Ks) (minpoly F a))

Tactic:
exact minpoly.dvd_map_of_isScalarTower F Ks a

Premises used: Membership.mem, Subtype, minpoly.dvd_map_of_isScalarTower
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K)
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) → Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L)
f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L
this_1 : FiniteDimensional.{u_2, u_3} F ↥Ks
this_2 : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra.{u_3, u_4} (↥Ks) L := RingHom.toAlgebra (↑f : ↥Ks →+* L)
H5 : IsIntegral (↥Ks) a
⊢ Splits (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a))

Tactic:
have H6 : ((minpoly Ks a).map (algebraMap Ks L)).Splits := by
      refine Splits.of_dvd H2 (map_ne_zero (minpoly.ne_zero H1)) ?_
      rw [IsScalarTower.algebraMap_eq F Ks L, ← map_map, map_dvd_map']
      exact minpoly.dvd_map_of_isScalarTower F Ks a
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K)
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) → Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L)
f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L
this_1 : FiniteDimensional.{u_2, u_3} F ↥Ks
this_2 : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra.{u_3, u_4} (↥Ks) L := RingHom.toAlgebra (↑f : ↥Ks →+* L)
H5 : IsIntegral (↥Ks) a
H6 : Splits (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a))
⊢ degree (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a)) ≠ 0

Tactic:
simp [(minpoly.degree_pos H5).ne']

Premises used: minpoly.degree_pos, LT.lt.ne'
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K)
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) → Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L)
f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L
this_1 : FiniteDimensional.{u_2, u_3} F ↥Ks
this_2 : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra.{u_3, u_4} (↥Ks) L := RingHom.toAlgebra (↑f : ↥Ks →+* L)
H5 : IsIntegral (↥Ks) a
H6 : Splits (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a))
refine_2 :
  ∀ (y : L) (hy : eval y (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a)) = 0),
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Subalgebra.restrictScalars F (S := ↥Ks) (↥Ks)[a])) L)
⊢ Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Subalgebra.restrictScalars F (S := ↥Ks) (↥Ks)[a])) L)

Tactic:
obtain ⟨y, hy⟩ := H6.exists_eval_eq_zero (by simp [(minpoly.degree_pos H5).ne'])

Premises used: Polynomial.Splits.exists_eval_eq_zero
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K)
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) → Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L)
f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L
this_1 : FiniteDimensional.{u_2, u_3} F ↥Ks
this_2 : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra.{u_3, u_4} (↥Ks) L := RingHom.toAlgebra (↑f : ↥Ks →+* L)
H5 : IsIntegral (↥Ks) a
H6 : Splits (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a))
y : L
hy : eval y (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a)) = 0
⊢ eval₂ (R := ↥Ks) (algebraMap (↥Ks) L) y (minpoly (↥Ks) a) = 0

Tactic:
rw [eval_map] at hy

Premises used: Polynomial.eval_map