-- Mathlib/FieldTheory/Extension.lean
theorem exists_algHom_adjoin_of_splits_of_aeval : ∃ φ : adjoin F S →ₐ[F] K, φ ⟨x, hx⟩ = y

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)
x : E
y : K
hx : x ∈ adjoin F S
hy : (aeval y) (minpoly F x) = 0
this : Algebra.IsAlgebraic F ↥(adjoin F S)
ix : IsIntegral F ↑⟨x, hx⟩
⊢ ∃ φ, φ ⟨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)

Result:
case intro
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)
x : E
y : K
hx : x ∈ adjoin F S
hy : (aeval y) (minpoly F x) = 0
this : Algebra.IsAlgebraic F ↥(adjoin F S)
ix : IsIntegral F ↑⟨x, hx⟩
φ : ↥(adjoin F S) →ₐ[F] K
hφ : φ.comp (inclusion ⋯) = (algHomAdjoinIntegralEquiv F ix).symm ⟨y, ⋯⟩
⊢ ∃ φ, φ ⟨x, hx⟩ = y

Proof state:
case intro
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)
x : E
y : K
hx : x ∈ adjoin F S
hy : (aeval y) (minpoly F x) = 0
this : Algebra.IsAlgebraic F ↥(adjoin F S)
ix : IsIntegral F ↑⟨x, hx⟩
φ : ↥(adjoin F S) →ₐ[F] K
hφ : φ.comp (inclusion ⋯) = (algHomAdjoinIntegralEquiv F ix).symm ⟨y, ⋯⟩
⊢ ∃ φ, φ ⟨x, hx⟩ = y

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

Result:
no goals

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)
x : E
y : K
hx : x ∈ adjoin F S
hy : (aeval y) (minpoly F x) = 0
⊢ ∃ φ, φ ⟨x, hx⟩ = y

Tactic:
have := isAlgebraic_adjoin (fun s hs ↦ (hK s hs).1)

Result:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)
x : E
y : K
hx : x ∈ adjoin F S
hy : (aeval y) (minpoly F x) = 0
this : Algebra.IsAlgebraic F ↥(adjoin F S)
⊢ ∃ φ, φ ⟨x, hx⟩ = y

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)
x : E
y : K
hx : x ∈ adjoin F S
hy : (aeval y) (minpoly F x) = 0
this : Algebra.IsAlgebraic F ↥(adjoin F S)
⊢ ∃ φ, φ ⟨x, hx⟩ = y

Tactic:
have ix : IsAlgebraic F _ := Algebra.IsAlgebraic.isAlgebraic (⟨x, hx⟩ : adjoin F S)

Result:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)
x : E
y : K
hx : x ∈ adjoin F S
hy : (aeval y) (minpoly F x) = 0
this : Algebra.IsAlgebraic F ↥(adjoin F S)
ix : IsAlgebraic F ⟨x, hx⟩
⊢ ∃ φ, φ ⟨x, hx⟩ = y

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)
x : E
y : K
hx : x ∈ adjoin F S
hy : (aeval y) (minpoly F x) = 0
this : Algebra.IsAlgebraic F ↥(adjoin F S)
ix : IsAlgebraic F ⟨x, hx⟩
⊢ ∃ φ, φ ⟨x, hx⟩ = y

Tactic:
rw [isAlgebraic_iff_isIntegral, isIntegral_iff] at ix

Result:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)
x : E
y : K
hx : x ∈ adjoin F S
hy : (aeval y) (minpoly F x) = 0
this : Algebra.IsAlgebraic F ↥(adjoin F S)
ix : IsIntegral F ↑⟨x, hx⟩
⊢ ∃ φ, φ ⟨x, hx⟩ = y