-- 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
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⟯)

Tactic:
simp only at 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 : finSepDegree F ↥L = finrank F ↥L
⊢ finSepDegree F ↥(restrictScalars F (↥L)⟮x⟯) = finrank F ↥(restrictScalars F (↥L)⟮x⟯)

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
⊢ finSepDegree F E = 0

Tactic:
have : Algebra.IsSeparable F L := Algebra.isSeparable_tower_bot_of_isSeparable F L E

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
⊢ finSepDegree F E = 0

Proof state:
case inr
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
⊢ finSepDegree F E = finrank F E

Tactic:
rw [finrank_of_infinite_dimensional hfd]

Result:
case inr
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
⊢ finSepDegree F E = 0

Proof state:
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

Tactic:
rw [← hd, hd', mul_zero]

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
⊢ finSepDegree F E = finrank F E

Tactic:
rw [← finSepDegree_top F, ← finrank_top F E]

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
⊢ finSepDegree F ↥⊤ = finrank F ↥⊤

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

Tactic:
wlog hfd : FiniteDimensional F E generalizing E with H

Result:
case inr
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
⊢ finSepDegree F E = finrank F E

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 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
⊢ (fun K => finSepDegree F ↥K = finrank F ↥K) ⊥

Tactic:
simp_rw [finSepDegree_bot, IntermediateField.finrank_bot]

Result:
no goals

Proof state:
case inr
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
⊢ finSepDegree F E = 0

Tactic:
obtain ⟨L, h, h'⟩ := exists_lt_finrank_of_infinite_dimensional hfd (finSepDegree F E)

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
⊢ finSepDegree F E = 0

Proof state:
case inr
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
⊢ finSepDegree F E = 0

Tactic:
have halg := Algebra.IsSeparable.isAlgebraic F E

Result:
case inr
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
⊢ 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
⊢ finSepDegree F E = 0

Tactic:
have hd := finSepDegree_mul_finSepDegree_of_isAlgebraic F L E

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 : finSepDegree F ↥L * finSepDegree (↥L) E = finSepDegree F E
⊢ finSepDegree F E = 0