awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
h : natSepDegree (minpoly F x) = 1
n : ℕ
y : F
hx : minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
⊢ ∃ (n : ℕ) (y : F),
    Eq.{v + 1} (α := E)
      ((Polynomial.aeval x : (a : F[X]) → E)
          (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])) :
        E)
      (0 : E)

Tactic:
⟨n, y, hx ▸ aeval F x⟩

Premises used: Eq.rec, minpoly.aeval, Exists.intro
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
h : natSepDegree (minpoly F x) = 1
n : ℕ
y : F
hx : minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
⊢ ∃ (n : ℕ) (y : F),
    Eq.{v + 1} (α := E)
      ((Polynomial.aeval x : (a : F[X]) → E)
          (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])) :
        E)
      (0 : E)

Tactic:
exact ⟨n, y, hx ▸ aeval F x⟩
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
h_1 :
  ∃ (n : ℕ) (y : F),
    Eq.{v + 1} (α := E)
      ((Polynomial.aeval x : (a : F[X]) → E)
          (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])) :
        E)
      (0 : E)
n : ℕ
y : F
h :
  Eq.{v + 1} (α := E)
    ((Polynomial.aeval x : (a : F[X]) → E)
        (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])) :
      E)
    (0 : E)
⊢ HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ≠ 0

Tactic:
have hnezero := X_pow_sub_C_ne_zero (expChar_pow_pos F q n) y
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
h_1 :
  ∃ (n : ℕ) (y : F),
    Eq.{v + 1} (α := E)
      ((Polynomial.aeval x : (a : F[X]) → E)
          (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])) :
        E)
      (0 : E)
n : ℕ
y : F
h :
  Eq.{v + 1} (α := E)
    ((Polynomial.aeval x : (a : F[X]) → E)
        (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])) :
      E)
    (0 : E)
hnezero : HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ≠ 0
⊢ natSepDegree (minpoly F x) = 1

Tactic:
((natSepDegree_le_of_dvd _ _ (minpoly.dvd F x h) hnezero).trans_eq <|
    natSepDegree_X_pow_char_pow_sub_C q n y).antisymm ?_

Premises used: LE.le.trans_eq, LE.le.antisymm, Polynomial.natSepDegree_X_pow_char_pow_sub_C, minpoly.dvd, Polynomial.natSepDegree_le_of_dvd
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
h_1 :
  ∃ (n : ℕ) (y : F),
    Eq.{v + 1} (α := E)
      ((Polynomial.aeval x : (a : F[X]) → E)
          (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])) :
        E)
      (0 : E)
n : ℕ
y : F
h :
  Eq.{v + 1} (α := E)
    ((Polynomial.aeval x : (a : F[X]) → E)
        (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])) :
      E)
    (0 : E)
hnezero : HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ≠ 0
convert_2 : 1 ≤ natSepDegree (minpoly F x)
⊢ natSepDegree (minpoly F x) = 1

Tactic:
refine ((natSepDegree_le_of_dvd _ _ (minpoly.dvd F x h) hnezero).trans_eq <|
    natSepDegree_X_pow_char_pow_sub_C q n y).antisymm ?_

Premises used: LE.le.trans_eq, LE.le.antisymm, Polynomial.natSepDegree_X_pow_char_pow_sub_C, minpoly.dvd, Polynomial.natSepDegree_le_of_dvd
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
h_1 :
  ∃ (n : ℕ) (y : F),
    Eq.{v + 1} (α := E)
      ((Polynomial.aeval x : (a : F[X]) → E)
          (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])) :
        E)
      (0 : E)
n : ℕ
y : F
h :
  Eq.{v + 1} (α := E)
    ((Polynomial.aeval x : (a : F[X]) → E)
        (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])) :
      E)
    (0 : E)
hnezero : HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ≠ 0
convert_2 : 1 ≤ natDegree (minpoly F x)
⊢ 1 ≤ natSepDegree (minpoly F x)

Tactic:
rw [Nat.one_le_iff_ne_zero, natSepDegree_ne_zero_iff, ← Nat.one_le_iff_ne_zero]

Premises used: Polynomial.natSepDegree_ne_zero_iff, Nat.one_le_iff_ne_zero
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
h_1 :
  ∃ (n : ℕ) (y : F),
    Eq.{v + 1} (α := E)
      ((Polynomial.aeval x : (a : F[X]) → E)
          (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])) :
        E)
      (0 : E)
n : ℕ
y : F
h :
  Eq.{v + 1} (α := E)
    ((Polynomial.aeval x : (a : F[X]) → E)
        (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])) :
      E)
    (0 : E)
hnezero : HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ≠ 0
⊢ 1 ≤ natDegree (minpoly F x)

Tactic:
minpoly.natDegree_pos <| IsAlgebraic.isIntegral ⟨_, hnezero, h⟩

Premises used: And.intro, IsAlgebraic.isIntegral, Exists.intro, minpoly.natDegree_pos, Nat.lt
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
h_1 :
  ∃ (n : ℕ) (y : F),
    Eq.{v + 1} (α := E)
      ((Polynomial.aeval x : (a : F[X]) → E)
          (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])) :
        E)
      (0 : E)
n : ℕ
y : F
h :
  Eq.{v + 1} (α := E)
    ((Polynomial.aeval x : (a : F[X]) → E)
        (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])) :
      E)
    (0 : E)
hnezero : HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ≠ 0
⊢ 1 ≤ natDegree (minpoly F x)

Tactic:
exact minpoly.natDegree_pos <| IsAlgebraic.isIntegral ⟨_, hnezero, h⟩

Premises used: And.intro, IsAlgebraic.isIntegral, Exists.intro, minpoly.natDegree_pos
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
⊢ ExpChar E q

Tactic:
haveI := expChar_of_injective_algebraMap (algebraMap F E).injective q
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this : ExpChar E q
⊢ ExpChar.{v} E[X] q

Tactic:
haveI := expChar_of_injective_ringHom (C_injective (R := E)) q
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
⊢ natSepDegree (minpoly F x) = 1 ↔
    ∃ (n : ℕ),
      Polynomial.map (algebraMap F E) (minpoly F x) =
        HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n

Tactic:
⟨fun h ↦ ?_, fun ⟨n, h⟩ ↦ (natSepDegree_eq_one_iff_pow_mem q).2 ?_⟩

Premises used: Iff.mpr, minpoly, Polynomial.natSepDegree, Iff.intro, minpoly.natSepDegree_eq_one_iff_pow_mem, _private.0.minpoly.natSepDegree_eq_one_iff_eq_X_sub_C_pow.match_1, OfNat.ofNat, Eq
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
refine_1 :
  ∀ (h : natSepDegree (minpoly F x) = 1),
    ∃ (n : ℕ),
      Polynomial.map (algebraMap F E) (minpoly F x) =
        HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
refine_2 :
  (∃ (n : ℕ),
      Polynomial.map (algebraMap F E) (minpoly F x) =
        HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n) →
    ∀ (n : ℕ)
      (h :
        Polynomial.map (algebraMap F E) (minpoly F x) =
          HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n),
      ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
⊢ natSepDegree (minpoly F x) = 1 ↔
    ∃ (n : ℕ),
      Polynomial.map (algebraMap F E) (minpoly F x) =
        HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨n, h⟩ ↦ (natSepDegree_eq_one_iff_pow_mem q).2 ?_⟩
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
h : natSepDegree (minpoly F x) = 1
refine_1 :
  ∀ (n : ℕ) (y : F)
    (h : minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])),
    ∃ (n : ℕ),
      Polynomial.map (algebraMap F E) (minpoly F x) =
        HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
⊢ ∃ (n : ℕ),
    Polynomial.map (algebraMap F E) (minpoly F x) =
      HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n

Tactic:
obtain ⟨n, y, h⟩ := (natSepDegree_eq_one_iff_eq_X_pow_sub_C q).1 h

Premises used: minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C, Iff.mp
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
h_1 : natSepDegree (minpoly F x) = 1
n : ℕ
y : F
h : minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
⊢ Eq.{v + 1} (α := E)
    ((Polynomial.aeval x : (a : F[X]) → E)
        (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])) :
      E)
    ((Polynomial.aeval x : (a : F[X]) → E) (minpoly F x) : E)

Tactic:
have hx := congr_arg (Polynomial.aeval x) h.symm
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
h_1 : natSepDegree (minpoly F x) = 1
n : ℕ
y : F
h : minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
hx :
  Eq.{v + 1} (α := E)
    ((Polynomial.aeval x : (a : F[X]) → E)
        (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])) :
      E)
    ((Polynomial.aeval x : (a : F[X]) → E) (minpoly F x) : E)
⊢ (algebraMap F E : (a : F) → E) y = x ^ q ^ n

Tactic:
rw [minpoly.aeval, map_sub, map_pow, aeval_X, aeval_C, sub_eq_zero, eq_comm] at hx

Premises used: map_sub, sub_eq_zero, map_pow, minpoly.aeval, eq_comm, Polynomial.aeval_C, Polynomial.aeval_X
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
h_1 : natSepDegree (minpoly F x) = 1
n : ℕ
y : F
h : minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
hx : (algebraMap F E : (a : F) → E) y = x ^ q ^ n
h₁ :
  Polynomial.map (algebraMap F E) (minpoly F x) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
⊢ ∃ (n : ℕ),
    Polynomial.map (algebraMap F E) (minpoly F x) =
      HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n

Tactic:
use n
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
h_1 : natSepDegree (minpoly F x) = 1
n : ℕ
y : F
h : minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
hx : (algebraMap F E : (a : F) → E) y = x ^ q ^ n
h₁ :
  Polynomial.map (algebraMap F E)
      (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₂ :
  HSub.hSub (α := E[X]) (Polynomial.map (algebraMap F E) (HPow.hPow (α := F[X]) X (q ^ n)))
      (Polynomial.map (algebraMap F E : F →+* E) ((C : (a : F) → F[X]) y)) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₃ :
  HPow.hPow (α := E[X]) (Polynomial.map (algebraMap F E : F →+* E) X) (q ^ n) -
      Polynomial.map (algebraMap F E : F →+* E) ((C : (a : F) → F[X]) y) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₄ :
  HPow.hPow (α := E[X]) X (q ^ n) - Polynomial.map (algebraMap F E : F →+* E) ((C : (a : F) → F[X]) y) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₅ :
  HSub.hSub (β := E[X]) (HPow.hPow (α := E[X]) X (q ^ n))
      ((C : (a : E) → E[X]) (((algebraMap F E : F →+* E) : (a : F) → E) y) : E[X]) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₆ :
  HSub.hSub (β := E[X]) (HPow.hPow (α := E[X]) X (q ^ n)) ((C : (a : E) → E[X]) (x ^ q ^ n) : E[X]) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₇ :
  HPow.hPow (α := E[X]) X (q ^ n) - HPow.hPow (α := E[X]) ((C : (a : E) → E[X]) x : E[X]) (q ^ n) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₈ h₉ :
  HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
⊢ Polynomial.map (algebraMap F E) (minpoly F x) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n

Tactic:
rw [h, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, hx, map_pow,
      ← sub_pow_expChar_pow_of_commute _ _ (commute_X _)]

Premises used: sub_pow_expChar_pow_of_commute, Polynomial.map_pow, Polynomial.map_X, map_pow, Polynomial.map_sub, Polynomial.map_C
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
h_1 :
  ∃ (n : ℕ),
    Polynomial.map (algebraMap F E) (minpoly F x) =
      HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
n : ℕ
h :
  Polynomial.map (algebraMap F E) (minpoly F x) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
⊢ Eq (α := E) ((constantCoeff : (a : E[X]) → E) (Polynomial.map (algebraMap F E) (minpoly F x)) : E)
    ((constantCoeff : (a : E[X]) → E) (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n) : E)

Tactic:
apply_fun constantCoeff at h

Premises used: Polynomial.constantCoeff
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
h_1 :
  ∃ (n : ℕ),
    Polynomial.map (algebraMap F E) (minpoly F x) =
      HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
n : ℕ
h :
  Eq (α := E) ((constantCoeff : (a : E[X]) → E) (Polynomial.map (algebraMap F E) (minpoly F x)) : E)
    ((constantCoeff : (a : E[X]) → E) (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n) : E)
⊢ (algebraMap F E : (a : F) → E) (coeff (minpoly F x) 0) = (0 - x) ^ q ^ n

Tactic:
simp_rw [map_pow, map_sub, constantCoeff_apply, coeff_map, coeff_X_zero, coeff_C_zero] at h

Premises used: Polynomial.coeff_map, map_sub, Polynomial.constantCoeff_apply, map_pow, Polynomial.coeff_X_zero, Polynomial.coeff_C_zero
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
h_1 :
  ∃ (n : ℕ),
    Polynomial.map (algebraMap F E) (minpoly F x) =
      HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
n : ℕ
h : (algebraMap F E : (a : F) → E) (coeff (minpoly F x) 0) = (0 - x) ^ q ^ n
⊢ (algebraMap F E : (a : F) → E) (coeff (minpoly F x) 0) = -1 * x ^ q ^ n

Tactic:
rw [zero_sub, neg_pow, neg_one_pow_expChar_pow] at h

Premises used: neg_pow, neg_one_pow_expChar_pow, zero_sub
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
h_1 :
  ∃ (n : ℕ),
    Polynomial.map (algebraMap F E) (minpoly F x) =
      HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
n : ℕ
h : (algebraMap F E : (a : F) → E) (coeff (minpoly F x) 0) = -1 * x ^ q ^ n
rw : -((algebraMap F E : F →+* E) : (a : F) → E) (coeff (minpoly F x) 0) = x ^ q ^ n
rw₁ : -(-1 * x ^ q ^ n) = x ^ q ^ n
rw₂ : - -(1 * x ^ q ^ n) = x ^ q ^ n
rw₃ : - -x ^ q ^ n = x ^ q ^ n
rw₄ rw₅ : x ^ q ^ n = x ^ q ^ n
⊢ ((algebraMap F E : F →+* E) : (a : F) → E) (-coeff (minpoly F x) 0) = x ^ q ^ n

Tactic:
rw [map_neg, h, neg_mul, one_mul, neg_neg]

Premises used: neg_neg, map_neg, neg_mul, one_mul
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
h_1 :
  ∃ (n : ℕ),
    Polynomial.map (algebraMap F E) (minpoly F x) =
      HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
n : ℕ
h : (algebraMap F E : (a : F) → E) (coeff (minpoly F x) 0) = -1 * x ^ q ^ n
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)

Tactic:
exact ⟨n, -(minpoly F x).coeff 0, by rw [map_neg, h, neg_mul, one_mul, neg_neg]⟩
-- 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 α
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ =
    Nat.card.{v}
      { x : AlgebraicClosure ↥F⟮α⟯ //
        Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x }

Tactic:
have : finSepDegree F F⟮α⟯ = _ := Nat.card_congr
    (algHomAdjoinIntegralEquiv F (K := AlgebraicClosure F⟮α⟯) 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 :
  finSepDegree.{u, v} F ↥F⟮α⟯ =
    Nat.card.{v}
      { x : AlgebraicClosure ↥F⟮α⟯ //
        Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x }
rw :
  Fintype.card.{v}
      { x : AlgebraicClosure ↥F⟮α⟯ //
        Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x } =
    Fintype.card.{v} ↥(Multiset.toFinset (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)))
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ = natSepDegree (minpoly F α)

Tactic:
rw [this, Nat.card_eq_fintype_card, natSepDegree_eq_of_isAlgClosed (E := AlgebraicClosure F⟮α⟯),
    ← Fintype.card_coe]

Premises used: Membership.mem, Subtype, IntermediateField.adjoin, Polynomial.natSepDegree_eq_of_isAlgClosed, Singleton.singleton, AlgebraicClosure, Fintype.card_coe, Nat.card_eq_fintype_card
-- 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 :
  finSepDegree.{u, v} F ↥F⟮α⟯ =
    Nat.card.{v}
      { x : AlgebraicClosure ↥F⟮α⟯ //
        Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x }
⊢ Fintype.card.{v}
      { x : AlgebraicClosure ↥F⟮α⟯ //
        Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x } =
    Fintype.card.{v} ↥(Multiset.toFinset (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)))

Tactic:
simp_rw [Multiset.mem_toFinset]

Premises used: Multiset.mem_toFinset
-- 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 :
  finSepDegree.{u, v} F ↥F⟮α⟯ =
    Nat.card.{v}
      { x : AlgebraicClosure ↥F⟮α⟯ //
        Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x }
rw :
  Nat.card.{v}
      { x : AlgebraicClosure ↥F⟮α⟯ //
        Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x } =
    natSepDegree (minpoly F α)
rw₁ :
  Fintype.card.{v}
      { x : AlgebraicClosure ↥F⟮α⟯ //
        Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x } =
    natSepDegree (minpoly F α)
rw₂ :
  Fintype.card.{v}
      { x : AlgebraicClosure ↥F⟮α⟯ //
        Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x } =
    Finset.card.{v} (α := AlgebraicClosure ↥F⟮α⟯) (Multiset.toFinset (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)))
rw₃ rw₄ rw₅ :
  Fintype.card.{v}
      { x : AlgebraicClosure ↥F⟮α⟯ //
        Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x } =
    Fintype.card.{v} ↥(Multiset.toFinset (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)))
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ = natSepDegree (minpoly F α)

Tactic:
classical
  rw [this, Nat.card_eq_fintype_card, natSepDegree_eq_of_isAlgClosed (E := AlgebraicClosure F⟮α⟯),
    ← Fintype.card_coe]
  simp_rw [Multiset.mem_toFinset]

Premises used: Membership.mem, Subtype, IntermediateField.adjoin, Polynomial.natSepDegree_eq_of_isAlgClosed, Singleton.singleton, AlgebraicClosure, Fintype.card_coe, Multiset.mem_toFinset, Nat.card_eq_fintype_card
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
pos : ∀ (halg : IsAlgebraic F α), finSepDegree.{u, v} F ↥F⟮α⟯ ∣ finrank.{u, v} F ↥F⟮α⟯
neg : ∀ (halg : ¬IsAlgebraic F α), finSepDegree.{u, v} F ↥F⟮α⟯ ∣ finrank.{u, v} F ↥F⟮α⟯
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ ∣ finrank.{u, v} F ↥F⟮α⟯

Tactic:
by_cases halg : IsAlgebraic F α

Premises used: 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 α
pos : natSepDegree (minpoly F α) ∣ natDegree (minpoly F α)
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ ∣ finrank.{u, v} F ↥F⟮α⟯

Tactic:
rw [finSepDegree_adjoin_simple_eq_natSepDegree F E halg, adjoin.finrank halg.isIntegral]

Premises used: IntermediateField.adjoin.finrank, IntermediateField.finSepDegree_adjoin_simple_eq_natSepDegree, IsAlgebraic.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 α
⊢ natSepDegree (minpoly F α) ∣ natDegree (minpoly F α)

Tactic:
(minpoly.irreducible halg.isIntegral).natSepDegree_dvd_natDegree

Premises used: Irreducible.natSepDegree_dvd_natDegree, IsAlgebraic.isIntegral, minpoly.irreducible
-- 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 α
⊢ natSepDegree (minpoly F α) ∣ natDegree (minpoly F α)

Tactic:
exact (minpoly.irreducible halg.isIntegral).natSepDegree_dvd_natDegree

Premises used: Irreducible.natSepDegree_dvd_natDegree, IsAlgebraic.isIntegral, minpoly.irreducible