-- Mathlib/FieldTheory/SeparableDegree.lean
theorem finSepDegree_eq_finrank_of_isSeparable [Algebra.IsSeparable F E] :
    finSepDegree F E = finrank F E

Proof state:
F : Type u
E✝ : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E✝
inst✝³ : Algebra F E✝
E : Type v
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hfd : FiniteDimensional F E
⊢ finSepDegree F ↥⊤ = finrank F ↥⊤

Tactic:
refine induction_on_adjoin (fun K : IntermediateField F E ↦ finSepDegree F K = finrank F K)
  (by simp_rw [finSepDegree_bot, IntermediateField.finrank_bot]) (fun L x h ↦ ?_) ⊤

Result:
F : Type u
E✝ : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E✝
inst✝³ : Algebra F E✝
E : Type v
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hfd : FiniteDimensional F E
L : IntermediateField F E
x : E
h : (fun K => finSepDegree F ↥K = finrank F ↥K) L
⊢ (fun K => finSepDegree F ↥K = finrank F ↥K) (restrictScalars F (↥L)⟮x⟯)

Proof state:
case neg
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
H :
  ∀ (E : Type v) [inst : Field E] [inst_1 : Algebra F E] [inst_2 : Algebra.IsSeparable F E],
    FiniteDimensional F E → finSepDegree F E = finrank F E
hfd : ¬FiniteDimensional F E
halg : Algebra.IsAlgebraic F E
L : IntermediateField F E
h : FiniteDimensional F ↥L
h' : finSepDegree F E < finrank F ↥L
this✝ : Algebra.IsSeparable F ↥L
this : Algebra.IsAlgebraic (↥L) E
hd : finrank F ↥L * finSepDegree (↥L) E = finSepDegree F E
hd' : ¬finSepDegree (↥L) E = 0
⊢ finSepDegree F E = 0

Tactic:
linarith only [h', hd, Nat.le_mul_of_pos_right (finrank F L) (Nat.pos_of_ne_zero hd')]

Result:
no goals

Proof state:
F : Type u
E✝ : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E✝
inst✝³ : Algebra F E✝
E : Type v
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hfd : FiniteDimensional F E
L : IntermediateField F E
x : E
h : finSepDegree F ↥L = finrank F ↥L
heq : finSepDegree F ↥L * finSepDegree ↥L ↥(↥L)⟮x⟯ = finrank F ↥L * finrank ↥L ↥(↥L)⟮x⟯
⊢ finSepDegree F ↥(restrictScalars F (↥L)⟮x⟯) = finrank F ↥(restrictScalars F (↥L)⟮x⟯)

Tactic:
set M := L⟮x⟯

Result:
F : Type u
E✝ : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E✝
inst✝³ : Algebra F E✝
E : Type v
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hfd : FiniteDimensional F E
L : IntermediateField F E
x : E
h : finSepDegree F ↥L = finrank F ↥L
M : IntermediateField (↥L) E := (↥L)⟮x⟯
heq : finSepDegree F ↥L * finSepDegree ↥L ↥M = finrank F ↥L * finrank ↥L ↥M
⊢ finSepDegree F ↥(restrictScalars F M) = finrank F ↥(restrictScalars F M)

Proof state:
case inr.intro.intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
H :
  ∀ (E : Type v) [inst : Field E] [inst_1 : Algebra F E] [inst_2 : Algebra.IsSeparable F E],
    FiniteDimensional F E → finSepDegree F E = finrank F E
hfd : ¬FiniteDimensional F E
halg : Algebra.IsAlgebraic F E
L : IntermediateField F E
h : FiniteDimensional F ↥L
h' : finSepDegree F E < finrank F ↥L
this : Algebra.IsSeparable F ↥L
⊢ finSepDegree F E = 0

Tactic:
have := (halg.tower_top L)

Result:
case inr.intro.intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
H :
  ∀ (E : Type v) [inst : Field E] [inst_1 : Algebra F E] [inst_2 : Algebra.IsSeparable F E],
    FiniteDimensional F E → finSepDegree F E = finrank F E
hfd : ¬FiniteDimensional F E
halg : Algebra.IsAlgebraic F E
L : IntermediateField F E
h : FiniteDimensional F ↥L
h' : finSepDegree F E < finrank F ↥L
this✝ : Algebra.IsSeparable F ↥L
this : Algebra.IsAlgebraic (↥L) E
⊢ finSepDegree F E = 0

Proof state:
case inr.intro.intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
H :
  ∀ (E : Type v) [inst : Field E] [inst_1 : Algebra F E] [inst_2 : Algebra.IsSeparable F E],
    FiniteDimensional F E → finSepDegree F E = finrank F E
hfd : ¬FiniteDimensional F E
halg : Algebra.IsAlgebraic F E
L : IntermediateField F E
h : FiniteDimensional F ↥L
h' : finSepDegree F E < finrank F ↥L
this✝ : Algebra.IsSeparable F ↥L
this : Algebra.IsAlgebraic (↥L) E
hd : finSepDegree F ↥L * finSepDegree (↥L) E = finSepDegree F E
⊢ finSepDegree F E = 0

Tactic:
rw [H L h] at hd

Result:
case inr.intro.intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
H :
  ∀ (E : Type v) [inst : Field E] [inst_1 : Algebra F E] [inst_2 : Algebra.IsSeparable F E],
    FiniteDimensional F E → finSepDegree F E = finrank F E
hfd : ¬FiniteDimensional F E
halg : Algebra.IsAlgebraic F E
L : IntermediateField F E
h : FiniteDimensional F ↥L
h' : finSepDegree F E < finrank F ↥L
this✝ : Algebra.IsSeparable F ↥L
this : Algebra.IsAlgebraic (↥L) E
hd : finrank F ↥L * finSepDegree (↥L) E = finSepDegree F E
⊢ finSepDegree F E = 0

Proof state:
case inr.intro.intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
H :
  ∀ (E : Type v) [inst : Field E] [inst_1 : Algebra F E] [inst_2 : Algebra.IsSeparable F E],
    FiniteDimensional F E → finSepDegree F E = finrank F E
hfd : ¬FiniteDimensional F E
halg : Algebra.IsAlgebraic F E
L : IntermediateField F E
h : FiniteDimensional F ↥L
h' : finSepDegree F E < finrank F ↥L
this✝ : Algebra.IsSeparable F ↥L
this : Algebra.IsAlgebraic (↥L) E
hd : finrank F ↥L * finSepDegree (↥L) E = finSepDegree F E
⊢ finSepDegree F E = 0

Tactic:
by_cases hd' : finSepDegree L E = 0

Result:
case pos
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
H :
  ∀ (E : Type v) [inst : Field E] [inst_1 : Algebra F E] [inst_2 : Algebra.IsSeparable F E],
    FiniteDimensional F E → finSepDegree F E = finrank F E
hfd : ¬FiniteDimensional F E
halg : Algebra.IsAlgebraic F E
L : IntermediateField F E
h : FiniteDimensional F ↥L
h' : finSepDegree F E < finrank F ↥L
this✝ : Algebra.IsSeparable F ↥L
this : Algebra.IsAlgebraic (↥L) E
hd : finrank F ↥L * finSepDegree (↥L) E = finSepDegree F E
hd' : finSepDegree (↥L) E = 0
⊢ finSepDegree F E = 0

case neg
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
H :
  ∀ (E : Type v) [inst : Field E] [inst_1 : Algebra F E] [inst_2 : Algebra.IsSeparable F E],
    FiniteDimensional F E → finSepDegree F E = finrank F E
hfd : ¬FiniteDimensional F E
halg : Algebra.IsAlgebraic F E
L : IntermediateField F E
h : FiniteDimensional F ↥L
h' : finSepDegree F E < finrank F ↥L
this✝ : Algebra.IsSeparable F ↥L
this : Algebra.IsAlgebraic (↥L) E
hd : finrank F ↥L * finSepDegree (↥L) E = finSepDegree F E
hd' : ¬finSepDegree (↥L) E = 0
⊢ finSepDegree F E = 0

Proof state:
F : Type u
E✝ : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E✝
inst✝³ : Algebra F E✝
E : Type v
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hfd : FiniteDimensional F E
L : IntermediateField F E
x : E
h : finSepDegree F ↥L = finrank F ↥L
M : IntermediateField (↥L) E := (↥L)⟮x⟯
heq : finSepDegree F ↥L * finSepDegree ↥L ↥M = finrank F ↥L * finrank ↥L ↥M
this : Algebra.IsAlgebraic ↥L ↥M
⊢ finSepDegree F ↥(restrictScalars F M) = finrank F ↥(restrictScalars F M)

Tactic:
rwa [finSepDegree_mul_finSepDegree_of_isAlgebraic F L M,
  Module.finrank_mul_finrank F L M] at heq

Result:
no goals