-- Mathlib/FieldTheory/PrimitiveElement.lean
theorem primitive_element_iff_algHom_eq_of_eval (α : E)
    (φ : E →ₐ[F] A) : F⟮α⟯ = ⊤ ↔ ∀ ψ : E →ₐ[F] A, φ α = ψ α → φ = ψ

Proof state:
F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), Splits (algebraMap F A) (minpoly F x)
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ
this✝ : Algebra (↥F⟮α⟯) A := (φ.comp F⟮α⟯.val).toAlgebra
this : Algebra.IsSeparable (↥F⟮α⟯) E
⊢ finrank (↥F⟮α⟯) E = finrank (↥⊤) E

Tactic:
rw [IntermediateField.finrank_top, ← AlgHom.card_of_splits _ _ A, Fintype.card_eq_one_iff]

Result:
F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), Splits (algebraMap F A) (minpoly F x)
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ
this✝ : Algebra (↥F⟮α⟯) A := (φ.comp F⟮α⟯.val).toAlgebra
this : Algebra.IsSeparable (↥F⟮α⟯) E
⊢ ∃ x, ∀ (y : E →ₐ[↥F⟮α⟯] A), y = x

F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), Splits (algebraMap F A) (minpoly F x)
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ
this✝ : Algebra (↥F⟮α⟯) A := (φ.comp F⟮α⟯.val).toAlgebra
this : Algebra.IsSeparable (↥F⟮α⟯) E
⊢ ∀ (x : E), Splits (algebraMap (↥F⟮α⟯) A) (minpoly (↥F⟮α⟯) x)

Proof state:
F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), Splits (algebraMap F A) (minpoly F x)
α : E
φ : E →ₐ[F] A
⊢ F⟮α⟯ = ⊤ ↔ ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ

Tactic:
refine ⟨fun h ψ hψ ↦ (Field.primitive_element_iff_algHom_eq_of_eval' F A hA α).mp h hψ,
  fun h ↦ eq_of_le_of_finrank_eq' le_top ?_⟩

Result:
F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), Splits (algebraMap F A) (minpoly F x)
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ
⊢ finrank (↥F⟮α⟯) E = finrank (↥⊤) E

Proof state:
F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), Splits (algebraMap F A) (minpoly F x)
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ
this : Algebra (↥F⟮α⟯) A := (φ.comp F⟮α⟯.val).toAlgebra
⊢ finrank (↥F⟮α⟯) E = finrank (↥⊤) E

Tactic:
haveI := Algebra.isSeparable_tower_top_of_isSeparable F F⟮α⟯ E

Result:
F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), Splits (algebraMap F A) (minpoly F x)
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ
this✝ : Algebra (↥F⟮α⟯) A := (φ.comp F⟮α⟯.val).toAlgebra
this : Algebra.IsSeparable (↥F⟮α⟯) E
⊢ finrank (↥F⟮α⟯) E = finrank (↥⊤) E

Proof state:
F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), Splits (algebraMap F A) (minpoly F x)
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ
this✝ : Algebra (↥F⟮α⟯) A := (φ.comp F⟮α⟯.val).toAlgebra
this : Algebra.IsSeparable (↥F⟮α⟯) E
⊢ ∀ (x : E), Splits (algebraMap (↥F⟮α⟯) A) (minpoly (↥F⟮α⟯) x)

Tactic:
exact fun x ↦ (IsIntegral.of_finite F x).minpoly_splits_tower_top (hA x)

Result:
no goals

Proof state:
F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), Splits (algebraMap F A) (minpoly F x)
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ
this✝ : Algebra (↥F⟮α⟯) A := (φ.comp F⟮α⟯.val).toAlgebra
this : Algebra.IsSeparable (↥F⟮α⟯) E
⊢ ∃ x, ∀ (y : E →ₐ[↥F⟮α⟯] A), y = x

Tactic:
exact ⟨{ __ := φ, commutes' := fun _ ↦ rfl }, fun ψ ↦ AlgHom.restrictScalars_injective F <|
  Eq.symm <| h _ (ψ.commutes <| AdjoinSimple.gen F α).symm⟩

Result:
no goals

Proof state:
F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), Splits (algebraMap F A) (minpoly F x)
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ
⊢ finrank (↥F⟮α⟯) E = finrank (↥⊤) E

Tactic:
letI : Algebra F⟮α⟯ A := (φ.comp F⟮α⟯.val).toAlgebra

Result:
F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), Splits (algebraMap F A) (minpoly F x)
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ
this : Algebra (↥F⟮α⟯) A := (φ.comp F⟮α⟯.val).toAlgebra
⊢ finrank (↥F⟮α⟯) E = finrank (↥⊤) E