awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
halg : IsAlgebraic F α
rw : natSepDegree (minpoly F α) = finrank.{u, v} F ↥F⟮α⟯ ↔ IsSeparable F α
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ = finrank.{u, v} F ↥F⟮α⟯ ↔ IsSeparable F α
have rw₁ : natSepDegree (minpoly F α) = natDegree (minpoly F α) ↔ IsSeparable F α
Tactic: rw [finSepDegree_adjoin_simple_eq_natSepDegree F E halg, adjoin.finrank halg.isIntegral,
    natSepDegree_eq_natDegree_iff _ (minpoly.ne_zero halg.isIntegral), IsSeparable]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
halg : IsAlgebraic F α
rw : natSepDegree (minpoly F α) = finrank.{u, v} F ↥F⟮α⟯ ↔ IsSeparable F α
rw₁ : natSepDegree (minpoly F α) = natDegree (minpoly F α) ↔ IsSeparable F α
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ = finrank.{u, v} F ↥F⟮α⟯ ↔ IsSeparable F α
have rw₂ : Separable (minpoly F α) ↔ IsSeparable F α
Tactic: rw [finSepDegree_adjoin_simple_eq_natSepDegree F E halg, adjoin.finrank halg.isIntegral,
    natSepDegree_eq_natDegree_iff _ (minpoly.ne_zero halg.isIntegral), IsSeparable]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
halg : IsAlgebraic F α
rw : natSepDegree (minpoly F α) = finrank.{u, v} F ↥F⟮α⟯ ↔ IsSeparable F α
rw₁ : natSepDegree (minpoly F α) = natDegree (minpoly F α) ↔ IsSeparable F α
rw₂ : Separable (minpoly F α) ↔ IsSeparable F α
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ = finrank.{u, v} F ↥F⟮α⟯ ↔ IsSeparable F α
have rw₃ : Separable (minpoly F α) ↔ Separable (minpoly F α)
Tactic: rw [finSepDegree_adjoin_simple_eq_natSepDegree F E halg, adjoin.finrank halg.isIntegral,
    natSepDegree_eq_natDegree_iff _ (minpoly.ne_zero halg.isIntegral), IsSeparable]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ finSepDegree F E ∣ finrank F E
have pos : ∀ (hfd : FiniteDimensional F E), finSepDegree F E ∣ finrank F E
Tactic: by_cases hfd : FiniteDimensional F E
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
pos : ∀ (hfd : FiniteDimensional F E), finSepDegree F E ∣ finrank F E
⊢ finSepDegree F E ∣ finrank F E
have neg : ∀ (hfd : ¬FiniteDimensional F E), finSepDegree F E ∣ finrank F E
Tactic: by_cases hfd : FiniteDimensional F E
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hfd : FiniteDimensional F E
⊢ finSepDegree F E ∣ finrank F E
have pos : finSepDegree.{u, v} F ↥⊤ ∣ finrank.{u, v} F ↥⊤
Tactic: rw [← finSepDegree_top F, ← finrank_top F E]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hfd : FiniteDimensional F E
simp_rw simp_rw₁ : finSepDegree.{u, v} F ↥⊥ ∣ finrank.{u, v} F ↥⊥
⊢ finSepDegree.{u, v} F ↥⊥ ∣ finrank.{u, v} F ↥⊥
have simp_rw₂ : 1 ∣ finrank.{u, v} F ↥⊥
Tactic: simp_rw [finSepDegree_bot, IntermediateField.finrank_bot, one_dvd]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hfd : FiniteDimensional F E
simp_rw simp_rw₁ : finSepDegree.{u, v} F ↥⊥ ∣ finrank.{u, v} F ↥⊥
simp_rw₂ : 1 ∣ finrank.{u, v} F ↥⊥
⊢ finSepDegree.{u, v} F ↥⊥ ∣ finrank.{u, v} F ↥⊥
have simp_rw₃ : Dvd.dvd (α := ℕ) 1 1
Tactic: simp_rw [finSepDegree_bot, IntermediateField.finrank_bot, one_dvd]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hfd : FiniteDimensional F E
⊢ finSepDegree.{u, v} F ↥⊤ ∣ finrank.{u, v} F ↥⊤
have pos : ∀ (L : IntermediateField F E) (x : E)
  (h : (fun (K : IntermediateField F E) ↦ finSepDegree.{u, v} F ↥K ∣ finrank.{u, v} F ↥K) L),
  (fun (K : IntermediateField F E) ↦ finSepDegree.{u, v} F ↥K ∣ finrank.{u, v} F ↥K)
    (IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯)
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 ↦ ?_) ⊤
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hfd : FiniteDimensional F E
L : IntermediateField F E
x : E
h : finSepDegree.{u, v} F ↥L ∣ finrank.{u, v} F ↥L
⊢ finSepDegree.{u, v} F ↥(IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯) ∣
    finrank.{u, v} F ↥(IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯)
have hdvd : finSepDegree.{u, v} F ↥L * finSepDegree.{v, v} ↥L ↥(↥L)⟮x⟯ ∣ finrank.{u, v} F ↥L * finrank.{v, v} ↥L ↥(↥L)⟮x⟯
Tactic: have hdvd := mul_dvd_mul h <| finSepDegree_adjoin_simple_dvd_finrank L E x
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hfd : FiniteDimensional F E
L : IntermediateField F E
x : E
h : finSepDegree.{u, v} F ↥L ∣ finrank.{u, v} F ↥L
hdvd : finSepDegree.{u, v} F ↥L * finSepDegree.{v, v} ↥L ↥(↥L)⟮x⟯ ∣ finrank.{u, v} F ↥L * finrank.{v, v} ↥L ↥(↥L)⟮x⟯
⊢ finSepDegree.{u, v} F ↥(IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯) ∣
    finrank.{u, v} F ↥(IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯)
have pos : let M : IntermediateField (↥L) E := (↥L)⟮x⟯;
∀ (hdvd : finSepDegree.{u, v} F ↥L * finSepDegree.{v, v} ↥L ↥M ∣ finrank.{u, v} F ↥L * finrank.{v, v} ↥L ↥M),
  finSepDegree.{u, v} F ↥(IntermediateField.restrictScalars F M) ∣
    finrank.{u, v} F ↥(IntermediateField.restrictScalars F M)
Tactic: set M := L⟮x⟯
Cleared hypotheses: hdvd
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hfd : FiniteDimensional F E
L : IntermediateField F E
x : E
h : finSepDegree.{u, v} F ↥L ∣ finrank.{u, v} F ↥L
M : IntermediateField (↥L) E := (↥L)⟮x⟯
hdvd : finSepDegree.{u, v} F ↥L * finSepDegree.{v, v} ↥L ↥M ∣ finrank.{u, v} F ↥L * finrank.{v, v} ↥L ↥M
⊢ finSepDegree.{u, v} F ↥(IntermediateField.restrictScalars F M) ∣
    finrank.{u, v} F ↥(IntermediateField.restrictScalars F M)
have pos : ∀ (hdvd : finSepDegree.{u, v} F ↥M ∣ finrank.{u, v} F ↥L * finrank.{v, v} ↥L ↥M),
  finSepDegree.{u, v} F ↥(IntermediateField.restrictScalars F M) ∣
    finrank.{u, v} F ↥(IntermediateField.restrictScalars F M)
Tactic: rwa [finSepDegree_mul_finSepDegree_of_isAlgebraic F L M,
      Module.finrank_mul_finrank F L M] at hdvd
Cleared hypotheses: hdvd
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hfd : FiniteDimensional F E
L : IntermediateField F E
x : E
h : finSepDegree.{u, v} F ↥L ∣ finrank.{u, v} F ↥L
M : IntermediateField (↥L) E := (↥L)⟮x⟯
hdvd : finSepDegree.{u, v} F ↥L * finSepDegree.{v, v} ↥L ↥M ∣ finrank.{u, v} F ↥L * finrank.{v, v} ↥L ↥M
pos :
  ∀ (hdvd : finSepDegree.{u, v} F ↥M ∣ finrank.{u, v} F ↥L * finrank.{v, v} ↥L ↥M),
    finSepDegree.{u, v} F ↥(IntermediateField.restrictScalars F M) ∣
      finrank.{u, v} F ↥(IntermediateField.restrictScalars F M)
⊢ finSepDegree.{u, v} F ↥(IntermediateField.restrictScalars F M) ∣
    finrank.{u, v} F ↥(IntermediateField.restrictScalars F M)
have pos₁ : ∀ (hdvd : finSepDegree.{u, v} F ↥M ∣ finrank.{u, v} F ↥M),
  finSepDegree.{u, v} F ↥(IntermediateField.restrictScalars F M) ∣
    finrank.{u, v} F ↥(IntermediateField.restrictScalars F M)
Tactic: rwa [finSepDegree_mul_finSepDegree_of_isAlgebraic F L M,
      Module.finrank_mul_finrank F L M] at hdvd
Cleared hypotheses: hdvd
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hfd : ¬FiniteDimensional F E
⊢ finSepDegree F E ∣ finrank F E
have neg : finSepDegree F E ∣ 0
Tactic: rw [finrank_of_infinite_dimensional hfd]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
⊢ finSepDegree F E = finrank F E
have inr : ∀
  (H :
    ∀ (E : Type v) [inst_4 : Field E] [inst_5 : Algebra F E] [Algebra.IsSeparable F E] (hfd : FiniteDimensional F E),
      finSepDegree F E = finrank F E)
  (hfd : ¬FiniteDimensional F E), finSepDegree F E = finrank F E
Tactic: wlog hfd : FiniteDimensional F E generalizing E with H
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
inr :
  ∀
    (H :
      ∀ (E : Type v) [inst_4 : Field E] [inst_5 : Algebra F E] [Algebra.IsSeparable F E] (hfd : FiniteDimensional F E),
        finSepDegree F E = finrank F E)
    (hfd : ¬FiniteDimensional F E), finSepDegree F E = finrank F E
⊢ finSepDegree F E = finrank F E
have wlog : ∀ (E : Type v) [inst_4 : Field E] [inst_5 : Algebra F E] [Algebra.IsSeparable F E] (hfd : FiniteDimensional F E),
  finSepDegree F E = finrank F E
Tactic: wlog hfd : FiniteDimensional F E generalizing E with H
Cleared hypotheses: inst_3
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
H :
  ∀ (E : Type v) [inst_4 : Field E] [inst_5 : Algebra F E] [Algebra.IsSeparable F E] (hfd : FiniteDimensional F E),
    finSepDegree F E = finrank F E
hfd : ¬FiniteDimensional F E
⊢ finSepDegree F E = finrank F E
have inr : finSepDegree F E = 0
Tactic: rw [finrank_of_infinite_dimensional hfd]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
H :
  ∀ (E : Type v) [inst_4 : Field E] [inst_5 : Algebra F E] [Algebra.IsSeparable F E] (hfd : FiniteDimensional F E),
    finSepDegree F E = finrank F E
hfd : ¬FiniteDimensional F E
⊢ finSepDegree F E = 0
have inr : ∀ (L : IntermediateField F E) (h : FiniteDimensional.{u, v} F ↥L) (h' : finSepDegree F E < finrank.{u, v} F ↥L),
  finSepDegree F E = 0
Tactic: obtain ⟨L, h, h'⟩ := exists_lt_finrank_of_infinite_dimensional hfd (finSepDegree F E)
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
H :
  ∀ (E : Type v) [inst_4 : Field E] [inst_5 : Algebra F E] [Algebra.IsSeparable F E] (hfd : FiniteDimensional F E),
    finSepDegree F E = finrank F E
hfd : ¬FiniteDimensional F E
L : IntermediateField F E
h : FiniteDimensional.{u, v} F ↥L
h' : finSepDegree F E < finrank.{u, v} F ↥L
⊢ finSepDegree F E = 0
have hd : finSepDegree.{u, v} F ↥L * finSepDegree (↥L) E = finSepDegree F E
Tactic: have hd := finSepDegree_mul_finSepDegree_of_isAlgebraic F L E
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
H :
  ∀ (E : Type v) [inst_4 : Field E] [inst_5 : Algebra F E] [Algebra.IsSeparable F E] (hfd : FiniteDimensional F E),
    finSepDegree F E = finrank F E
hfd : ¬FiniteDimensional F E
L : IntermediateField F E
h : FiniteDimensional.{u, v} F ↥L
h' : finSepDegree F E < finrank.{u, v} F ↥L
hd : finSepDegree.{u, v} F ↥L * finSepDegree (↥L) E = finSepDegree F E
⊢ finSepDegree F E = 0
have hd₁ : finrank.{u, v} F ↥L * finSepDegree (↥L) E = finSepDegree F E
Tactic: rw [H L h] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
H :
  ∀ (E : Type v) [inst_4 : Field E] [inst_5 : Algebra F E] [Algebra.IsSeparable F E] (hfd : FiniteDimensional F E),
    finSepDegree F E = finrank F E
hfd : ¬FiniteDimensional F E
L : IntermediateField F E
h : FiniteDimensional.{u, v} F ↥L
h' : finSepDegree F E < finrank.{u, v} F ↥L
hd : finrank.{u, v} F ↥L * finSepDegree (↥L) E = finSepDegree F E
⊢ finSepDegree F E = 0
have pos : ∀ (hd' : finSepDegree (↥L) E = 0), finSepDegree F E = 0
Tactic: by_cases hd' : finSepDegree L E = 0
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
H :
  ∀ (E : Type v) [inst_4 : Field E] [inst_5 : Algebra F E] [Algebra.IsSeparable F E] (hfd : FiniteDimensional F E),
    finSepDegree F E = finrank F E
hfd : ¬FiniteDimensional F E
L : IntermediateField F E
h : FiniteDimensional.{u, v} F ↥L
h' : finSepDegree F E < finrank.{u, v} F ↥L
hd : finrank.{u, v} F ↥L * finSepDegree (↥L) E = finSepDegree F E
pos : ∀ (hd' : finSepDegree (↥L) E = 0), finSepDegree F E = 0
⊢ finSepDegree F E = 0
have neg : ∀ (hd' : ¬finSepDegree (↥L) E = 0), finSepDegree F E = 0
Tactic: by_cases hd' : finSepDegree L E = 0
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
H :
  ∀ (E : Type v) [inst_4 : Field E] [inst_5 : Algebra F E] [Algebra.IsSeparable F E] (hfd : FiniteDimensional F E),
    finSepDegree F E = finrank F E
hfd : ¬FiniteDimensional F E
L : IntermediateField F E
h : FiniteDimensional.{u, v} F ↥L
h' : finSepDegree F E < finrank.{u, v} F ↥L
hd : finrank.{u, v} F ↥L * finSepDegree (↥L) E = finSepDegree F E
hd' : finSepDegree (↥L) E = 0
⊢ finSepDegree F E = 0
have pos : finrank.{u, v} F ↥L * finSepDegree (↥L) E = 0
Tactic: rw [← hd, hd', mul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
H :
  ∀ (E : Type v) [inst_4 : Field E] [inst_5 : Algebra F E] [Algebra.IsSeparable F E] (hfd : FiniteDimensional F E),
    finSepDegree F E = finrank F E
hfd : ¬FiniteDimensional F E
L : IntermediateField F E
h : FiniteDimensional.{u, v} F ↥L
h' : finSepDegree F E < finrank.{u, v} F ↥L
hd : finrank.{u, v} F ↥L * finSepDegree (↥L) E = finSepDegree F E
hd' : finSepDegree (↥L) E = 0
pos : finrank.{u, v} F ↥L * finSepDegree (↥L) E = 0
⊢ finSepDegree F E = 0
have pos₁ : finrank.{u, v} F ↥L * 0 = 0
Tactic: rw [← hd, hd', mul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
H :
  ∀ (E : Type v) [inst_4 : Field E] [inst_5 : Algebra F E] [Algebra.IsSeparable F E] (hfd : FiniteDimensional F E),
    finSepDegree F E = finrank F E
hfd : ¬FiniteDimensional F E
L : IntermediateField F E
h : FiniteDimensional.{u, v} F ↥L
h' : finSepDegree F E < finrank.{u, v} F ↥L
hd : finrank.{u, v} F ↥L * finSepDegree (↥L) E = finSepDegree F E
hd' : finSepDegree (↥L) E = 0
pos : finrank.{u, v} F ↥L * finSepDegree (↥L) E = 0
pos₁ : finrank.{u, v} F ↥L * 0 = 0
⊢ finSepDegree F E = 0
have pos₂ : Eq (α := ℕ) 0 0
Tactic: rw [← hd, hd', mul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
H :
  ∀ (E : Type v) [inst_4 : Field E] [inst_5 : Algebra F E] [Algebra.IsSeparable F E] (hfd : FiniteDimensional F E),
    finSepDegree F E = finrank F E
hfd : ¬FiniteDimensional F E
L : IntermediateField F E
h : FiniteDimensional.{u, v} F ↥L
h' : finSepDegree F E < finrank.{u, v} F ↥L
hd : finrank.{u, v} F ↥L * finSepDegree (↥L) E = finSepDegree F E
hd' : ¬finSepDegree (↥L) E = 0
⊢ finSepDegree F E = 0
have linarith : finSepDegree F E < 0 →
  -1 + HSub.hSub (α := ℤ) 0 (↑(finSepDegree F E) : ℤ) + (HAdd.hAdd (α := ℤ) (↑(finSepDegree F E) : ℤ) 1 - 0) = 0
Tactic: linarith only [h', hd, Nat.le_mul_of_pos_right (finrank F L) (Nat.pos_of_ne_zero hd')]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
H :
  ∀ (E : Type v) [inst_4 : Field E] [inst_5 : Algebra F E] [Algebra.IsSeparable F E] (hfd : FiniteDimensional F E),
    finSepDegree F E = finrank F E
hfd : ¬FiniteDimensional F E
L : IntermediateField F E
h : FiniteDimensional.{u, v} F ↥L
h' : finSepDegree F E < finrank.{u, v} F ↥L
hd : finrank.{u, v} F ↥L * finSepDegree (↥L) E = finSepDegree F E
hd' : ¬finSepDegree (↥L) E = 0
linarith :
  finSepDegree F E < 0 →
    -1 + HSub.hSub (α := ℤ) 0 (↑(finSepDegree F E) : ℤ) + (HAdd.hAdd (α := ℤ) (↑(finSepDegree F E) : ℤ) 1 - 0) = 0
⊢ finSepDegree F E = 0
have linarith₁ : 0 < finSepDegree F E →
  -1 + (HAdd.hAdd (α := ℤ) (↑(finSepDegree F E) : ℤ) 1 - (↑(finrank.{u, v} F ↥L) : ℤ)) +
        (HMul.hMul (α := ℤ) (↑(finrank.{u, v} F ↥L) : ℤ) (↑(finSepDegree (↥L) E) : ℤ) - (↑(finSepDegree F E) : ℤ)) +
      ((↑(finrank.{u, v} F ↥L) : ℤ) - HMul.hMul (α := ℤ) (↑(finrank.{u, v} F ↥L) : ℤ) (↑(finSepDegree (↥L) E) : ℤ)) =
    0
Tactic: linarith only [h', hd, Nat.le_mul_of_pos_right (finrank F L) (Nat.pos_of_ne_zero hd')]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E_1 : Type v
inst : Field F
inst_1 : Field E_1
inst_2 : Algebra F E_1
E : Type v
inst_3 : Field E
inst_4 : Algebra F E
inst_5 : Algebra.IsSeparable F E
hfd : FiniteDimensional F E
⊢ finSepDegree F E = finrank F E
have rw : finSepDegree.{u, v} F ↥⊤ = finrank.{u, v} F ↥⊤
Tactic: rw [← finSepDegree_top F, ← finrank_top F E]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E_1 : Type v
inst : Field F
inst_1 : Field E_1
inst_2 : Algebra F E_1
E : Type v
inst_3 : Field E
inst_4 : Algebra F E
inst_5 : Algebra.IsSeparable F E
hfd : FiniteDimensional F E
simp_rw simp_rw₁ : finSepDegree.{u, v} F ↥⊥ = finrank.{u, v} F ↥⊥
⊢ finSepDegree.{u, v} F ↥⊥ = finrank.{u, v} F ↥⊥
have simp_rw₂ : 1 = finrank.{u, v} F ↥⊥
Tactic: simp_rw [finSepDegree_bot, IntermediateField.finrank_bot]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E_1 : Type v
inst : Field F
inst_1 : Field E_1
inst_2 : Algebra F E_1
E : Type v
inst_3 : Field E
inst_4 : Algebra F E
inst_5 : Algebra.IsSeparable F E
hfd : FiniteDimensional F E
⊢ finSepDegree.{u, v} F ↥⊤ = finrank.{u, v} F ↥⊤
have refine : ∀ (L : IntermediateField F E) (x : E)
  (h : (fun (K : IntermediateField F E) ↦ finSepDegree.{u, v} F ↥K = finrank.{u, v} F ↥K) L),
  (fun (K : IntermediateField F E) ↦ finSepDegree.{u, v} F ↥K = finrank.{u, v} F ↥K)
    (IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯)
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 ↦ ?_) ⊤
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
E_1 : Type v
inst : Field F
inst_1 : Field E_1
inst_2 : Algebra F E_1
E : Type v
inst_3 : Field E
inst_4 : Algebra F E
inst_5 : Algebra.IsSeparable F E
hfd : FiniteDimensional F E
L : IntermediateField F E
x : E
h : finSepDegree.{u, v} F ↥L = finrank.{u, v} F ↥L
⊢ finSepDegree.{u, v} F ↥(IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯) =
    finrank.{u, v} F ↥(IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯)
have heq : finSepDegree.{u, v} F ↥L * finSepDegree.{v, v} ↥L ↥(↥L)⟮x⟯ = finrank.{u, v} F ↥L * finrank.{v, v} ↥L ↥(↥L)⟮x⟯
Tactic: have heq : _ * _ = _ * _ := congr_arg₂ (· * ·) h <|
    (finSepDegree_adjoin_simple_eq_finrank_iff L E x (IsAlgebraic.of_finite L x)).2 <|
      IsSeparable.tower_top L (Algebra.IsSeparable.isSeparable F x)
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E_1 : Type v
inst : Field F
inst_1 : Field E_1
inst_2 : Algebra F E_1
E : Type v
inst_3 : Field E
inst_4 : Algebra F E
inst_5 : Algebra.IsSeparable F E
hfd : FiniteDimensional F E
L : IntermediateField F E
x : E
h : finSepDegree.{u, v} F ↥L = finrank.{u, v} F ↥L
heq : finSepDegree.{u, v} F ↥L * finSepDegree.{v, v} ↥L ↥(↥L)⟮x⟯ = finrank.{u, v} F ↥L * finrank.{v, v} ↥L ↥(↥L)⟮x⟯
⊢ finSepDegree.{u, v} F ↥(IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯) =
    finrank.{u, v} F ↥(IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯)
have set : let M : IntermediateField (↥L) E := (↥L)⟮x⟯;
∀ (heq : finSepDegree.{u, v} F ↥L * finSepDegree.{v, v} ↥L ↥M = finrank.{u, v} F ↥L * finrank.{v, v} ↥L ↥M),
  finSepDegree.{u, v} F ↥(IntermediateField.restrictScalars F M) =
    finrank.{u, v} F ↥(IntermediateField.restrictScalars F M)
Tactic: set M := L⟮x⟯
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E_1 : Type v
inst : Field F
inst_1 : Field E_1
inst_2 : Algebra F E_1
E : Type v
inst_3 : Field E
inst_4 : Algebra F E
inst_5 : Algebra.IsSeparable F E
hfd : FiniteDimensional F E
L : IntermediateField F E
x : E
h : finSepDegree.{u, v} F ↥L = finrank.{u, v} F ↥L
M : IntermediateField (↥L) E := (↥L)⟮x⟯
heq : finSepDegree.{u, v} F ↥L * finSepDegree.{v, v} ↥L ↥M = finrank.{u, v} F ↥L * finrank.{v, v} ↥L ↥M
⊢ finSepDegree.{u, v} F ↥(IntermediateField.restrictScalars F M) =
    finrank.{u, v} F ↥(IntermediateField.restrictScalars F M)
have rwa : ∀ (heq : finSepDegree.{u, v} F ↥M = finrank.{u, v} F ↥L * finrank.{v, v} ↥L ↥M),
  finSepDegree.{u, v} F ↥(IntermediateField.restrictScalars F M) =
    finrank.{u, v} F ↥(IntermediateField.restrictScalars F M)
Tactic: rwa [finSepDegree_mul_finSepDegree_of_isAlgebraic F L M,
    Module.finrank_mul_finrank F L M] at heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E_1 : Type v
inst : Field F
inst_1 : Field E_1
inst_2 : Algebra F E_1
E : Type v
inst_3 : Field E
inst_4 : Algebra F E
inst_5 : Algebra.IsSeparable F E
hfd : FiniteDimensional F E
L : IntermediateField F E
x : E
h : finSepDegree.{u, v} F ↥L = finrank.{u, v} F ↥L
M : IntermediateField (↥L) E := (↥L)⟮x⟯
heq : finSepDegree.{u, v} F ↥L * finSepDegree.{v, v} ↥L ↥M = finrank.{u, v} F ↥L * finrank.{v, v} ↥L ↥M
rwa :
  ∀ (heq : finSepDegree.{u, v} F ↥M = finrank.{u, v} F ↥L * finrank.{v, v} ↥L ↥M),
    finSepDegree.{u, v} F ↥(IntermediateField.restrictScalars F M) =
      finrank.{u, v} F ↥(IntermediateField.restrictScalars F M)
⊢ finSepDegree.{u, v} F ↥(IntermediateField.restrictScalars F M) =
    finrank.{u, v} F ↥(IntermediateField.restrictScalars F M)
have rwa₁ : ∀ (heq : finSepDegree.{u, v} F ↥M = finrank.{u, v} F ↥M),
  finSepDegree.{u, v} F ↥(IntermediateField.restrictScalars F M) =
    finrank.{u, v} F ↥(IntermediateField.restrictScalars F M)
Tactic: rwa [finSepDegree_mul_finSepDegree_of_isAlgebraic F L M,
    Module.finrank_mul_finrank F L M] at heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
heq : finSepDegree F E = finrank F E
x : E
⊢ IsSeparable F x
have halg : IsAlgebraic F x
Tactic: have halg := IsAlgebraic.of_finite F x
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
heq : finSepDegree F E = finrank F E
x : E
halg : IsAlgebraic F x
⊢ IsSeparable F x
have refine : ∀ (h : finSepDegree.{u, v} F ↥F⟮x⟯ < finrank.{u, v} F ↥F⟮x⟯), False
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_gt fun h ↦ ?_