-- Mathlib/FieldTheory/PurelyInseparable/Basic.lean
theorem finSepDegree_eq [Algebra.IsAlgebraic F E] :
    finSepDegree F E = Cardinal.toNat (sepDegree F E)

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this✝ : Algebra.IsAlgebraic (↥(separableClosure F E)) E
h : finSepDegree F E = finSepDegree F ↥(separableClosure F E) * finSepDegree (↥(separableClosure F E)) E
this : Algebra.IsSeparable F ↥(separableClosure F E)
⊢ finSepDegree F E = Cardinal.toNat (sepDegree F E)

Tactic:
haveI := separableClosure.isPurelyInseparable F E

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this✝¹ : Algebra.IsAlgebraic (↥(separableClosure F E)) E
h : finSepDegree F E = finSepDegree F ↥(separableClosure F E) * finSepDegree (↥(separableClosure F E)) E
this✝ : Algebra.IsSeparable F ↥(separableClosure F E)
this : IsPurelyInseparable (↥(separableClosure F E)) E
⊢ finSepDegree F E = Cardinal.toNat (sepDegree F E)

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : Algebra.IsAlgebraic (↥(separableClosure F E)) E
⊢ finSepDegree F E = Cardinal.toNat (sepDegree F E)

Tactic:
have h := finSepDegree_mul_finSepDegree_of_isAlgebraic F (separableClosure F E) E |>.symm

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : Algebra.IsAlgebraic (↥(separableClosure F E)) E
h : finSepDegree F E = finSepDegree F ↥(separableClosure F E) * finSepDegree (↥(separableClosure F E)) E
⊢ finSepDegree F E = Cardinal.toNat (sepDegree F E)

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : Algebra.IsAlgebraic (↥(separableClosure F E)) E
h : finSepDegree F E = finSepDegree F ↥(separableClosure F E) * finSepDegree (↥(separableClosure F E)) E
⊢ finSepDegree F E = Cardinal.toNat (sepDegree F E)

Tactic:
haveI := separableClosure.isSeparable F E

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this✝ : Algebra.IsAlgebraic (↥(separableClosure F E)) E
h : finSepDegree F E = finSepDegree F ↥(separableClosure F E) * finSepDegree (↥(separableClosure F E)) E
this : Algebra.IsSeparable F ↥(separableClosure F E)
⊢ finSepDegree F E = Cardinal.toNat (sepDegree F E)

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this✝¹ : Algebra.IsAlgebraic (↥(separableClosure F E)) E
h : finSepDegree F E = finSepDegree F ↥(separableClosure F E) * finSepDegree (↥(separableClosure F E)) E
this✝ : Algebra.IsSeparable F ↥(separableClosure F E)
this : IsPurelyInseparable (↥(separableClosure F E)) E
⊢ finSepDegree F E = Cardinal.toNat (sepDegree F E)

Tactic:
rwa [finSepDegree_eq_finrank_of_isSeparable F (separableClosure F E),
  IsPurelyInseparable.finSepDegree_eq_one (separableClosure F E) E, mul_one] at h

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
⊢ finSepDegree F E = Cardinal.toNat (sepDegree F E)

Tactic:
have : Algebra.IsAlgebraic (separableClosure F E) E := Algebra.IsAlgebraic.tower_top (K := F) _

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : Algebra.IsAlgebraic (↥(separableClosure F E)) E
⊢ finSepDegree F E = Cardinal.toNat (sepDegree F E)