-- 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 }
hfin : Finite G
g : IntermediateField F E → G := fun K => ⟨Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α), ⋯⟩
hinj : Function.Injective g
⊢ Finite (IntermediateField F E)

Tactic:
exact Finite.of_injective g hinj

Result:
no goals

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).comp (algebraMap F ↥K)) (minpoly F α)

Tactic:
rfl

Result:
no goals

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 : g K = g K'
⊢ K = K'

Tactic:
rw [Subtype.mk.injEq] at heq

Result:
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 : Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α) = Polynomial.map (algebraMap (↥K') E) (minpoly (↥K') α)
⊢ K = K'

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
K : IntermediateField F E
⊢ Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α) ∣ Polynomial.map (algebraMap F E) f

Tactic:
convert Polynomial.map_dvd (algebraMap K E) (minpoly.dvd_map_of_isScalarTower F K α)

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) (Polynomial.map (algebraMap F ↥K) (minpoly F α))

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 α
⊢ Finite (IntermediateField F E)

Tactic:
let G := { g : E[X] // g.Monic ∧ g ∣ f.map (algebraMap F E) }

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 }
⊢ 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 }
hfin : Finite G
g : IntermediateField F E → G := fun K => ⟨Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α), ⋯⟩
⊢ Finite (IntermediateField F E)

Tactic:
have hinj : Function.Injective g := fun K K' heq ↦ by
  rw [Subtype.mk.injEq] at heq
  apply_fun fun f : E[X] ↦ adjoin F (f.coeffs : Set E) at heq
  simpa only [adjoin_minpoly_coeff_of_exists_primitive_element F hprim] using heq

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
g : IntermediateField F E → G := fun K => ⟨Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α), ⋯⟩
hinj : Function.Injective g
⊢ 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⟮α⟯ = ⊤
⊢ Finite (IntermediateField F E)

Tactic:
let f : F[X] := minpoly 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 α
⊢ 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 : Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α) = Polynomial.map (algebraMap (↥K') E) (minpoly (↥K') α)
⊢ K = K'

Tactic:
apply_fun fun f : E[X] ↦ adjoin F (f.coeffs : Set E) at heq

Result:
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'

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 }
hfin : Finite G
⊢ Finite (IntermediateField F E)

Tactic:
let g : IntermediateField F E → G := fun K ↦
  ⟨(minpoly K α).map (algebraMap K E), (minpoly.monic <| .of_finite K α).map _, by
    convert Polynomial.map_dvd (algebraMap K E) (minpoly.dvd_map_of_isScalarTower F K α)
    rw [Polynomial.map_map]; rfl⟩

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
g : IntermediateField F E → G := fun K => ⟨Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α), ⋯⟩
⊢ Finite (IntermediateField F E)