-- Mathlib/FieldTheory/PrimitiveElement.lean
theorem finite_intermediateField_of_exists_primitive_element [Algebra.IsAlgebraic F E]
    (h : ∃ α : E, F⟮α⟯ = ⊤) : Finite (IntermediateField F E)

Proof state:
case intro
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : F⟮α⟯ = ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
⊢ Finite (IntermediateField F E)

Tactic:
have hfin : Finite G := @Finite.of_fintype _ <| fintypeSubtypeMonicDvd
  (f.map (algebraMap F E)) <| map_ne_zero (minpoly.ne_zero_of_finite F α)

Result:
case intro
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : F⟮α⟯ = ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
⊢ Finite (IntermediateField F E)

Proof state:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
h : ∃ α, F⟮α⟯ = ⊤
⊢ Finite (IntermediateField F E)

Tactic:
haveI := FiniteDimensional.of_exists_primitive_element F E h

Result:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
h : ∃ α, F⟮α⟯ = ⊤
this : FiniteDimensional F E
⊢ Finite (IntermediateField F E)

Proof state:
case h.e'_4
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : F⟮α⟯ = ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
K : IntermediateField F E
⊢ Polynomial.map (algebraMap F E) f =
    Polynomial.map (algebraMap (↥K) E) (Polynomial.map (algebraMap F ↥K) (minpoly F α))

Tactic:
rw [Polynomial.map_map]

Result:
case h.e'_4
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : F⟮α⟯ = ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
K : IntermediateField F E
⊢ Polynomial.map (algebraMap F E) f = Polynomial.map ((algebraMap (↥K) E).comp (algebraMap F ↥K)) (minpoly F α)

Proof state:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
h : ∃ α, F⟮α⟯ = ⊤
this : FiniteDimensional F E
⊢ Finite (IntermediateField F E)

Tactic:
obtain ⟨α, hprim⟩ := h

Result:
case intro
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : F⟮α⟯ = ⊤
⊢ Finite (IntermediateField F E)

Proof state:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : F⟮α⟯ = ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
g : IntermediateField F E → G := fun K => ⟨Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α), ⋯⟩
K K' : IntermediateField F E
heq :
  adjoin F ↑(Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)).coeffs =
    adjoin F ↑(Polynomial.map (algebraMap (↥K') E) (minpoly (↥K') α)).coeffs
⊢ K = K'

Tactic:
simpa only [adjoin_minpoly_coeff_of_exists_primitive_element F hprim] using heq

Result:
no goals