case a
F : Type u_2
inst✝⁴ : Field F
E : Type u_1
inst✝³ : Field E
inst✝² : Algebra F E
α✝ : E
K : Type ?u.817326
inst✝¹ : Field K
inst✝ : Algebra F K
α : E
⊢ ↑(↑(aeval (AdjoinSimple.gen F α)) (minpoly F α)) = ↑0
F : Type u_2
inst✝⁴ : Field F
E : Type u_1
inst✝³ : Field E
inst✝² : Algebra F E
α✝ : E
K : Type ?u.817326
inst✝¹ : Field K
inst✝ : Algebra F K
α : E
⊢ ↑(aeval (AdjoinSimple.gen F α)) (minpoly F α) = 0
ext
case h.e'_2
F : Type u_2
inst✝⁴ : Field F
E : Type u_1
inst✝³ : Field E
inst✝² : Algebra F E
α✝ : E
K : Type ?u.817326
inst✝¹ : Field K
inst✝ : Algebra F K
α : E
⊢ ↑(↑(aeval (AdjoinSimple.gen F α)) (minpoly F α)) = ↑(aeval α) (minpoly F α)
case a
F : Type u_2
inst✝⁴ : Field F
E : Type u_1
inst✝³ : Field E
inst✝² : Algebra F E
α✝ : E
K : Type ?u.817326
inst✝¹ : Field K
inst✝ : Algebra F K
α : E
⊢ ↑(↑(aeval (AdjoinSimple.gen F α)) (minpoly F α)) = ↑0
convert minpoly.aeval F α
case h.e'_2
F : Type u_2
inst✝⁴ : Field F
E : Type u_1
inst✝³ : Field E
inst✝² : Algebra F E
α✝ : E
K : Type ?u.817326
inst✝¹ : Field K
inst✝ : Algebra F K
α : E
⊢ ↑(↑(aeval (AdjoinSimple.gen F α)) (minpoly F α)) =
    ↑(aeval (↑(algebraMap { x // x ∈ F⟮α⟯ } E) (AdjoinSimple.gen F α))) (minpoly F α)
case h.e'_2
F : Type u_2
inst✝⁴ : Field F
E : Type u_1
inst✝³ : Field E
inst✝² : Algebra F E
α✝ : E
K : Type ?u.817326
inst✝¹ : Field K
inst✝ : Algebra F K
α : E
⊢ ↑(↑(aeval (AdjoinSimple.gen F α)) (minpoly F α)) = ↑(aeval α) (minpoly F α)
conv in aeval α => rw [← AdjoinSimple.algebraMap_gen F α]
no goals
case h.e'_2
F : Type u_2
inst✝⁴ : Field F
E : Type u_1
inst✝³ : Field E
inst✝² : Algebra F E
α✝ : E
K : Type ?u.817326
inst✝¹ : Field K
inst✝ : Algebra F K
α : E
⊢ ↑(↑(aeval (AdjoinSimple.gen F α)) (minpoly F α)) =
    ↑(aeval (↑(algebraMap { x // x ∈ F⟮α⟯ } E) (AdjoinSimple.gen F α))) (minpoly F α)
exact (aeval_algebraMap_apply E (AdjoinSimple.gen F α) _).symm