-- Mathlib/FieldTheory/SeparableDegree.lean
theorem finSepDegree_dvd_finrank : finSepDegree F E ∣ finrank F E

Proof state:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra 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:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra 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 neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hfd : ¬FiniteDimensional F E
⊢ finSepDegree F E ∣ 0

Tactic:
exact dvd_zero _

Result:
no goals

Proof state:
case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hfd : ¬FiniteDimensional F E
⊢ finSepDegree F E ∣ finrank F E

Tactic:
rw [finrank_of_infinite_dimensional hfd]

Result:
case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra 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
hfd : FiniteDimensional F E
L : IntermediateField F E
x : E
h : finSepDegree F ↥L ∣ finrank F ↥L
M : IntermediateField (↥L) E := (↥L)⟮x⟯
hdvd : 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 hdvd

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ finSepDegree F E ∣ finrank F E

Tactic:
by_cases hfd : FiniteDimensional F E

Result:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hfd : FiniteDimensional F E
⊢ finSepDegree F E ∣ finrank F E

case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hfd : ¬FiniteDimensional F E
⊢ finSepDegree F E ∣ finrank F E

Proof state:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hfd : FiniteDimensional F E
⊢ finSepDegree F E ∣ finrank F E

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

Result:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hfd : FiniteDimensional F E
⊢ finSepDegree F ↥⊤ ∣ finrank F ↥⊤

Proof state:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hfd : FiniteDimensional F E
L : IntermediateField F E
x : E
h : finSepDegree F ↥L ∣ finrank F ↥L
hdvd : 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:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra 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⟯
hdvd : 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 pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra 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, one_dvd]) (fun L x h ↦ ?_) ⊤

Result:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra 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 pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra 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⟯)

Tactic:
have hdvd := mul_dvd_mul h <| finSepDegree_adjoin_simple_dvd_finrank L E x

Result:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hfd : FiniteDimensional F E
L : IntermediateField F E
x : E
h : finSepDegree F ↥L ∣ finrank F ↥L
hdvd : 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⟯)

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hfd : FiniteDimensional F E
⊢ (fun K => finSepDegree F ↥K ∣ finrank F ↥K) ⊥

Tactic:
simp_rw [finSepDegree_bot, IntermediateField.finrank_bot, one_dvd]

Result:
no goals

Proof state:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra 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⟯
hdvd : finSepDegree F ↥L * finSepDegree ↥L ↥M ∣ finrank F ↥L * finrank ↥L ↥M
⊢ finSepDegree F ↥(restrictScalars F M) ∣ finrank F ↥(restrictScalars F M)

Tactic:
have := Algebra.IsAlgebraic.of_finite L M

Result:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra 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⟯
hdvd : 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)