-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem adjoin_minpoly_coeff_of_exists_primitive_element
    [FiniteDimensional F E] (hprim : adjoin F {α} = ⊤) (K : IntermediateField F E) :
    adjoin F ((minpoly K α).map (algebraMap K E)).coeffs = K

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
dvd_g : minpoly (↥K') α ∣ g.toSubring K'.toSubring ⋯
⊢ K' = K

Tactic:
have finrank_eq : ∀ K : IntermediateField F E, finrank K E = natDegree (minpoly K α) := by
  intro K
  have := adjoin.finrank (.of_finite K α)
  erw [adjoin_eq_top_of_adjoin_eq_top F hprim, finrank_top K E] at this
  exact this

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
dvd_g : minpoly (↥K') α ∣ g.toSubring K'.toSubring ⋯
finrank_eq : ∀ (K : IntermediateField F E), finrank (↥K) E = (minpoly (↥K) α).natDegree
⊢ K' = K

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
⊢ K' = K

Tactic:
have hsub : K' ≤ K := by
  refine adjoin_le_iff.mpr fun x ↦ ?_
  rw [Finset.mem_coe, mem_coeffs_iff]
  rintro ⟨n, -, rfl⟩
  rw [coeff_map]
  apply Subtype.mem

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
⊢ K' = K

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
⊢ adjoin F ↑g.coeffs = K

Tactic:
set K' : IntermediateField F E := adjoin F g.coeffs

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
⊢ K' = K

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
⊢ K' ≤ K

Tactic:
refine adjoin_le_iff.mpr fun x ↦ ?_

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
x : E
⊢ x ∈ ↑g.coeffs → x ∈ ↑K

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
x : E
⊢ x ∈ ↑g.coeffs → x ∈ ↑K

Tactic:
rw [Finset.mem_coe, mem_coeffs_iff]

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
x : E
⊢ (∃ n ∈ g.support, x = g.coeff n) → x ∈ ↑K

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
dvd_g : minpoly (↥K') α ∣ g.toSubring K'.toSubring ⋯
finrank_eq : ∀ (K : IntermediateField F E), finrank (↥K) E = (minpoly (↥K) α).natDegree
⊢ (minpoly (↥K') α).natDegree ≤ (minpoly (↥K) α).natDegree

Tactic:
convert natDegree_le_of_dvd dvd_g
  ((g.monic_toSubring _ _).mpr <| (minpoly.monic <| .of_finite K α).map _).ne_zero using 1

Result:
case h.e'_4
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
dvd_g : minpoly (↥K') α ∣ g.toSubring K'.toSubring ⋯
finrank_eq : ∀ (K : IntermediateField F E), finrank (↥K) E = (minpoly (↥K) α).natDegree
⊢ (minpoly (↥K) α).natDegree = (g.toSubring K'.toSubring ⋯).natDegree

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
x : E
⊢ (∃ n ∈ g.support, x = g.coeff n) → x ∈ ↑K

Tactic:
rintro ⟨n, -, rfl⟩

Result:
case intro.intro
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
n : ℕ
⊢ g.coeff n ∈ ↑K

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
dvd_g : minpoly (↥K') α ∣ g.toSubring K'.toSubring ⋯
finrank_eq : ∀ (K : IntermediateField F E), finrank (↥K) E = (minpoly (↥K) α).natDegree
⊢ finrank (↥K') E ≤ finrank (↥K) E

Tactic:
simp_rw [finrank_eq]

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
dvd_g : minpoly (↥K') α ∣ g.toSubring K'.toSubring ⋯
finrank_eq : ∀ (K : IntermediateField F E), finrank (↥K) E = (minpoly (↥K) α).natDegree
⊢ (minpoly (↥K') α).natDegree ≤ (minpoly (↥K) α).natDegree

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
⊢ minpoly (↥K') α ∣ g.toSubring K'.toSubring ⋯

Tactic:
apply minpoly.dvd

Result:
case hp
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
⊢ (aeval α) (g.toSubring K'.toSubring ⋯) = 0