awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
halg : ¬IsAlgebraic F α
⊢ finrank.{u, v} F ↥F⟮α⟯ = 0

Tactic:
have : finrank F F⟮α⟯ = 0 := finrank_of_infinite_dimensional fun _ ↦
    halg ((AdjoinSimple.isIntegral_gen F α).1 (IsIntegral.of_finite F _)).isAlgebraic
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
halg : ¬IsAlgebraic F α
this : finrank.{u, v} F ↥F⟮α⟯ = 0
neg : finSepDegree.{u, v} F ↥F⟮α⟯ ∣ 0
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ ∣ finrank.{u, v} F ↥F⟮α⟯

Tactic:
rw [this]
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
halg : ¬IsAlgebraic F α
this : finrank.{u, v} F ↥F⟮α⟯ = 0
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ ∣ 0

Tactic:
dvd_zero _

Premises used: dvd_zero
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
halg : ¬IsAlgebraic F α
this : finrank.{u, v} F ↥F⟮α⟯ = 0
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ ∣ 0

Tactic:
exact dvd_zero _

Premises used: dvd_zero
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
halg : IsAlgebraic F α
⊢ FiniteDimensional.{u, v} F ↥F⟮α⟯

Tactic:
haveI := adjoin.finiteDimensional halg.isIntegral
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
halg : IsAlgebraic F α
this : FiniteDimensional.{u, v} F ↥F⟮α⟯
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ ≤ finrank.{u, v} F ↥F⟮α⟯

Tactic:
Nat.le_of_dvd finrank_pos <| finSepDegree_adjoin_simple_dvd_finrank F E α

Premises used: _private.0.IntermediateField.finSepDegree_adjoin_simple_dvd_finrank, Nat.le_of_dvd, Module.finrank_pos
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
halg : IsAlgebraic F α
this : FiniteDimensional.{u, v} F ↥F⟮α⟯
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ ≤ finrank.{u, v} F ↥F⟮α⟯

Tactic:
exact Nat.le_of_dvd finrank_pos <| finSepDegree_adjoin_simple_dvd_finrank F E α

Premises used: _private.0.IntermediateField.finSepDegree_adjoin_simple_dvd_finrank, Nat.le_of_dvd, Module.finrank_pos
-- Module: Mathlib.FieldTheory.SeparableDegree
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 α
rw₃ rw₄ : Separable (minpoly F α) ↔ Separable (minpoly F α)
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ = finrank.{u, v} F ↥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]

Premises used: IntermediateField.adjoin.finrank, Polynomial.natSepDegree_eq_natDegree_iff, IntermediateField.finSepDegree_adjoin_simple_eq_natSepDegree, IsAlgebraic.isIntegral, IsSeparable, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.SeparableDegree
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
neg : ∀ (hfd : ¬FiniteDimensional F E), finSepDegree F E ∣ finrank F E
⊢ finSepDegree F E ∣ finrank F E

Tactic:
by_cases hfd : FiniteDimensional F E

Premises used: FiniteDimensional
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hfd : FiniteDimensional F E
pos : finSepDegree.{u, v} F ↥⊤ ∣ finrank.{u, v} F ↥⊤
⊢ finSepDegree F E ∣ finrank F E

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

Premises used: finrank_top, IntermediateField.finSepDegree_top
-- Module: Mathlib.FieldTheory.SeparableDegree
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 ↥⊥
simp_rw₃ : Dvd.dvd (α := ℕ) 1 1
⊢ finSepDegree.{u, v} F ↥⊥ ∣ finrank.{u, v} F ↥⊥

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

Premises used: IntermediateField.finrank_bot, one_dvd, IntermediateField.finSepDegree_bot
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hfd : FiniteDimensional F E
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⟯)
⊢ finSepDegree.{u, v} F ↥⊤ ∣ finrank.{u, v} 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 ↦ ?_) ⊤

Premises used: Dvd.dvd, Membership.mem, Field.finSepDegree, Subtype, Top.top, IntermediateField.induction_on_adjoin, Module.finrank
-- Module: Mathlib.FieldTheory.SeparableDegree
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 ↥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
-- Module: Mathlib.FieldTheory.SeparableDegree
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⟯
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)
⊢ finSepDegree.{u, v} F ↥(IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯) ∣
    finrank.{u, v} F ↥(IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯)

Tactic:
set M := L⟮x⟯
-- Module: Mathlib.FieldTheory.SeparableDegree
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)
pos₁ pos₂ pos₃ 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)
⊢ 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

Premises used: Membership.mem, Subtype, Field.finSepDegree_mul_finSepDegree_of_isAlgebraic, Module.finrank_mul_finrank
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
hfd : ¬FiniteDimensional F E
neg : finSepDegree F E ∣ 0
⊢ finSepDegree F E ∣ finrank F E

Tactic:
rw [finrank_of_infinite_dimensional hfd]

Premises used: Module.finrank_of_infinite_dimensional
-- Module: Mathlib.FieldTheory.SeparableDegree
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 ∣ 0

Tactic:
dvd_zero _

Premises used: dvd_zero
-- Module: Mathlib.FieldTheory.SeparableDegree
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 ∣ 0

Tactic:
exact dvd_zero _

Premises used: dvd_zero
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
⊢ finSepDegree F E ≤ finrank F E

Tactic:
Nat.le_of_dvd finrank_pos <| finSepDegree_dvd_finrank F E

Premises used: Field.finSepDegree_dvd_finrank, Nat.le_of_dvd, Module.finrank_pos
-- Module: Mathlib.FieldTheory.SeparableDegree
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
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
⊢ finSepDegree F E = finrank F E

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

Premises used: FiniteDimensional
-- Module: Mathlib.FieldTheory.SeparableDegree
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
inr : finSepDegree F E = 0
⊢ finSepDegree F E = finrank F E

Tactic:
rw [finrank_of_infinite_dimensional hfd]

Premises used: Module.finrank_of_infinite_dimensional
-- Module: Mathlib.FieldTheory.SeparableDegree
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
inr :
  ∀ (L : IntermediateField F E) (h : FiniteDimensional.{u, v} F ↥L) (h' : finSepDegree F E < finrank.{u, v} F ↥L),
    finSepDegree F E = 0
⊢ finSepDegree F E = 0

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

Premises used: Field.finSepDegree, IntermediateField.exists_lt_finrank_of_infinite_dimensional
-- Module: Mathlib.FieldTheory.SeparableDegree
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.{u, v} F ↥L * finSepDegree (↥L) E = finSepDegree F E

Tactic:
have hd := finSepDegree_mul_finSepDegree_of_isAlgebraic F L E
-- Module: Mathlib.FieldTheory.SeparableDegree
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
⊢ finrank.{u, v} F ↥L * finSepDegree (↥L) E = finSepDegree F E

Tactic:
rw [H L h] at hd

Premises used: Membership.mem, Subtype
-- Module: Mathlib.FieldTheory.SeparableDegree
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
neg : ∀ (hd' : ¬finSepDegree (↥L) E = 0), finSepDegree F E = 0
⊢ finSepDegree F E = 0

Tactic:
by_cases hd' : finSepDegree L E = 0

Premises used: Membership.mem, Field.finSepDegree, Subtype
-- Module: Mathlib.FieldTheory.SeparableDegree
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
pos₂ pos₃ : Eq (α := ℕ) 0 0
⊢ finSepDegree F E = 0

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

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.FieldTheory.SeparableDegree
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
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
⊢ finSepDegree F E = 0

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

Premises used: Nat.le_mul_of_pos_right, Membership.mem, Subtype, Nat.pos_of_ne_zero, Module.finrank
-- Module: Mathlib.FieldTheory.SeparableDegree
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
rw : finSepDegree.{u, v} F ↥⊤ = finrank.{u, v} F ↥⊤
⊢ finSepDegree F E = finrank F E

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

Premises used: finrank_top, IntermediateField.finSepDegree_top
-- Module: Mathlib.FieldTheory.SeparableDegree
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 ↥⊥
simp_rw₂ : 1 = finrank.{u, v} F ↥⊥
⊢ finSepDegree.{u, v} F ↥⊥ = finrank.{u, v} F ↥⊥

Tactic:
simp_rw [finSepDegree_bot, IntermediateField.finrank_bot]

Premises used: IntermediateField.finrank_bot, IntermediateField.finSepDegree_bot
-- Module: Mathlib.FieldTheory.SeparableDegree
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
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⟯)
⊢ finSepDegree.{u, v} F ↥⊤ = finrank.{u, v} 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 ↦ ?_) ⊤

Premises used: Membership.mem, Field.finSepDegree, Subtype, Top.top, Eq, IntermediateField.induction_on_adjoin, Module.finrank
-- Module: Mathlib.FieldTheory.SeparableDegree
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 ↥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)
-- Module: Mathlib.FieldTheory.SeparableDegree
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⟯
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)
⊢ finSepDegree.{u, v} F ↥(IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯) =
    finrank.{u, v} F ↥(IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯)

Tactic:
set M := L⟮x⟯
-- Module: Mathlib.FieldTheory.SeparableDegree
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)
rwa₁ rwa₂ rwa₃ 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)
⊢ 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

Premises used: Membership.mem, Subtype, Field.finSepDegree_mul_finSepDegree_of_isAlgebraic, Module.finrank_mul_finrank
-- Module: Mathlib.FieldTheory.SeparableDegree
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
⊢ IsAlgebraic F x

Tactic:
have halg := IsAlgebraic.of_finite F x
-- Module: Mathlib.FieldTheory.SeparableDegree
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

Tactic:
(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 ↦ ?_

Premises used: IntermediateField.finSepDegree_adjoin_simple_eq_finrank_iff, le_of_not_gt, IntermediateField.finSepDegree_adjoin_simple_le_finrank, le_antisymm, Iff.mp
-- Module: Mathlib.FieldTheory.SeparableDegree
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
refine : ∀ (h : finSepDegree.{u, v} F ↥F⟮x⟯ < finrank.{u, v} F ↥F⟮x⟯), False
⊢ 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_gt fun h ↦ ?_

Premises used: IntermediateField.finSepDegree_adjoin_simple_eq_finrank_iff, le_of_not_gt, IntermediateField.finSepDegree_adjoin_simple_le_finrank, le_antisymm, Iff.mp
-- Module: Mathlib.FieldTheory.SeparableDegree
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
h : finSepDegree.{u, v} F ↥F⟮x⟯ < finrank.{u, v} F ↥F⟮x⟯
⊢ finSepDegree.{u, v} F ↥F⟮x⟯ * finSepDegree (↥F⟮x⟯) E < finrank.{u, v} F ↥F⟮x⟯ * finrank (↥F⟮x⟯) E

Tactic:
have := Nat.mul_lt_mul_of_lt_of_le' h (finSepDegree_le_finrank F⟮x⟯ E) Fin.pos'
-- Module: Mathlib.FieldTheory.SeparableDegree
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
h : finSepDegree.{u, v} F ↥F⟮x⟯ < finrank.{u, v} F ↥F⟮x⟯
this : finSepDegree.{u, v} F ↥F⟮x⟯ * finSepDegree (↥F⟮x⟯) E < finrank.{u, v} F ↥F⟮x⟯ * finrank (↥F⟮x⟯) E
⊢ finSepDegree F E < finrank F E

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

Premises used: Membership.mem, Subtype, Field.finSepDegree_mul_finSepDegree_of_isAlgebraic, Module.finrank_mul_finrank, IntermediateField.adjoin, Singleton.singleton
-- Module: Mathlib.FieldTheory.SeparableDegree
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
h : finSepDegree.{u, v} F ↥F⟮x⟯ < finrank.{u, v} F ↥F⟮x⟯
this : finSepDegree F E < finrank F E
linarith :
  -1 + -HSub.hSub (α := ℤ) (↑(finSepDegree F E) : ℤ) (↑(finrank F E) : ℤ) +
      (HAdd.hAdd (α := ℤ) (↑(finSepDegree F E) : ℤ) 1 - (↑(finrank F E) : ℤ)) =
    0
⊢ False

Tactic:
linarith only [heq, this]
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : IntermediateField F E
inst_3 : Algebra.IsSeparable.{u, v} F ↥L
x : E
h : x ∈ L
⊢ IsSeparable F x

Tactic:
simpa only [IsSeparable, minpoly_eq] using Algebra.IsSeparable.isSeparable F (K := L) ⟨x, h⟩

Premises used: Algebra.IsSeparable.isSeparable, Subtype.mk, IntermediateField.minpoly_eq, IsSeparable
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
⊢ Algebra.IsSeparable.{u, v} F ↥F⟮x⟯ ↔ IsSeparable F x

Tactic:
⟨fun _ ↦ ?_, fun hsep ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
refine_1 : Algebra.IsSeparable.{u, v} F ↥F⟮x⟯ → IsSeparable F x
refine_2 : ∀ (hsep : IsSeparable F x), Algebra.IsSeparable.{u, v} F ↥F⟮x⟯
⊢ Algebra.IsSeparable.{u, v} F ↥F⟮x⟯ ↔ IsSeparable F x

Tactic:
refine ⟨fun _ ↦ ?_, fun hsep ↦ ?_⟩
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
h : Algebra.IsSeparable.{u, v} F ↥F⟮x⟯
⊢ IsSeparable F x

Tactic:
isSeparable_of_mem_isSeparable F E <| mem_adjoin_simple_self F x

Premises used: IntermediateField.isSeparable_of_mem_isSeparable, IntermediateField.mem_adjoin_simple_self