no goals
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
h_sep : Separable (minpoly F α)
h_splits : Splits (algebraMap F K) (minpoly F α)
⊢ Fintype.card ({ x // x ∈ F⟮α⟯ } →ₐ[F] K) = natDegree (minpoly F α)
rw [AlgHom.card_of_powerBasis] <;>
  simp only [adjoin.powerBasis_dim, adjoin.powerBasis_gen, minpoly_gen h, h_sep, h_splits]