awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
F_inf : IsEmpty.{u_1 + 1} (Fintype F)
P : IntermediateField F E → Prop := fun (K : IntermediateField F E) ↦ ∃ (α : E), F⟮α⟯ = K
base : P ⊥
ih : ∀ (K : IntermediateField F E) (x : E), P K → P (IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
⊢ ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤

Tactic:
induction_on_adjoin P base ih ⊤

Premises used: Top.top, IntermediateField.induction_on_adjoin
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
F_inf : IsEmpty.{u_1 + 1} (Fintype F)
P : IntermediateField F E → Prop := fun (K : IntermediateField F E) ↦ ∃ (α : E), F⟮α⟯ = K
base : P ⊥
ih : ∀ (K : IntermediateField F E) (x : E), P K → P (IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
⊢ ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤

Tactic:
exact induction_on_adjoin P base ih ⊤

Premises used: Top.top, IntermediateField.induction_on_adjoin
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
F_finite : Fintype F
⊢ ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤

Tactic:
exact exists_primitive_element_of_finite_bot F E

Premises used: Field.exists_primitive_element_of_finite_bot
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
inr :
  ∀
    (this :
      ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_3 : Field E] [inst_4 : Algebra F E] {α : E} {m n : ℕ}
        (hneq : m ≠ n) (heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯) (hmn : m < n), IsAlgebraic F α)
    (hmn : ¬m < n), IsAlgebraic F α
wlog :
  ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_3 : Field E] [inst_4 : Algebra F E] {α : E} {m n : ℕ}
    (hneq : m ≠ n) (heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯) (hmn : m < n), IsAlgebraic F α
⊢ IsAlgebraic F α

Tactic:
wlog hmn : m < n
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
this :
  ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_3 : Field E] [inst_4 : Algebra F E] {α : E} {m n : ℕ}
    (hneq : m ≠ n) (heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯) (hmn : m < n), IsAlgebraic F α
hmn : ¬m < n
⊢ IsAlgebraic F α

Tactic:
this F E hneq.symm heq.symm (hneq.lt_or_gt.resolve_left hmn)

Premises used: Or.resolve_left, Ne.symm, Eq.symm, Ne.lt_or_gt
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
this :
  ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_3 : Field E] [inst_4 : Algebra F E] {α : E} {m n : ℕ}
    (hneq : m ≠ n) (heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯) (hmn : m < n), IsAlgebraic F α
hmn : ¬m < n
⊢ IsAlgebraic F α

Tactic:
exact this F E hneq.symm heq.symm (hneq.lt_or_gt.resolve_left hmn)

Premises used: Or.resolve_left, Ne.symm, Eq.symm, Ne.lt_or_gt
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
pos : ∀ (hm : m = 0), IsAlgebraic F α
neg : ∀ (hm : ¬m = 0), IsAlgebraic F α
⊢ IsAlgebraic F α

Tactic:
by_cases hm : m = 0
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
hm : m = 0
⊢ Eq (α := IntermediateField F E) F⟮HPow.hPow (β := ℕ) α 0⟯ F⟮α ^ n⟯

Tactic:
rw [hm] at heq hmn
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
hm : m = 0
heq₁ : Eq (α := IntermediateField F E) F⟮HPow.hPow (β := ℕ) α 0⟯ F⟮α ^ n⟯
⊢ 0 < n

Tactic:
rw [hm] at heq hmn
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
hm : m = 0
heq₁ : Eq (α := IntermediateField F E) F⟮HPow.hPow (β := ℕ) α 0⟯ F⟮α ^ n⟯
hmn₁ : 0 < n
⊢ m = 0

Tactic:
rw [hm] at heq hmn
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮HPow.hPow (β := ℕ) α 0⟯ F⟮α ^ n⟯
hmn : 0 < n
hm : m = 0
⊢ Eq (α := IntermediateField F E) ⊥ F⟮α ^ n⟯

Tactic:
simp only [pow_zero, adjoin_one] at heq

Premises used: IntermediateField.adjoin_one, pow_zero
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
hmn : 0 < n
hm : m = 0
heq : Eq (α := IntermediateField F E) ⊥ F⟮α ^ n⟯
pos : ∀ (y : F) (h : (algebraMap F E : (a : F) → E) y = α ^ n), IsAlgebraic F α
⊢ IsAlgebraic F α

Tactic:
obtain ⟨y, h⟩ := mem_bot.1 (heq.symm ▸ mem_adjoin_simple_self F (α ^ n))

Premises used: Iff.mp, IntermediateField.mem_bot
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
hmn : 0 < n
hm : m = 0
heq : Eq (α := IntermediateField F E) ⊥ F⟮α ^ n⟯
y : F
h : (algebraMap F E : (a : F) → E) y = α ^ n
⊢ IsAlgebraic F α

Tactic:
⟨X ^ n - C y, X_pow_sub_C_ne_zero hmn y, ?_⟩

Premises used: Polynomial.C, IsAlgebraic, HSub.hSub, HPow.hPow, And.intro, Exists.intro, Polynomial.X, DFunLike.coe, Polynomial.X_pow_sub_C_ne_zero
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
hmn : 0 < n
hm : m = 0
heq : Eq (α := IntermediateField F E) ⊥ F⟮α ^ n⟯
y : F
h : (algebraMap F E : (a : F) → E) y = α ^ n
pos :
  Eq.{u_2 + 1} (α := E)
    ((aeval α : (a : F[X]) → E) (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) y : F[X])) : E)
    (0 : E)
⊢ IsAlgebraic F α

Tactic:
refine ⟨X ^ n - C y, X_pow_sub_C_ne_zero hmn y, ?_⟩
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
hmn : 0 < n
hm : m = 0
heq : Eq (α := IntermediateField F E) ⊥ F⟮α ^ n⟯
y : F
h : (algebraMap F E : (a : F) → E) y = α ^ n
⊢ Eq.{u_2 + 1} (α := E)
    ((aeval α : (a : F[X]) → E) (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) y : F[X])) : E)
    (0 : E)

Tactic:
simp only [map_sub, map_pow, aeval_X, aeval_C, h, sub_self]

Premises used: map_sub, sub_self, map_pow, Polynomial.aeval_C, Polynomial.aeval_X
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
hm : ¬m = 0
neg :
  ∀ (r s : F[X])
    (h :
      α ^ m =
        HDiv.hDiv (α := E) (β := E) ((aeval (α ^ n) : (a : F[X]) → E) r : E) ((aeval (α ^ n) : (a : F[X]) → E) s : E)),
    IsAlgebraic F α
⊢ IsAlgebraic F α

Tactic:
obtain ⟨r, s, h⟩ := (mem_adjoin_simple_iff F _).1 (heq ▸ mem_adjoin_simple_self F (α ^ m))

Premises used: Iff.mp, IntermediateField.mem_adjoin_simple_iff
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
hm : ¬m = 0
r s : F[X]
h :
  α ^ m = HDiv.hDiv (α := E) (β := E) ((aeval (α ^ n) : (a : F[X]) → E) r : E) ((aeval (α ^ n) : (a : F[X]) → E) s : E)
pos : ∀ (hzero : Eq.{u_2 + 1} (α := E) ((aeval (α ^ n) : (a : F[X]) → E) s : E) (0 : E)), IsAlgebraic F α
neg : ∀ (hzero : ¬Eq.{u_2 + 1} (α := E) ((aeval (α ^ n) : (a : F[X]) → E) s : E) (0 : E)), IsAlgebraic F α
⊢ IsAlgebraic F α

Tactic:
by_cases hzero : aeval (α ^ n) s = 0

Premises used: HPow.hPow, Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
hm : ¬m = 0
r s : F[X]
h :
  α ^ m = HDiv.hDiv (α := E) (β := E) ((aeval (α ^ n) : (a : F[X]) → E) r : E) ((aeval (α ^ n) : (a : F[X]) → E) s : E)
hzero : Eq.{u_2 + 1} (α := E) ((aeval (α ^ n) : (a : F[X]) → E) s : E) (0 : E)
⊢ α = 0

Tactic:
simp only [hzero, div_zero, pow_eq_zero_iff hm] at h

Premises used: pow_eq_zero_iff, div_zero
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
hm : ¬m = 0
r s : F[X]
hzero : Eq.{u_2 + 1} (α := E) ((aeval (α ^ n) : (a : F[X]) → E) s : E) (0 : E)
h : α = 0
⊢ IsAlgebraic F α

Tactic:
h.symm ▸ isAlgebraic_zero

Premises used: Eq.rec, isAlgebraic_zero, Eq.symm
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
hm : ¬m = 0
r s : F[X]
hzero : Eq.{u_2 + 1} (α := E) ((aeval (α ^ n) : (a : F[X]) → E) s : E) (0 : E)
h : α = 0
⊢ IsAlgebraic F α

Tactic:
exact h.symm ▸ isAlgebraic_zero
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
hm : ¬m = 0
r s : F[X]
h :
  α ^ m = HDiv.hDiv (α := E) (β := E) ((aeval (α ^ n) : (a : F[X]) → E) r : E) ((aeval (α ^ n) : (a : F[X]) → E) s : E)
hzero : ¬Eq.{u_2 + 1} (α := E) ((aeval (α ^ n) : (a : F[X]) → E) s : E) (0 : E)
⊢ 0 < m

Tactic:
replace hm : 0 < m := Nat.pos_of_ne_zero hm
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h :
  α ^ m = HDiv.hDiv (α := E) (β := E) ((aeval (α ^ n) : (a : F[X]) → E) r : E) ((aeval (α ^ n) : (a : F[X]) → E) s : E)
hzero : ¬Eq.{u_2 + 1} (α := E) ((aeval (α ^ n) : (a : F[X]) → E) s : E) (0 : E)
hm : 0 < m
⊢ HSub.hSub (β := E) (HMul.hMul (β := E) (α ^ m) ((aeval (α ^ n) : (a : F[X]) → E) s : E))
      ((aeval (α ^ n) : (a : F[X]) → E) r : E) =
    0

Tactic:
rw [eq_div_iff hzero, ← sub_eq_zero] at h

Premises used: sub_eq_zero, eq_div_iff
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h :
  α ^ m = HDiv.hDiv (α := E) (β := E) ((aeval (α ^ n) : (a : F[X]) → E) r : E) ((aeval (α ^ n) : (a : F[X]) → E) s : E)
hzero : ¬Eq.{u_2 + 1} (α := E) ((aeval (α ^ n) : (a : F[X]) → E) s : E) (0 : E)
hm : 0 < m
h₁ :
  HSub.hSub (β := E) (HMul.hMul (β := E) (α ^ m) ((aeval (α ^ n) : (a : F[X]) → E) s : E))
      ((aeval (α ^ n) : (a : F[X]) → E) r : E) =
    0
⊢ ¬Eq.{u_2 + 1} (α := E) ((aeval (α ^ n) : (a : F[X]) → E) s : E) (0 : E)

Tactic:
rw [eq_div_iff hzero, ← sub_eq_zero] at h

Premises used: sub_eq_zero, eq_div_iff
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h :
  α ^ m = HDiv.hDiv (α := E) (β := E) ((aeval (α ^ n) : (a : F[X]) → E) r : E) ((aeval (α ^ n) : (a : F[X]) → E) s : E)
hzero : ¬Eq.{u_2 + 1} (α := E) ((aeval (α ^ n) : (a : F[X]) → E) s : E) (0 : E)
hm : 0 < m
h₁ :
  HSub.hSub (β := E) (HMul.hMul (β := E) (α ^ m) ((aeval (α ^ n) : (a : F[X]) → E) s : E))
      ((aeval (α ^ n) : (a : F[X]) → E) r : E) =
    0
hzero₁ : ¬Eq.{u_2 + 1} (α := E) ((aeval (α ^ n) : (a : F[X]) → E) s : E) (0 : E)
⊢ 0 < m

Tactic:
rw [eq_div_iff hzero, ← sub_eq_zero] at h

Premises used: sub_eq_zero, eq_div_iff
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
r : F[X]
hm : 0 < m
h :
  HSub.hSub (β := E) (HMul.hMul (β := E) (α ^ m) ((aeval (α ^ n) : (a : F[X]) → E) 0 : E))
      ((aeval (α ^ n) : (a : F[X]) → E) r : E) =
    0
hzero : ¬Eq.{u_2 + 1} (α := E) ((aeval (α ^ n) : (a : F[X]) → E) 0 : E) (0 : E)
⊢ False

Tactic:
simp only [map_zero, not_true_eq_false] at hzero

Premises used: map_zero, not_true_eq_false
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h :
  HSub.hSub (β := E) (HMul.hMul (β := E) (α ^ m) ((aeval (α ^ n) : (a : F[X]) → E) s : E))
      ((aeval (α ^ n) : (a : F[X]) → E) r : E) =
    0
hzero : ¬Eq.{u_2 + 1} (α := E) ((aeval (α ^ n) : (a : F[X]) → E) s : E) (0 : E)
hm : 0 < m
⊢ s ≠ 0

Tactic:
replace hzero : s ≠ 0 := by rintro rfl; simp only [map_zero, not_true_eq_false] at hzero
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h :
  HSub.hSub (β := E) (HMul.hMul (β := E) (α ^ m) ((aeval (α ^ n) : (a : F[X]) → E) s : E))
      ((aeval (α ^ n) : (a : F[X]) → E) r : E) =
    0
hm : 0 < m
hzero : s ≠ 0
f : F[X] :=
  HSub.hSub (β := F[X]) (HMul.hMul (β := F[X]) (HPow.hPow (α := F[X]) X m) ((expand F n : (a : F[X]) → F[X]) s : F[X]))
    ((expand F n : (a : F[X]) → F[X]) r : F[X])
⊢ IsAlgebraic F α

Tactic:
⟨f, ?_, ?_⟩

Premises used: IsAlgebraic, And.intro, Exists.intro
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h :
  HSub.hSub (β := E) (HMul.hMul (β := E) (α ^ m) ((aeval (α ^ n) : (a : F[X]) → E) s : E))
      ((aeval (α ^ n) : (a : F[X]) → E) r : E) =
    0
hm : 0 < m
hzero : s ≠ 0
f : F[X] :=
  HSub.hSub (β := F[X]) (HMul.hMul (β := F[X]) (HPow.hPow (α := F[X]) X m) ((expand F n : (a : F[X]) → F[X]) s : F[X]))
    ((expand F n : (a : F[X]) → F[X]) r : F[X])
neg : f ≠ 0
neg₁ : Eq.{u_2 + 1} (α := E) ((aeval α : (a : F[X]) → E) f : E) (0 : E)
⊢ IsAlgebraic F α

Tactic:
refine ⟨f, ?_, ?_⟩
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h :
  HSub.hSub (β := E) (HMul.hMul (β := E) (α ^ m) ((aeval (α ^ n) : (a : F[X]) → E) s : E))
      ((aeval (α ^ n) : (a : F[X]) → E) r : E) =
    0
hm : 0 < m
hzero : s ≠ 0
f : F[X] :=
  HSub.hSub (β := F[X]) (HMul.hMul (β := F[X]) (HPow.hPow (α := F[X]) X m) ((expand F n : (a : F[X]) → F[X]) s : F[X]))
    ((expand F n : (a : F[X]) → F[X]) r : F[X])
linarith :
  n ≤ 0 →
    HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) (↑n : ℤ) 0 + (HAdd.hAdd (α := ℤ) 0 1 - (↑m : ℤ)) +
        (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 - (↑n : ℤ)) =
      0
linarith₁ : n ≤ 0 → GT.gt (α := ℤ) 2 0
⊢ 0 < n

Tactic:
linarith only [hm, hmn]
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h :
  HSub.hSub (β := E) (HMul.hMul (β := E) (α ^ m) ((aeval (α ^ n) : (a : F[X]) → E) s : E))
      ((aeval (α ^ n) : (a : F[X]) → E) r : E) =
    0
hm : 0 < m
hzero : s ≠ 0
f : F[X] :=
  HSub.hSub (β := F[X]) (HMul.hMul (β := F[X]) (HPow.hPow (α := F[X]) X m) ((expand F n : (a : F[X]) → F[X]) s : F[X]))
    ((expand F n : (a : F[X]) → F[X]) r : F[X])
⊢ 0 < n

Tactic:
have hn : 0 < n := by linarith only [hm, hmn]
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h :
  HSub.hSub (β := E) (HMul.hMul (β := E) (α ^ m) ((aeval (α ^ n) : (a : F[X]) → E) s : E))
      ((aeval (α ^ n) : (a : F[X]) → E) r : E) =
    0
hm : 0 < m
hzero : s ≠ 0
f : F[X] :=
  HSub.hSub (β := F[X]) (HMul.hMul (β := F[X]) (HPow.hPow (α := F[X]) X m) ((expand F n : (a : F[X]) → F[X]) s : F[X]))
    ((expand F n : (a : F[X]) → F[X]) r : F[X])
hn : 0 < n
rw : ¬n ∣ m
⊢ ¬n ∣ n * s.natDegree + m

Tactic:
rw [← Nat.dvd_add_iff_right (n.dvd_mul_right s.natDegree)]

Premises used: Nat.dvd_mul_right, Polynomial.natDegree, Nat.dvd_add_iff_right
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h :
  HSub.hSub (β := E) (HMul.hMul (β := E) (α ^ m) ((aeval (α ^ n) : (a : F[X]) → E) s : E))
      ((aeval (α ^ n) : (a : F[X]) → E) r : E) =
    0
hm : 0 < m
hzero : s ≠ 0
f : F[X] :=
  HSub.hSub (β := F[X]) (HMul.hMul (β := F[X]) (HPow.hPow (α := F[X]) X m) ((expand F n : (a : F[X]) → F[X]) s : F[X]))
    ((expand F n : (a : F[X]) → F[X]) r : F[X])
hn : 0 < n
⊢ ¬n ∣ m

Tactic:
Nat.not_dvd_of_pos_of_lt hm hmn

Premises used: Nat.not_dvd_of_pos_of_lt
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h :
  HSub.hSub (β := E) (HMul.hMul (β := E) (α ^ m) ((aeval (α ^ n) : (a : F[X]) → E) s : E))
      ((aeval (α ^ n) : (a : F[X]) → E) r : E) =
    0
hm : 0 < m
hzero : s ≠ 0
f : F[X] :=
  HSub.hSub (β := F[X]) (HMul.hMul (β := F[X]) (HPow.hPow (α := F[X]) X m) ((expand F n : (a : F[X]) → F[X]) s : F[X]))
    ((expand F n : (a : F[X]) → F[X]) r : F[X])
hn : 0 < n
⊢ ¬n ∣ m

Tactic:
exact Nat.not_dvd_of_pos_of_lt hm hmn

Premises used: Nat.not_dvd_of_pos_of_lt
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h :
  HSub.hSub (β := E) (HMul.hMul (β := E) (α ^ m) ((aeval (α ^ n) : (a : F[X]) → E) s : E))
      ((aeval (α ^ n) : (a : F[X]) → E) r : E) =
    0
hm : 0 < m
hzero : s ≠ 0
f : F[X] :=
  HSub.hSub (β := F[X]) (HMul.hMul (β := F[X]) (HPow.hPow (α := F[X]) X m) ((expand F n : (a : F[X]) → F[X]) s : F[X]))
    ((expand F n : (a : F[X]) → F[X]) r : F[X])
hn : 0 < n
⊢ ¬n ∣ n * s.natDegree + m

Tactic:
have hndvd : ¬ n ∣ n * s.natDegree + m := by
        rw [← Nat.dvd_add_iff_right (n.dvd_mul_right s.natDegree)]
        exact Nat.not_dvd_of_pos_of_lt hm hmn
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h :
  HSub.hSub (β := E) (HMul.hMul (β := E) (α ^ m) ((aeval (α ^ n) : (a : F[X]) → E) s : E))
      ((aeval (α ^ n) : (a : F[X]) → E) r : E) =
    0
hm : 0 < m
hzero : s ≠ 0
f : F[X] :=
  HSub.hSub (β := F[X]) (HMul.hMul (β := F[X]) (HPow.hPow (α := F[X]) X m) ((expand F n : (a : F[X]) → F[X]) s : F[X]))
    ((expand F n : (a : F[X]) → F[X]) r : F[X])
hn : 0 < n
hndvd : ¬n ∣ n * s.natDegree + m
simp : s.leadingCoeff ≠ 0
⊢ f.coeff (n * s.natDegree + m) ≠ 0

Tactic:
simp only [f, coeff_sub, coeff_X_pow_mul, s.coeff_expand_mul' hn, coeff_natDegree,
        coeff_expand hn r, hndvd, ite_false, sub_zero]

Premises used: Polynomial.coeff_natDegree, ite_false, sub_zero, Polynomial.coeff_X_pow_mul, Polynomial.coeff_sub, Polynomial.coeff_expand, Polynomial.coeff_expand_mul'