awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ (∃ (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))
        ((algebraMap F E : (a : F) → E) y : 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
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
⊢ (∃ (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) (x ^ q ^ n) ((algebraMap F E : (a : F) → E) y : 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
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
⊢ (∃ (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), x ^ q ^ n = (algebraMap F E : (a : F) → E) y
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
⊢ 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)
have 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)
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
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)
⊢ 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)
have 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
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
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)
have 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)
Tactic: obtain ⟨n, y, hx⟩ := (minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C q).1 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_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)
⊢ natSepDegree (minpoly F x) = 1
have hnezero : 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
-- 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.{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
have convert_2 : 1 ≤ natSepDegree (minpoly F x)
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 ?_
-- 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.{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 ≤ natSepDegree (minpoly F x)
have convert_2 : 1 ≤ natDegree (minpoly F x)
Tactic: rw [Nat.one_le_iff_ne_zero, natSepDegree_ne_zero_iff, ← Nat.one_le_iff_ne_zero]
-- 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
⊢ 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
have this : ExpChar E q
Tactic: haveI := expChar_of_injective_algebraMap (algebraMap F E).injective q
-- 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
this : ExpChar E 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
have this₁ : ExpChar.{v} E[X] q
Tactic: haveI := expChar_of_injective_ringHom (C_injective (R := E)) q
-- 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
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
have 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
Tactic: refine ⟨fun h ↦ ?_, fun ⟨n, h⟩ ↦ (natSepDegree_eq_one_iff_pow_mem q).2 ?_⟩
-- 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
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
⊢ 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
have 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)
Tactic: refine ⟨fun h ↦ ?_, fun ⟨n, h⟩ ↦ (natSepDegree_eq_one_iff_pow_mem q).2 ?_⟩
-- 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
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
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
have 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
Tactic: obtain ⟨n, y, h⟩ := (natSepDegree_eq_one_iff_eq_X_pow_sub_C q).1 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
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])
⊢ ∃ (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
have 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)
Tactic: have hx := congr_arg (Polynomial.aeval x) h.symm
-- 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
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)
⊢ ∃ (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
have hx₁ : (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
Cleared hypotheses: hx
-- 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
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
⊢ ∃ (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
have 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
Tactic: use n
-- 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
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
⊢ 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
have 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
Tactic: rw [h, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, hx, map_pow,
      ← sub_pow_expChar_pow_of_commute _ _ (commute_X _)]
-- 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
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
⊢ 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
have 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
Tactic: rw [h, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, hx, map_pow,
      ← sub_pow_expChar_pow_of_commute _ _ (commute_X _)]
-- 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
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
⊢ 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
have 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
Tactic: rw [h, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, hx, map_pow,
      ← sub_pow_expChar_pow_of_commute _ _ (commute_X _)]
-- 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
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
⊢ 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
have 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
Tactic: rw [h, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, hx, map_pow,
      ← sub_pow_expChar_pow_of_commute _ _ (commute_X _)]