-- Mathlib/FieldTheory/SeparableDegree.lean
theorem finSepDegree_eq_finrank_iff [FiniteDimensional F E] :
    finSepDegree F E = finrank F E ↔ Algebra.IsSeparable F E :=
  ⟨fun heq ↦ ⟨fun x ↦ by
    have halg := IsAlgebraic.of_finite F x
    refine (finSepDegree_adjoin_simple_eq_finrank_iff F E x halg).1 <| le_antisymm
      (finSepDegree_adjoin_simple_le_finrank F E x halg) <| le_of_not_lt fun h ↦ ?_
    have := Nat.mul_lt_mul_of_lt_of_le' h (finSepDegree_le_finrank F⟮x⟯ E) Fin.pos'
    rw [finSepDegree_mul_finSepDegree_of_isAlgebraic F F⟮x⟯ E,
      Module.finrank_mul_finrank F F⟮x⟯ E] at this
    linarith only [heq, this]⟩, fun _ ↦ finSepDegree_eq_finrank_of_isSeparable F E⟩

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
heq : finSepDegree F E = finrank F E
x : E
halg : IsAlgebraic F x
h : finSepDegree F ↥F⟮x⟯ < finrank F ↥F⟮x⟯
this : finSepDegree F ↥F⟮x⟯ * finSepDegree (↥F⟮x⟯) E < finrank F ↥F⟮x⟯ * finrank (↥F⟮x⟯) E
⊢ False

Tactic:
rw [finSepDegree_mul_finSepDegree_of_isAlgebraic F F⟮x⟯ E,
  Module.finrank_mul_finrank F F⟮x⟯ E] at this

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
heq : finSepDegree F E = finrank F E
x : E
halg : IsAlgebraic F x
h : finSepDegree F ↥F⟮x⟯ < finrank F ↥F⟮x⟯
this : finSepDegree F E < finrank F E
⊢ False

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
heq : finSepDegree F E = finrank F E
x : E
halg : IsAlgebraic F x
⊢ IsSeparable F x

Tactic:
refine (finSepDegree_adjoin_simple_eq_finrank_iff F E x halg).1 <| le_antisymm
  (finSepDegree_adjoin_simple_le_finrank F E x halg) <| le_of_not_lt fun h ↦ ?_

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
heq : finSepDegree F E = finrank F E
x : E
halg : IsAlgebraic F x
h : finSepDegree F ↥F⟮x⟯ < finrank F ↥F⟮x⟯
⊢ False

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
heq : finSepDegree F E = finrank F E
x : E
halg : IsAlgebraic F x
h : finSepDegree F ↥F⟮x⟯ < finrank F ↥F⟮x⟯
this : finSepDegree F E < finrank F E
⊢ False

Tactic:
linarith only [heq, this]

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
heq : finSepDegree F E = finrank F E
x : E
⊢ IsSeparable F x

Tactic:
have halg := IsAlgebraic.of_finite F x

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
heq : finSepDegree F E = finrank F E
x : E
halg : IsAlgebraic F x
⊢ IsSeparable F x

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
heq : finSepDegree F E = finrank F E
x : E
halg : IsAlgebraic F x
h : finSepDegree F ↥F⟮x⟯ < finrank F ↥F⟮x⟯
⊢ False

Tactic:
have := Nat.mul_lt_mul_of_lt_of_le' h (finSepDegree_le_finrank F⟮x⟯ E) Fin.pos'

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
heq : finSepDegree F E = finrank F E
x : E
halg : IsAlgebraic F x
h : finSepDegree F ↥F⟮x⟯ < finrank F ↥F⟮x⟯
this : finSepDegree F ↥F⟮x⟯ * finSepDegree (↥F⟮x⟯) E < finrank F ↥F⟮x⟯ * finrank (↥F⟮x⟯) E
⊢ False