F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α✝ : E
K : Type ?u.813260
inst✝¹ : Field K
inst✝ : Algebra F K
α : E
h : IsIntegral F (↑(algebraMap { x // x ∈ F⟮α⟯ } E) (AdjoinSimple.gen F α))
⊢ minpoly F (AdjoinSimple.gen F α) = minpoly F α
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α✝ : E
K : Type ?u.813260
inst✝¹ : Field K
inst✝ : Algebra F K
α : E
h : IsIntegral F α
⊢ minpoly F (AdjoinSimple.gen F α) = minpoly F α
rw [← AdjoinSimple.algebraMap_gen F α] at h
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α✝ : E
K : Type ?u.813260
inst✝¹ : Field K
inst✝ : Algebra F K
α : E
h : IsIntegral F (↑(algebraMap { x // x ∈ F⟮α⟯ } E) (AdjoinSimple.gen F α))
inj : Function.Injective ↑(algebraMap { x // x ∈ F⟮α⟯ } E)
⊢ minpoly F (AdjoinSimple.gen F α) = minpoly F α
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α✝ : E
K : Type ?u.813260
inst✝¹ : Field K
inst✝ : Algebra F K
α : E
h : IsIntegral F (↑(algebraMap { x // x ∈ F⟮α⟯ } E) (AdjoinSimple.gen F α))
⊢ minpoly F (AdjoinSimple.gen F α) = minpoly F α
have inj := (algebraMap F⟮α⟯ E).injective
no goals
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α✝ : E
K : Type ?u.813260
inst✝¹ : Field K
inst✝ : Algebra F K
α : E
h : IsIntegral F (↑(algebraMap { x // x ∈ F⟮α⟯ } E) (AdjoinSimple.gen F α))
inj : Function.Injective ↑(algebraMap { x // x ∈ F⟮α⟯ } E)
⊢ minpoly F (AdjoinSimple.gen F α) = minpoly F α
exact
  minpoly.eq_of_algebraMap_eq inj ((isIntegral_algebraMap_iff inj).mp h)
    (AdjoinSimple.algebraMap_gen _ _).symm