case refine'_1
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s : Finset K
x✝ : ∀ (x : K), x ∈ ∅ → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty ({ x // x ∈ Algebra.adjoin F ↑∅ } →ₐ[F] L)

case refine'_2
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H : ∀ (x : K), x ∈ insert a s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty ({ x // x ∈ Algebra.adjoin F ↑(insert a s) } →ₐ[F] L)
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s : Finset K
⊢ (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
refine' Finset.induction_on s (fun _ => _) fun a s _ ih H => _
case refine'_2
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H :
  (IsIntegral F a ∧ Splits (algebraMap F L) (minpoly F a)) ∧
    ∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty ({ x // x ∈ Algebra.adjoin F ↑(insert a s) } →ₐ[F] L)
case refine'_2
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H : ∀ (x : K), x ∈ insert a s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty ({ x // x ∈ Algebra.adjoin F ↑(insert a s) } →ₐ[F] L)
rw [forall_mem_insert] at H
case refine'_2.intro.intro
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H3 : ∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
⊢ Nonempty ({ x // x ∈ Algebra.adjoin F ↑(insert a s) } →ₐ[F] L)
case refine'_2
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H :
  (IsIntegral F a ∧ Splits (algebraMap F L) (minpoly F a)) ∧
    ∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty ({ x // x ∈ Algebra.adjoin F ↑(insert a s) } →ₐ[F] L)
rcases H with ⟨⟨H1, H2⟩, H3⟩
case refine'_2.intro.intro.intro
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H3 : ∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
⊢ Nonempty ({ x // x ∈ Algebra.adjoin F ↑(insert a s) } →ₐ[F] L)
case refine'_2.intro.intro
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H3 : ∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
⊢ Nonempty ({ x // x ∈ Algebra.adjoin F ↑(insert a s) } →ₐ[F] L)
cases' ih H3 with f
case refine'_2.intro.intro.intro
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty ({ x // x ∈ Algebra.adjoin F ↑(insert a s) } →ₐ[F] L)
case refine'_2.intro.intro.intro
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H3 : ∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
⊢ Nonempty ({ x // x ∈ Algebra.adjoin F ↑(insert a s) } →ₐ[F] L)
choose H3 _ using H3
case refine'_2.intro.intro.intro
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty ({ x // x ∈ Subalgebra.restrictScalars F (Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a}) } →ₐ[F] L)
case refine'_2.intro.intro.intro
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty ({ x // x ∈ Algebra.adjoin F ↑(insert a s) } →ₐ[F] L)
rw [coe_insert, Set.insert_eq, Set.union_comm, Algebra.adjoin_union_eq_adjoin_adjoin]
case refine'_2.intro.intro.intro
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
⊢ Nonempty ({ x // x ∈ Subalgebra.restrictScalars F (Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a}) } →ₐ[F] L)
case refine'_2.intro.intro.intro
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty ({ x // x ∈ Subalgebra.restrictScalars F (Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a}) } →ₐ[F] L)
letI := (f : Algebra.adjoin F (↑s : Set K) →+* L).toAlgebra
case refine'_2.intro.intro.intro
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝ : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
⊢ Nonempty ({ x // x ∈ Subalgebra.restrictScalars F (Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a}) } →ₐ[F] L)
case refine'_2.intro.intro.intro
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
⊢ Nonempty ({ x // x ∈ Subalgebra.restrictScalars F (Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a}) } →ₐ[F] L)
haveI : FiniteDimensional F (Algebra.adjoin F (↑s : Set K)) :=
  ((Submodule.fg_iff_finiteDimensional _).1
    (FG_adjoin_of_finite s.finite_toSet H3)).of_subalgebra_toSubmodule
case refine'_2.intro.intro.intro
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝¹ : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
⊢ Nonempty ({ x // x ∈ Subalgebra.restrictScalars F (Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a}) } →ₐ[F] L)
case refine'_2.intro.intro.intro
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝ : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
⊢ Nonempty ({ x // x ∈ Subalgebra.restrictScalars F (Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a}) } →ₐ[F] L)
letI := fieldOfFiniteDimensional F (Algebra.adjoin F (↑s : Set K))
case refine'_2.intro.intro.intro
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝¹ : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
⊢ Nonempty ({ x // x ∈ Subalgebra.restrictScalars F (Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a}) } →ₐ[F] L)
case refine'_2.intro.intro.intro
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝¹ : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
⊢ Nonempty ({ x // x ∈ Subalgebra.restrictScalars F (Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a}) } →ₐ[F] L)
have H5 : IsIntegral (Algebra.adjoin F (s : Set K)) a := isIntegral_of_isScalarTower H1
case refine'_2.intro.intro.intro.intro
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝¹ : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
H6 : Splits (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) (minpoly { x // x ∈ Algebra.adjoin F ↑s } a)
y : L
hy : eval₂ (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) y (minpoly { x // x ∈ Algebra.adjoin F ↑s } a) = 0
⊢ Nonempty ({ x // x ∈ Subalgebra.restrictScalars F (Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a}) } →ₐ[F] L)
case refine'_2.intro.intro.intro
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝¹ : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
H6 : Splits (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) (minpoly { x // x ∈ Algebra.adjoin F ↑s } a)
⊢ Nonempty ({ x // x ∈ Subalgebra.restrictScalars F (Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a}) } →ₐ[F] L)
obtain ⟨y, hy⟩ := Polynomial.exists_root_of_splits _ H6 (ne_of_lt (minpoly.degree_pos H5)).symm
case refine'_2.intro.intro.intro.intro
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝¹ : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
H6 : Splits (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) (minpoly { x // x ∈ Algebra.adjoin F ↑s } a)
y : L
hy : eval₂ (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) y (minpoly { x // x ∈ Algebra.adjoin F ↑s } a) = 0
⊢ { x // x ∈ Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a} } →ₐ[{ x // x ∈ Algebra.adjoin F ↑s }] L
case refine'_2.intro.intro.intro.intro
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝¹ : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
H6 : Splits (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) (minpoly { x // x ∈ Algebra.adjoin F ↑s } a)
y : L
hy : eval₂ (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) y (minpoly { x // x ∈ Algebra.adjoin F ↑s } a) = 0
⊢ Nonempty ({ x // x ∈ Subalgebra.restrictScalars F (Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a}) } →ₐ[F] L)
refine' ⟨Subalgebra.ofRestrictScalars F _ _⟩
case refine'_2.intro.intro.intro.intro
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝¹ : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
H6 : Splits (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) (minpoly { x // x ∈ Algebra.adjoin F ↑s } a)
y : L
hy : eval₂ (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) y (minpoly { x // x ∈ Algebra.adjoin F ↑s } a) = 0
⊢ { x // x ∈ Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a} } →ₐ[{ x // x ∈ Algebra.adjoin F ↑s }]
    AdjoinRoot (minpoly { x // x ∈ Algebra.adjoin F ↑s } a)
case refine'_2.intro.intro.intro.intro
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝¹ : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
H6 : Splits (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) (minpoly { x // x ∈ Algebra.adjoin F ↑s } a)
y : L
hy : eval₂ (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) y (minpoly { x // x ∈ Algebra.adjoin F ↑s } a) = 0
⊢ { x // x ∈ Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a} } →ₐ[{ x // x ∈ Algebra.adjoin F ↑s }] L
refine' (AdjoinRoot.liftHom (minpoly (Algebra.adjoin F (↑s : Set K)) a) y hy).comp _
no goals
case refine'_2.intro.intro.intro.intro
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝¹ : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
H6 : Splits (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) (minpoly { x // x ∈ Algebra.adjoin F ↑s } a)
y : L
hy : eval₂ (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) y (minpoly { x // x ∈ Algebra.adjoin F ↑s } a) = 0
⊢ { x // x ∈ Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a} } →ₐ[{ x // x ∈ Algebra.adjoin F ↑s }]
    AdjoinRoot (minpoly { x // x ∈ Algebra.adjoin F ↑s } a)
exact (AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly
  (Algebra.adjoin F (↑s : Set K)) a).toAlgHom
case refine'_1
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s : Finset K
x✝ : ∀ (x : K), x ∈ ∅ → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty ({ x // x ∈ ⊥ } →ₐ[F] L)
case refine'_1
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s : Finset K
x✝ : ∀ (x : K), x ∈ ∅ → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty ({ x // x ∈ Algebra.adjoin F ↑∅ } →ₐ[F] L)
rw [coe_empty, Algebra.adjoin_empty]
no goals
case refine'_1
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s : Finset K
x✝ : ∀ (x : K), x ∈ ∅ → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty ({ x // x ∈ ⊥ } →ₐ[F] L)
exact ⟨(Algebra.ofId F L).comp (Algebra.botEquiv F K)⟩
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝² : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝¹ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this✝ : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
this : Polynomial.map (algebraMap F { x // x ∈ Algebra.adjoin F ↑s }) (minpoly F a) ≠ 0
⊢ Splits (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) (minpoly { x // x ∈ Algebra.adjoin F ↑s } a)
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝¹ : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
⊢ Splits (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) (minpoly { x // x ∈ Algebra.adjoin F ↑s } a)
have : Polynomial.map (algebraMap F (Algebra.adjoin F (s : Set K))) (minpoly F a) ≠ 0 :=
  Polynomial.map_ne_zero <| minpoly.ne_zero H1
case refine'_1
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝² : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝¹ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this✝ : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
this : Polynomial.map (algebraMap F { x // x ∈ Algebra.adjoin F ↑s }) (minpoly F a) ≠ 0
⊢ Splits (RingHom.comp (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) (algebraMap F { x // x ∈ Algebra.adjoin F ↑s }))
    (minpoly F a)

case refine'_2
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝² : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝¹ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this✝ : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
this : Polynomial.map (algebraMap F { x // x ∈ Algebra.adjoin F ↑s }) (minpoly F a) ≠ 0
⊢ ↑(aeval a) (Polynomial.map (algebraMap F { x // x ∈ Algebra.adjoin F ↑s }) (minpoly F a)) = 0
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝² : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝¹ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this✝ : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
this : Polynomial.map (algebraMap F { x // x ∈ Algebra.adjoin F ↑s }) (minpoly F a) ≠ 0
⊢ Splits (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) (minpoly { x // x ∈ Algebra.adjoin F ↑s } a)
refine' Polynomial.splits_of_splits_of_dvd _ this
  ((Polynomial.splits_map_iff _ _).2 _) (minpoly.dvd _ _ _)
case refine'_1
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝² : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝¹ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this✝ : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
this : Polynomial.map (algebraMap F { x // x ∈ Algebra.adjoin F ↑s }) (minpoly F a) ≠ 0
⊢ Splits (algebraMap F L) (minpoly F a)
case refine'_1
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝² : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝¹ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this✝ : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
this : Polynomial.map (algebraMap F { x // x ∈ Algebra.adjoin F ↑s }) (minpoly F a) ≠ 0
⊢ Splits (RingHom.comp (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) (algebraMap F { x // x ∈ Algebra.adjoin F ↑s }))
    (minpoly F a)
rw [← IsScalarTower.algebraMap_eq]
no goals
case refine'_1
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝² : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝¹ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this✝ : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
this : Polynomial.map (algebraMap F { x // x ∈ Algebra.adjoin F ↑s }) (minpoly F a) ≠ 0
⊢ Splits (algebraMap F L) (minpoly F a)
exact H2
no goals
case refine'_2
F✝ : Type ?u.30572
inst✝⁵ : Field F✝
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝² : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝¹ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this✝ : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
this : Polynomial.map (algebraMap F { x // x ∈ Algebra.adjoin F ↑s }) (minpoly F a) ≠ 0
⊢ ↑(aeval a) (Polynomial.map (algebraMap F { x // x ∈ Algebra.adjoin F ↑s }) (minpoly F a)) = 0
rw [Polynomial.aeval_map_algebraMap, minpoly.aeval]