awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
⊢ ∃ (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 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
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
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
⊢ ∃ (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 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
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
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
⊢ ∃ (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 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
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
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
⊢ ∃ (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 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
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
have 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
Tactic: refine ⟨fun h ↦ ?_, fun ⟨m, n, y, hm, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
⊢ 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
have 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
Tactic: refine ⟨fun h ↦ ?_, fun ⟨m, n, y, hm, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
q : ℕ
inst_1 : ExpChar F q
hm : f.Monic
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
have 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
Tactic: obtain ⟨m, n, y, hm, -, h⟩ := hm.eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one q h
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
⊢ f.natSepDegree = 1
have refine_2 : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X]) ^ m).natSepDegree = 1
Tactic: simp_rw [h, natSepDegree_pow, hm, ite_false, natSepDegree_X_pow_char_pow_sub_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
⊢ f.natSepDegree = 1
have 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
Tactic: simp_rw [h, natSepDegree_pow, hm, ite_false, natSepDegree_X_pow_char_pow_sub_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
⊢ f.natSepDegree = 1
have 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
Tactic: simp_rw [h, natSepDegree_pow, hm, ite_false, natSepDegree_X_pow_char_pow_sub_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
⊢ f.natSepDegree = 1
have refine_2₃ : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])).natSepDegree = 1
Tactic: simp_rw [h, natSepDegree_pow, hm, ite_false, natSepDegree_X_pow_char_pow_sub_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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])))
have 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])))
Tactic: refine ⟨fun h ↦ ?_, fun ⟨n, y, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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])))
⊢ 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])))
have 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
Tactic: refine ⟨fun h ↦ ?_, fun ⟨n, y, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
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),
    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])))
have halg : 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
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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])))
⊢ natSepDegree (minpoly F x) = 1
have 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
Tactic: rw [h, natSepDegree_expand _ q, natSepDegree_X_sub_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
⊢ natSepDegree (minpoly F x) = 1
have refine_2₁ : (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])).natSepDegree = 1
Tactic: rw [h, natSepDegree_expand _ q, natSepDegree_X_sub_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
⊢ natSepDegree (minpoly F x) = 1
have refine_2₂ : Eq (α := ℕ) 1 1
Tactic: rw [h, natSepDegree_expand _ q, natSepDegree_X_sub_C]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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 : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
have 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)
Tactic: convert_to _ ↔ ∃ (n : ℕ) (y : F), Polynomial.aeval x (X ^ q ^ n - C y) = 0
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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)
⊢ natSepDegree (minpoly F x) = 1 ↔
    ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
have 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)
Tactic: convert_to _ ↔ ∃ (n : ℕ) (y : F), Polynomial.aeval x (X ^ q ^ n - C y) = 0
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
⊢ (∃ (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)
have 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)
Tactic: simp_rw [RingHom.mem_range, map_sub, map_pow, aeval_C, aeval_X, sub_eq_zero, eq_comm]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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)
⊢ (∃ (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)
have 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
Tactic: simp_rw [RingHom.mem_range, map_sub, map_pow, aeval_C, aeval_X, sub_eq_zero, eq_comm]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
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
⊢ (∃ (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)
have 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
Tactic: simp_rw [RingHom.mem_range, map_sub, map_pow, aeval_C, aeval_X, sub_eq_zero, eq_comm]