[GOAL]
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
⊢ { x_1 // x_1 ∈ Algebra.adjoin F {x} } ≃ₐ[F] AdjoinRoot (minpoly F x)
[PROOFSTEP]
refine AlgEquiv.symm ?_
[GOAL]
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
⊢ AdjoinRoot (minpoly F x) ≃ₐ[F] { x_1 // x_1 ∈ Algebra.adjoin F {x} }
[PROOFSTEP]
refine AlgEquiv.ofBijective (AlgHom.codRestrict (AdjoinRoot.liftHom _ x <| minpoly.aeval F x) _ fun p => ?_) ⟨?_, ?_⟩
[GOAL]
case refine_1
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
p : AdjoinRoot (minpoly F x)
⊢ ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) p ∈ Algebra.adjoin F {x}
[PROOFSTEP]
induction p using AdjoinRoot.induction_on with
| ih p => exact (Algebra.adjoin_singleton_eq_range_aeval F x).symm ▸ (Polynomial.aeval _).mem_range.mpr ⟨p, rfl⟩
[GOAL]
case refine_1
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
p : AdjoinRoot (minpoly F x)
⊢ ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) p ∈ Algebra.adjoin F {x}
[PROOFSTEP]
induction p using AdjoinRoot.induction_on with
| ih p => exact (Algebra.adjoin_singleton_eq_range_aeval F x).symm ▸ (Polynomial.aeval _).mem_range.mpr ⟨p, rfl⟩
[GOAL]
case refine_1.ih
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
p : F[X]
⊢ ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) (↑(AdjoinRoot.mk (minpoly F x)) p) ∈
    Algebra.adjoin F {x}
[PROOFSTEP]

| ih p => exact (Algebra.adjoin_singleton_eq_range_aeval F x).symm ▸ (Polynomial.aeval _).mem_range.mpr ⟨p, rfl⟩
[GOAL]
case refine_1.ih
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
p : F[X]
⊢ ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) (↑(AdjoinRoot.mk (minpoly F x)) p) ∈
    Algebra.adjoin F {x}
[PROOFSTEP]
exact (Algebra.adjoin_singleton_eq_range_aeval F x).symm ▸ (Polynomial.aeval _).mem_range.mpr ⟨p, rfl⟩
[GOAL]
case refine_2
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
⊢ Function.Injective
    ↑(AlgHom.codRestrict (AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) (Algebra.adjoin F {x})
        (_ :
          ∀ (p : AdjoinRoot (minpoly F x)),
            ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) p ∈ Algebra.adjoin F {x}))
[PROOFSTEP]
apply (AlgHom.injective_codRestrict _ _ _).2
[GOAL]
case refine_2
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
⊢ Function.Injective ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0))
[PROOFSTEP]
apply (injective_iff_map_eq_zero _).2
[GOAL]
case refine_2
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
⊢ ∀ (a : AdjoinRoot (minpoly F x)),
    ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) a = 0 → a = 0
[PROOFSTEP]
intro p
[GOAL]
case refine_2
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
p : AdjoinRoot (minpoly F x)
⊢ ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) p = 0 → p = 0
[PROOFSTEP]
induction p using AdjoinRoot.induction_on with
| ih p =>
  intro hp
  apply Ideal.Quotient.eq_zero_iff_mem.2
  apply Ideal.mem_span_singleton.2
  apply minpoly.dvd F x hp
[GOAL]
case refine_2
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
p : AdjoinRoot (minpoly F x)
⊢ ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) p = 0 → p = 0
[PROOFSTEP]
induction p using AdjoinRoot.induction_on with
| ih p =>
  intro hp
  apply Ideal.Quotient.eq_zero_iff_mem.2
  apply Ideal.mem_span_singleton.2
  apply minpoly.dvd F x hp
[GOAL]
case refine_2.ih
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
p : F[X]
⊢ ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) (↑(AdjoinRoot.mk (minpoly F x)) p) = 0 →
    ↑(AdjoinRoot.mk (minpoly F x)) p = 0
[PROOFSTEP]

| ih p =>
  intro hp
  apply Ideal.Quotient.eq_zero_iff_mem.2
  apply Ideal.mem_span_singleton.2
  apply minpoly.dvd F x hp
[GOAL]
case refine_2.ih
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
p : F[X]
⊢ ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) (↑(AdjoinRoot.mk (minpoly F x)) p) = 0 →
    ↑(AdjoinRoot.mk (minpoly F x)) p = 0
[PROOFSTEP]
intro hp
[GOAL]
case refine_2.ih
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
p : F[X]
hp : ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) (↑(AdjoinRoot.mk (minpoly F x)) p) = 0
⊢ ↑(AdjoinRoot.mk (minpoly F x)) p = 0
[PROOFSTEP]
apply Ideal.Quotient.eq_zero_iff_mem.2
[GOAL]
case refine_2.ih
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
p : F[X]
hp : ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) (↑(AdjoinRoot.mk (minpoly F x)) p) = 0
⊢ p ∈ Ideal.span {minpoly F x}
[PROOFSTEP]
apply Ideal.mem_span_singleton.2
[GOAL]
case refine_2.ih
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
p : F[X]
hp : ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) (↑(AdjoinRoot.mk (minpoly F x)) p) = 0
⊢ minpoly F x ∣ p
[PROOFSTEP]
apply minpoly.dvd F x hp
[GOAL]
case refine_3
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
⊢ Function.Surjective
    ↑(AlgHom.codRestrict (AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) (Algebra.adjoin F {x})
        (_ :
          ∀ (p : AdjoinRoot (minpoly F x)),
            ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) p ∈ Algebra.adjoin F {x}))
[PROOFSTEP]
intro y
[GOAL]
case refine_3
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
y : { x_1 // x_1 ∈ Algebra.adjoin F {x} }
⊢ ∃ a,
    ↑(AlgHom.codRestrict (AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) (Algebra.adjoin F {x})
            (_ :
              ∀ (p : AdjoinRoot (minpoly F x)),
                ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) p ∈ Algebra.adjoin F {x}))
        a =
      y
[PROOFSTEP]
let ⟨p, hp⟩ := (SetLike.ext_iff.1 (Algebra.adjoin_singleton_eq_range_aeval F x) (y : R)).1 y.2
[GOAL]
case refine_3
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
y : { x_1 // x_1 ∈ Algebra.adjoin F {x} }
p : F[X]
hp : ↑↑(aeval x) p = ↑y
⊢ ∃ a,
    ↑(AlgHom.codRestrict (AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) (Algebra.adjoin F {x})
            (_ :
              ∀ (p : AdjoinRoot (minpoly F x)),
                ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) p ∈ Algebra.adjoin F {x}))
        a =
      y
[PROOFSTEP]
exact ⟨AdjoinRoot.mk _ p, Subtype.eq hp⟩
[GOAL]
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
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)
[PROOFSTEP]
classical
refine' Finset.induction_on s (fun _ => _) fun a s _ ih H => _
· rw [coe_empty, Algebra.adjoin_empty]
  exact ⟨(Algebra.ofId F L).comp (Algebra.botEquiv F K)⟩
rw [forall_mem_insert] at H 
rcases H with ⟨⟨H1, H2⟩, H3⟩
cases' ih H3 with f
choose H3 _ using H3
rw [coe_insert, Set.insert_eq, Set.union_comm, Algebra.adjoin_union_eq_adjoin_adjoin]
letI := (f : Algebra.adjoin F (↑s : Set K) →+* L).toAlgebra
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
letI := fieldOfFiniteDimensional F (Algebra.adjoin F (↑s : Set K))
have H5 : IsIntegral (Algebra.adjoin F (s : Set K)) a := isIntegral_of_isScalarTower H1
have H6 : (minpoly (Algebra.adjoin F (s : Set K)) a).Splits (algebraMap (Algebra.adjoin F (s : Set K)) L) :=
  by
  have : Polynomial.map (algebraMap F (Algebra.adjoin F (s : Set K))) (minpoly F a) ≠ 0 :=
    Polynomial.map_ne_zero <| minpoly.ne_zero H1
  refine' Polynomial.splits_of_splits_of_dvd _ this ((Polynomial.splits_map_iff _ _).2 _) (minpoly.dvd _ _ _)
  · rw [← IsScalarTower.algebraMap_eq]
    exact H2
  · rw [Polynomial.aeval_map_algebraMap, minpoly.aeval]
obtain ⟨y, hy⟩ := Polynomial.exists_root_of_splits _ H6 (ne_of_lt (minpoly.degree_pos H5)).symm
refine' ⟨Subalgebra.ofRestrictScalars F _ _⟩
refine' (AdjoinRoot.liftHom (minpoly (Algebra.adjoin F (↑s : Set K)) a) y hy).comp _
exact (AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly (Algebra.adjoin F (↑s : Set K)) a).toAlgHom
[GOAL]
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
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)
[PROOFSTEP]
refine' Finset.induction_on s (fun _ => _) fun a s _ ih H => _
[GOAL]
case refine'_1
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
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)
[PROOFSTEP]
rw [coe_empty, Algebra.adjoin_empty]
[GOAL]
case refine'_1
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
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)
[PROOFSTEP]
exact ⟨(Algebra.ofId F L).comp (Algebra.botEquiv F K)⟩
[GOAL]
case refine'_2
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
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)
[PROOFSTEP]
rw [forall_mem_insert] at H 
[GOAL]
case refine'_2
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
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)
[PROOFSTEP]
rcases H with ⟨⟨H1, H2⟩, H3⟩
[GOAL]
case refine'_2.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
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)
[PROOFSTEP]
cases' ih H3 with f
[GOAL]
case refine'_2.intro.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
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)
[PROOFSTEP]
choose H3 _ using H3
[GOAL]
case refine'_2.intro.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
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)
[PROOFSTEP]
rw [coe_insert, Set.insert_eq, Set.union_comm, Algebra.adjoin_union_eq_adjoin_adjoin]
[GOAL]
case refine'_2.intro.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
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)
[PROOFSTEP]
letI := (f : Algebra.adjoin F (↑s : Set K) →+* L).toAlgebra
[GOAL]
case refine'_2.intro.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
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)
[PROOFSTEP]
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
[GOAL]
case refine'_2.intro.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
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)
[PROOFSTEP]
letI := fieldOfFiniteDimensional F (Algebra.adjoin F (↑s : Set K))
[GOAL]
case refine'_2.intro.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
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)
[PROOFSTEP]
have H5 : IsIntegral (Algebra.adjoin F (s : Set K)) a := isIntegral_of_isScalarTower H1
[GOAL]
case refine'_2.intro.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
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)
[PROOFSTEP]
have H6 : (minpoly (Algebra.adjoin F (s : Set K)) a).Splits (algebraMap (Algebra.adjoin F (s : Set K)) L) :=
  by
  have : Polynomial.map (algebraMap F (Algebra.adjoin F (s : Set K))) (minpoly F a) ≠ 0 :=
    Polynomial.map_ne_zero <| minpoly.ne_zero H1
  refine' Polynomial.splits_of_splits_of_dvd _ this ((Polynomial.splits_map_iff _ _).2 _) (minpoly.dvd _ _ _)
  · rw [← IsScalarTower.algebraMap_eq]
    exact H2
  · rw [Polynomial.aeval_map_algebraMap, minpoly.aeval]
[GOAL]
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
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)
[PROOFSTEP]
have : Polynomial.map (algebraMap F (Algebra.adjoin F (s : Set K))) (minpoly F a) ≠ 0 :=
  Polynomial.map_ne_zero <| minpoly.ne_zero H1
[GOAL]
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
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)
[PROOFSTEP]
refine' Polynomial.splits_of_splits_of_dvd _ this ((Polynomial.splits_map_iff _ _).2 _) (minpoly.dvd _ _ _)
[GOAL]
case refine'_1
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
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)
[PROOFSTEP]
rw [← IsScalarTower.algebraMap_eq]
[GOAL]
case refine'_1
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
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)
[PROOFSTEP]
exact H2
[GOAL]
case refine'_2
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
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
[PROOFSTEP]
rw [Polynomial.aeval_map_algebraMap, minpoly.aeval]
[GOAL]
case refine'_2.intro.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
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)
[PROOFSTEP]
obtain ⟨y, hy⟩ := Polynomial.exists_root_of_splits _ H6 (ne_of_lt (minpoly.degree_pos H5)).symm
[GOAL]
case refine'_2.intro.intro.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
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)
[PROOFSTEP]
refine' ⟨Subalgebra.ofRestrictScalars F _ _⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
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
[PROOFSTEP]
refine' (AdjoinRoot.liftHom (minpoly (Algebra.adjoin F (↑s : Set K)) a) y hy).comp _
[GOAL]
case refine'_2.intro.intro.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
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)
[PROOFSTEP]
exact (AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly (Algebra.adjoin F (↑s : Set K)) a).toAlgHom
