awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H : n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)
hp : p = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
⊢ ∃ (m : ℕ) (n : ℕ) (y : F),
    m ≠ 0 ∧
      (n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)) ∧
        f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m

Tactic:
⟨_, n, y, hne, H, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H : n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)
hp : p = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
refine : f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ multiplicity p f
⊢ ∃ (m : ℕ) (n : ℕ) (y : F),
    m ≠ 0 ∧
      (n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)) ∧
        f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m

Tactic:
refine ⟨_, n, y, hne, H, ?_⟩
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H : n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)
hp : p = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
obtain :
  ∀ (c : F[X]) (hf : f = p ^ multiplicity p f * c) (H : ¬p ∣ c),
    f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ multiplicity p f
⊢ f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ multiplicity p f

Tactic:
obtain ⟨c, hf, H⟩ := hF.exists_eq_pow_mul_and_not_dvd

Premises used: FiniteMultiplicity.exists_eq_pow_mul_and_not_dvd
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf_1 : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H_1 : n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)
hp : p = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
c : F[X]
hf : f = p ^ multiplicity p f * c
H : ¬p ∣ c
⊢ c.natDegree = 0

Tactic:
rw [hf, natSepDegree_mul_of_isCoprime _ c <| IsCoprime.pow_left <|
    (hI.isCoprime_or_dvd c).resolve_right H, natSepDegree_pow_of_ne_zero _ hne, hD,
    add_eq_left, natSepDegree_eq_zero_iff] at h

Premises used: IsCoprime.pow_left, Polynomial.natSepDegree_eq_zero_iff, Polynomial.natSepDegree_pow_of_ne_zero, add_eq_left, Irreducible.isCoprime_or_dvd, Polynomial.natSepDegree_mul_of_isCoprime, Or.resolve_right
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf_1 : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H_1 : n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)
hp : p = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
c : F[X]
hf : f = p ^ multiplicity p f * c
H : ¬p ∣ c
h₁ : c.natDegree = 0
⊢ f = p ^ multiplicity p f * c

Tactic:
rw [hf, natSepDegree_mul_of_isCoprime _ c <| IsCoprime.pow_left <|
    (hI.isCoprime_or_dvd c).resolve_right H, natSepDegree_pow_of_ne_zero _ hne, hD,
    add_eq_left, natSepDegree_eq_zero_iff] at h

Premises used: IsCoprime.pow_left, Polynomial.natSepDegree_eq_zero_iff, Polynomial.natSepDegree_pow_of_ne_zero, add_eq_left, Irreducible.isCoprime_or_dvd, Polynomial.natSepDegree_mul_of_isCoprime, Or.resolve_right
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf_1 : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H_1 : n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)
hp : p = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
c : F[X]
hf : f = p ^ multiplicity p f * c
H : ¬p ∣ c
h₁ : c.natDegree = 0
hf₁ : f = p ^ multiplicity p f * c
⊢ ¬p ∣ c

Tactic:
rw [hf, natSepDegree_mul_of_isCoprime _ c <| IsCoprime.pow_left <|
    (hI.isCoprime_or_dvd c).resolve_right H, natSepDegree_pow_of_ne_zero _ hne, hD,
    add_eq_left, natSepDegree_eq_zero_iff] at h

Premises used: IsCoprime.pow_left, Polynomial.natSepDegree_eq_zero_iff, Polynomial.natSepDegree_pow_of_ne_zero, add_eq_left, Irreducible.isCoprime_or_dvd, Polynomial.natSepDegree_mul_of_isCoprime, Or.resolve_right
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
p : F[X]
hM : p.Monic
hI : Irreducible p
hf_1 : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H_1 : n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)
hp : p = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
c : F[X]
h : c.natDegree = 0
hf : f = p ^ multiplicity p f * c
H : ¬p ∣ c
⊢ f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ multiplicity p f

Tactic:
simpa only [eq_one_of_monic_natDegree_zero ((hM.pow _).of_mul_monic_left (hf ▸ hm)) h,
    mul_one, ← hp] using hf

Premises used: Polynomial.Monic.of_mul_monic_left, Polynomial.Monic.pow, mul_one, Polynomial.eq_one_of_monic_natDegree_zero
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H : n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)
hp : p = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
hF : FiniteMultiplicity p f
have have₁ have₂ :
  ∀ (hne : multiplicity p f ≠ 0),
    ∃ (m : ℕ) (n : ℕ) (y : F),
      m ≠ 0 ∧
        (n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)) ∧
          f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m
have₃ :
  ∀ (hne : multiplicity p f ≠ 0),
    f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ multiplicity p f
have₄ :
  ∀ (hne : multiplicity p f ≠ 0) (c : F[X]) (hf : f = p ^ multiplicity p f * c) (H : ¬p ∣ c),
    f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ multiplicity p f
have₅ :
  ∀ (hne : multiplicity p f ≠ 0) (c : F[X]) (h : c.natDegree = 0) (hf : f = p ^ multiplicity p f * c) (H : ¬p ∣ c),
    f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ multiplicity p f
⊢ ∃ (m : ℕ) (n : ℕ) (y : F),
    m ≠ 0 ∧
      (n = 0 ∨ y ∉ RingHom.range (R := F) (frobenius F q)) ∧
        f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m

Tactic:
classical
  have hne := (multiplicity_pos_of_dvd hf).ne'
  refine ⟨_, n, y, hne, H, ?_⟩
  obtain ⟨c, hf, H⟩ := hF.exists_eq_pow_mul_and_not_dvd
  rw [hf, natSepDegree_mul_of_isCoprime _ c <| IsCoprime.pow_left <|
    (hI.isCoprime_or_dvd c).resolve_right H, natSepDegree_pow_of_ne_zero _ hne, hD,
    add_eq_left, natSepDegree_eq_zero_iff] at h
  simpa only [eq_one_of_monic_natDegree_zero ((hM.pow _).of_mul_monic_left (hf ▸ hm)) h,
    mul_one, ← hp] using hf

Premises used: IsCoprime.pow_left, Polynomial.natSepDegree_eq_zero_iff, FiniteMultiplicity.exists_eq_pow_mul_and_not_dvd, add_eq_left, mul_one
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
⊢ f.natSepDegree = 1 ↔
    ∃ (m : ℕ) (n : ℕ) (y : F),
      m ≠ 0 ∧ f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m

Tactic:
⟨fun h ↦ ?_, fun ⟨m, n, y, hm, h⟩ ↦ ?_⟩

Premises used: Polynomial.natSepDegree, Iff.intro, OfNat.ofNat, Eq, _private.0.Polynomial.Monic.natSepDegree_eq_one_iff.match_1
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
refine_1 :
  ∀ (h : f.natSepDegree = 1),
    ∃ (m : ℕ) (n : ℕ) (y : F),
      m ≠ 0 ∧ f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m
refine_2 :
  (∃ (m : ℕ) (n : ℕ) (y : F),
      m ≠ 0 ∧ f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m) →
    ∀ (m n : ℕ) (y : F) (hm : m ≠ 0)
      (h : f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m),
      f.natSepDegree = 1
⊢ f.natSepDegree = 1 ↔
    ∃ (m : ℕ) (n : ℕ) (y : F),
      m ≠ 0 ∧ f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨m, n, y, hm, h⟩ ↦ ?_⟩
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
refine_1 :
  ∀ (m n : ℕ) (y : F) (hm : m ≠ 0)
    (h : f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m),
    ∃ (m : ℕ) (n : ℕ) (y : F),
      m ≠ 0 ∧ f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m
⊢ ∃ (m : ℕ) (n : ℕ) (y : F),
    m ≠ 0 ∧ f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m

Tactic:
obtain ⟨m, n, y, hm, -, h⟩ := hm.eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one q h

Premises used: Polynomial.Monic.eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm_1 : f.Monic
h_1 : f.natSepDegree = 1
m n : ℕ
y : F
hm : m ≠ 0
h : f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m
⊢ ∃ (m : ℕ) (n : ℕ) (y : F),
    m ≠ 0 ∧ f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m

Tactic:
⟨m, n, y, hm, h⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm_1 : f.Monic
h_1 : f.natSepDegree = 1
m n : ℕ
y : F
hm : m ≠ 0
h : f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m
⊢ ∃ (m : ℕ) (n : ℕ) (y : F),
    m ≠ 0 ∧ f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m

Tactic:
exact ⟨m, n, y, hm, h⟩
-- Module: Mathlib.FieldTheory.SeparableDegree
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm_1 : f.Monic
h_1 :
  ∃ (m : ℕ) (n : ℕ) (y : F),
    m ≠ 0 ∧ f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m
m n : ℕ
y : F
hm : m ≠ 0
h : f = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m
refine_2 :
  (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m).natSepDegree = 1
refine_2₁ :
  (if m = 0 then 0
    else (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])).natSepDegree) =
    1
refine_2₂ :
  (if False then 0
    else (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])).natSepDegree) =
    1
refine_2₃ : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])).natSepDegree = 1
⊢ f.natSepDegree = 1

Tactic:
simp_rw [h, natSepDegree_pow, hm, ite_false, natSepDegree_X_pow_char_pow_sub_C]

Premises used: Polynomial.natSepDegree_pow, ite_false, Polynomial.natSepDegree_X_pow_char_pow_sub_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
⊢ natSepDegree (minpoly F x) = 1 ↔
    ∃ (n : ℕ) (y : F),
      Eq (α := F[X]) (minpoly F x)
        ((expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])))

Tactic:
⟨fun h ↦ ?_, fun ⟨n, y, h⟩ ↦ ?_⟩

Premises used: _private.0.minpoly.natSepDegree_eq_one_iff_eq_expand_X_sub_C.match_1, minpoly, Polynomial.natSepDegree, Iff.intro, 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
refine_1 :
  ∀ (h : natSepDegree (minpoly F x) = 1),
    ∃ (n : ℕ) (y : F),
      Eq (α := F[X]) (minpoly F x)
        ((expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])))
refine_2 :
  (∃ (n : ℕ) (y : F),
      Eq (α := F[X]) (minpoly F x)
        ((expand F (q ^ n) : (a : F[X]) → F[X])
          (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])))) →
    ∀ (n : ℕ) (y : F)
      (h :
        Eq (α := F[X]) (minpoly F x)
          ((expand F (q ^ n) : (a : F[X]) → F[X])
            (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])))),
      natSepDegree (minpoly F x) = 1
⊢ natSepDegree (minpoly F x) = 1 ↔
    ∃ (n : ℕ) (y : F),
      Eq (α := F[X]) (minpoly F x)
        ((expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])))

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨n, y, h⟩ ↦ ?_⟩
-- 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
h' : ¬IsIntegral F x
⊢ False

Tactic:
simp only [eq_zero h', natSepDegree_zero, zero_ne_one] at h

Premises used: Polynomial.natSepDegree_zero, zero_ne_one, minpoly.eq_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 : natSepDegree (minpoly F x) = 1
⊢ IsIntegral F x

Tactic:
have halg : IsIntegral F x := by_contra fun h' ↦ by
      simp only [eq_zero h', natSepDegree_zero, zero_ne_one] at h
-- 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
halg : IsIntegral F x
⊢ ∃ (n : ℕ) (y : F),
    Eq (α := F[X]) (minpoly F x)
      ((expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])))

Tactic:
(minpoly.irreducible halg).natSepDegree_eq_one_iff_of_monic' q
      (minpoly.monic halg) |>.1 h

Premises used: minpoly.monic, Irreducible.natSepDegree_eq_one_iff_of_monic', Iff.mp, minpoly.irreducible
-- 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
halg : IsIntegral F x
⊢ ∃ (n : ℕ) (y : F),
    Eq (α := F[X]) (minpoly F x)
      ((expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])))

Tactic:
exact (minpoly.irreducible halg).natSepDegree_eq_one_iff_of_monic' q
      (minpoly.monic halg) |>.1 h

Premises used: minpoly.monic, Irreducible.natSepDegree_eq_one_iff_of_monic', Iff.mp, minpoly.irreducible
-- 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 (α := F[X]) (minpoly F x)
      ((expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])))
n : ℕ
y : F
h :
  Eq (α := F[X]) (minpoly F x)
    ((expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])))
refine_2 :
  natSepDegree.{u} (F := F)
      ((expand F (q ^ n) : (a : F[X]) → F[X]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X]))) =
    1
refine_2₁ : (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])).natSepDegree = 1
refine_2₂ refine_2₃ : Eq (α := ℕ) 1 1
⊢ natSepDegree (minpoly F x) = 1

Tactic:
rw [h, natSepDegree_expand _ q, natSepDegree_X_sub_C]

Premises used: Polynomial.natSepDegree_expand, Polynomial.natSepDegree_X_sub_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
⊢ natSepDegree (minpoly F x) = 1 ↔
    ∃ (n : ℕ) (y : F),
      minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])

Tactic:
simp only [minpoly.natSepDegree_eq_one_iff_eq_expand_X_sub_C q, map_sub, expand_X, expand_C]

Premises used: map_sub, Polynomial.expand_C, Polynomial.expand_X, minpoly.natSepDegree_eq_one_iff_eq_expand_X_sub_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
h :
  (∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)) ↔
    ∃ (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)
convert_2 :
  natSepDegree (minpoly F x) = 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)
⊢ natSepDegree (minpoly F x) = 1 ↔
    ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)

Tactic:
convert_to _ ↔ ∃ (n : ℕ) (y : F), Polynomial.aeval x (X ^ q ^ n - C y) = 0
-- 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 :
  (∃ (n : ℕ) (x_1 : F), ((algebraMap F E : F →+* E) : (a : F) → E) x_1 = x ^ q ^ n) ↔
    ∃ (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)
h₁ :
  (∃ (n : ℕ) (x_1 : F), ((algebraMap F E : F →+* E) : (a : F) → E) x_1 = x ^ q ^ n) ↔
    ∃ (n : ℕ) (y : F),
      HSub.hSub (α := E) (β := E) ((Polynomial.aeval x : (a : F[X]) → E) (HPow.hPow (α := F[X]) X (q ^ n)) : E)
          ((Polynomial.aeval x : (a : F[X]) → E) ((C : (a : F) → F[X]) y : F[X]) : E) =
        0
h₂ :
  (∃ (n : ℕ) (x_1 : F), ((algebraMap F E : F →+* E) : (a : F) → E) x_1 = x ^ q ^ n) ↔
    ∃ (n : ℕ) (y : F),
      HSub.hSub (β := E) (HPow.hPow (α := E) ((Polynomial.aeval x : (a : F[X]) → E) X : E) (q ^ n))
          ((Polynomial.aeval x : (a : F[X]) → E) ((C : (a : F) → F[X]) y : F[X]) : E) =
        0
h₃ :
  (∃ (n : ℕ) (x_1 : F), ((algebraMap F E : F →+* E) : (a : F) → E) x_1 = x ^ q ^ n) ↔
    ∃ (n : ℕ) (y : F),
      HSub.hSub (β := E) (HPow.hPow (α := E) ((Polynomial.aeval x : (a : F[X]) → E) X : E) (q ^ n))
          ((algebraMap F E : (a : F) → E) y : E) =
        0
h₄ :
  (∃ (n : ℕ) (x_1 : F), ((algebraMap F E : F →+* E) : (a : F) → E) x_1 = x ^ q ^ n) ↔
    ∃ (n : ℕ) (y : F), HSub.hSub (β := E) (x ^ q ^ n) ((algebraMap F E : (a : F) → E) y : E) = 0
h₅ :
  (∃ (n : ℕ) (x_1 : F), ((algebraMap F E : F →+* E) : (a : F) → E) x_1 = x ^ q ^ n) ↔
    ∃ (n : ℕ) (y : F), x ^ q ^ n = (algebraMap F E : (a : F) → E) y
⊢ (∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)) ↔
    ∃ (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:
simp_rw [RingHom.mem_range, map_sub, map_pow, aeval_C, aeval_X, sub_eq_zero, eq_comm]

Premises used: map_sub, RingHom.mem_range, sub_eq_zero, map_pow, 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
⊢ natSepDegree (minpoly F x) = 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)

Tactic:
⟨fun h ↦ ?_, fun ⟨n, y, h⟩ ↦ ?_⟩

Premises used: _private.0.minpoly.natSepDegree_eq_one_iff_pow_mem.match_3, minpoly, Polynomial.natSepDegree, Iff.intro, 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
convert_2 :
  ∀ (h : natSepDegree (minpoly F x) = 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)
convert_2₁ :
  (∃ (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)),
      natSepDegree (minpoly F x) = 1
⊢ natSepDegree (minpoly F x) = 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)

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨n, y, h⟩ ↦ ?_⟩
-- 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
convert_2 :
  ∀ (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)
⊢ ∃ (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:
obtain ⟨n, y, hx⟩ := (minpoly.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