awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
h : Irreducible (map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - X - 1))
neg :
  ∀ (h : Irreducible (map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - X) - map (Int.castRingHom ℚ) 1)),
    Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
neg₁ :
  ∀
    (h :
      Irreducible
        (map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n) - map (Int.castRingHom ℚ) X - map (Int.castRingHom ℚ) 1)),
    Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
neg₂ :
  ∀ (h : Irreducible (map (Int.castRingHom ℚ) X ^ n - map (Int.castRingHom ℚ) X - map (Int.castRingHom ℚ) 1)),
    Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
⊢ Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
have neg₃ : ∀ (h : Irreducible (map (Int.castRingHom ℚ) X ^ n - map (Int.castRingHom ℚ) X - 1)),
  Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
Tactic: rwa [Polynomial.map_sub, Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_one,
      Polynomial.map_X] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Selmer (goal)
Goal:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : HPow.hPow (α := ℤ[X]) X n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
h : Irreducible (map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - X - 1))
neg :
  ∀ (h : Irreducible (map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - X) - map (Int.castRingHom ℚ) 1)),
    Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
neg₁ :
  ∀
    (h :
      Irreducible
        (map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n) - map (Int.castRingHom ℚ) X - map (Int.castRingHom ℚ) 1)),
    Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
neg₂ :
  ∀ (h : Irreducible (map (Int.castRingHom ℚ) X ^ n - map (Int.castRingHom ℚ) X - map (Int.castRingHom ℚ) 1)),
    Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
neg₃ :
  ∀ (h : Irreducible (map (Int.castRingHom ℚ) X ^ n - map (Int.castRingHom ℚ) X - 1)),
    Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
⊢ Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
have neg₄ : ∀ (h : Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)), Irreducible (HPow.hPow (α := ℚ[X]) X n - X - 1)
Tactic: rwa [Polynomial.map_sub, Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_one,
      Polynomial.map_X] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F : Type u_1
inst : CommSemiring F
q : ℕ
f g : F[X]
hf : IsSeparableContraction q f g
⊢ ∃ (m : ℕ), g.natDegree * q ^ m = f.natDegree
have obtain : ∀ (m : ℕ) (hf : IsSeparableContraction q ((expand F (q ^ m) : (a : F[X]) → F[X]) g) g),
  ∃ (m_1 : ℕ), g.natDegree * q ^ m_1 = natDegree.{u_1} (R := F) ((expand F (q ^ m) : (a : F[X]) → F[X]) g)
Tactic: obtain ⟨m, rfl⟩ := hf.2
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F : Type u_1
inst : CommSemiring F
q : ℕ
g : F[X]
m : ℕ
hf : IsSeparableContraction q ((expand F (q ^ m) : (a : F[X]) → F[X]) g) g
⊢ ∃ (m_1 : ℕ), g.natDegree * q ^ m_1 = natDegree.{u_1} (R := F) ((expand F (q ^ m) : (a : F[X]) → F[X]) g)
have h : g.natDegree * q ^ m = natDegree.{u_1} (R := F) ((expand F (q ^ m) : (a : F[X]) → F[X]) g)
Tactic: use m
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F : Type u_1
inst : CommSemiring F
q : ℕ
g : F[X]
m : ℕ
hf : IsSeparableContraction q ((expand F (q ^ m) : (a : F[X]) → F[X]) g) g
⊢ g.natDegree * q ^ m = natDegree.{u_1} (R := F) ((expand F (q ^ m) : (a : F[X]) → F[X]) g)
have h : g.natDegree * q ^ m = g.natDegree * q ^ m
Tactic: rw [natDegree_expand]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F : Type u_1
inst : CommSemiring F
f : F[X]
hf : HasSeparableContraction 1 f
⊢ hf.degree = f.natDegree
have let : ∀ (a : ℕ) (ha : hf.degree * HPow.hPow (α := ℕ) 1 a = f.natDegree), hf.degree = f.natDegree
Tactic: let ⟨a, ha⟩ := hf.dvd_degree'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
q : ℕ
hF : ExpChar F q
f : F[X]
irred : Irreducible f
⊢ HasSeparableContraction q f
have zero : ∀ [CharZero F], HasSeparableContraction 1 f
Tactic: cases hF
Cleared hypotheses: q, hF
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
q : ℕ
hF : ExpChar F q
f : F[X]
irred : Irreducible f
zero : ∀ [CharZero F], HasSeparableContraction 1 f
⊢ HasSeparableContraction q f
have prime : Nat.Prime q → ∀ [CharP F q], HasSeparableContraction q f
Tactic: cases hF
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
f : F[X]
irred : Irreducible f
inst_1 : CharZero F
⊢ (expand F (HPow.hPow (α := ℕ) (β := ℕ) 1 0) : (a : F[X]) → F[X]) f = f
have rw : (expand F 1 : (a : F[X]) → F[X]) f = f
Tactic: rw [pow_zero, expand_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
f : F[X]
irred : Irreducible f
inst_1 : CharZero F
rw : (expand F 1 : (a : F[X]) → F[X]) f = f
⊢ (expand F (HPow.hPow (α := ℕ) (β := ℕ) 1 0) : (a : F[X]) → F[X]) f = f
have rw₁ : f = f
Tactic: rw [pow_zero, expand_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
q : ℕ
f : F[X]
irred : Irreducible f
hprime : Nat.Prime q
hchar : CharP F q
⊢ HasSeparableContraction q f
have prime : ∀ (n : ℕ) (g : F[X]) (hgs : g.Separable) (hge : (expand F (q ^ n) : (a : F[X]) → F[X]) g = f),
  HasSeparableContraction q f
Tactic: rcases exists_separable_of_irreducible q irred ‹q.Prime›.ne_zero with ⟨n, g, hgs, hge⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
q : ℕ
hq : NeZero q
inst_1 : CharP F q
g g' : F[X]
m m' : ℕ
h_expand :
  Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X]) ((expand F (q ^ m') : (a : F[X]) → F[X]) g' : F[X])
hg : g.Separable
hg' : g'.Separable
⊢ g.natDegree = g'.natDegree
have inr : ∀
  (this :
    ∀ {F : Type u_1} [inst : Field F] (q : ℕ) [hq : NeZero q] [CharP F q] (g g' : F[X]) (m m' : ℕ)
      (h_expand :
        Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X])
          ((expand F (q ^ m') : (a : F[X]) → F[X]) g' : F[X]))
      (hg : g.Separable) (hg' : g'.Separable) (hm : m ≤ m'), g.natDegree = g'.natDegree)
  (hm : ¬m ≤ m'), g.natDegree = g'.natDegree
Tactic: wlog hm : m ≤ m'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
q : ℕ
hq : NeZero q
inst_1 : CharP F q
g g' : F[X]
m m' : ℕ
h_expand :
  Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X]) ((expand F (q ^ m') : (a : F[X]) → F[X]) g' : F[X])
hg : g.Separable
hg' : g'.Separable
inr :
  ∀
    (this :
      ∀ {F : Type u_1} [inst : Field F] (q : ℕ) [hq : NeZero q] [CharP F q] (g g' : F[X]) (m m' : ℕ)
        (h_expand :
          Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X])
            ((expand F (q ^ m') : (a : F[X]) → F[X]) g' : F[X]))
        (hg : g.Separable) (hg' : g'.Separable) (hm : m ≤ m'), g.natDegree = g'.natDegree)
    (hm : ¬m ≤ m'), g.natDegree = g'.natDegree
⊢ g.natDegree = g'.natDegree
have wlog : ∀ {F : Type u_1} [inst : Field F] (q : ℕ) [hq : NeZero q] [CharP F q] (g g' : F[X]) (m m' : ℕ)
  (h_expand :
    Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X])
      ((expand F (q ^ m') : (a : F[X]) → F[X]) g' : F[X]))
  (hg : g.Separable) (hg' : g'.Separable) (hm : m ≤ m'), g.natDegree = g'.natDegree
Tactic: wlog hm : m ≤ m'
Cleared hypotheses: hq, inst_1, g, g', m, m', h_expand, hg, hg'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F_1 : Type u_1
inst : Field F_1
q_1 : ℕ
F : Type u_1
inst_1 : Field F
q : ℕ
hq : NeZero q
inst_2 : CharP F q
g g' : F[X]
m m' : ℕ
h_expand :
  Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X]) ((expand F (q ^ m') : (a : F[X]) → F[X]) g' : F[X])
hg : g.Separable
hg' : g'.Separable
hm : m ≤ m'
⊢ g.natDegree = g'.natDegree
have obtain : ∀ (s : ℕ)
  (h_expand :
    Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X])
      ((expand F (q ^ (m + s)) : (a : F[X]) → F[X]) g' : F[X]))
  (hm : m ≤ m + s), g.natDegree = g'.natDegree
Tactic: obtain ⟨s, rfl⟩ := exists_add_of_le hm
Cleared hypotheses: m', h_expand, hm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (hypothesis)
Goal:
F_1 : Type u_1
inst : Field F_1
q_1 : ℕ
F : Type u_1
inst_1 : Field F
q : ℕ
hq : NeZero q
inst_2 : CharP F q
g g' : F[X]
m : ℕ
hg : g.Separable
hg' : g'.Separable
s : ℕ
h_expand :
  Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X])
    ((expand F (q ^ (m + s)) : (a : F[X]) → F[X]) g' : F[X])
hm : m ≤ m + s
⊢ g.natDegree = g'.natDegree
have h_expand₁ : g = (expand F (q ^ s) : (a : F[X]) → F[X]) g'
Tactic: rw [pow_add, expand_mul, expand_inj (pow_pos (NeZero.pos q) m)] at h_expand
Cleared hypotheses: h_expand, hm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F_1 : Type u_1
inst : Field F_1
q_1 : ℕ
F : Type u_1
inst_1 : Field F
q : ℕ
hq : NeZero q
inst_2 : CharP F q
g g' : F[X]
m : ℕ
hg : g.Separable
hg' : g'.Separable
s : ℕ
h_expand : g = (expand F (q ^ s) : (a : F[X]) → F[X]) g'
hm : m ≤ m + s
⊢ g.natDegree = g'.natDegree
have subst : ∀ (hg : Separable.{u_1} (R := F) ((expand F (q ^ s) : (a : F[X]) → F[X]) g')),
  natDegree.{u_1} (R := F) ((expand F (q ^ s) : (a : F[X]) → F[X]) g') = g'.natDegree
Tactic: subst h_expand
Cleared hypotheses: g, hg, h_expand
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F_1 : Type u_1
inst : Field F_1
q_1 : ℕ
F : Type u_1
inst_1 : Field F
q : ℕ
hq : NeZero q
inst_2 : CharP F q
g' : F[X]
m : ℕ
hg' : g'.Separable
s : ℕ
hm : m ≤ m + s
hg : Separable.{u_1} (R := F) ((expand F (q ^ s) : (a : F[X]) → F[X]) g')
⊢ natDegree.{u_1} (R := F) ((expand F (q ^ s) : (a : F[X]) → F[X]) g') = g'.natDegree
have inl : ∀ (h : IsUnit g'), natDegree.{u_1} (R := F) ((expand F (q ^ s) : (a : F[X]) → F[X]) g') = g'.natDegree
Tactic: rcases isUnit_or_eq_zero_of_separable_expand q s (NeZero.pos q) hg with (h | rfl)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F_1 : Type u_1
inst : Field F_1
q_1 : ℕ
F : Type u_1
inst_1 : Field F
q : ℕ
hq : NeZero q
inst_2 : CharP F q
g' : F[X]
m : ℕ
hg' : g'.Separable
s : ℕ
hm : m ≤ m + s
hg : Separable.{u_1} (R := F) ((expand F (q ^ s) : (a : F[X]) → F[X]) g')
inl : ∀ (h : IsUnit g'), natDegree.{u_1} (R := F) ((expand F (q ^ s) : (a : F[X]) → F[X]) g') = g'.natDegree
⊢ natDegree.{u_1} (R := F) ((expand F (q ^ s) : (a : F[X]) → F[X]) g') = g'.natDegree
have inr : ∀ (hm : m ≤ m + 0) (hg : Separable.{u_1} (R := F) ((expand F (HPow.hPow (β := ℕ) q 0) : (a : F[X]) → F[X]) g')),
  natDegree.{u_1} (R := F) ((expand F (HPow.hPow (β := ℕ) q 0) : (a : F[X]) → F[X]) g') = g'.natDegree
Tactic: rcases isUnit_or_eq_zero_of_separable_expand q s (NeZero.pos q) hg with (h | rfl)
Cleared hypotheses: s, hm, hg
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F_1 : Type u_1
inst : Field F_1
q_1 : ℕ
F : Type u_1
inst_1 : Field F
q : ℕ
hq : NeZero q
inst_2 : CharP F q
g' : F[X]
m : ℕ
hg' : g'.Separable
s : ℕ
hm : m ≤ m + s
hg : Separable.{u_1} (R := F) ((expand F (q ^ s) : (a : F[X]) → F[X]) g')
h : IsUnit g'
⊢ natDegree.{u_1} (R := F) ((expand F (q ^ s) : (a : F[X]) → F[X]) g') = g'.natDegree
have inl : g'.natDegree * q ^ s = g'.natDegree
Tactic: rw [natDegree_expand, natDegree_eq_zero_of_isUnit h, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F_1 : Type u_1
inst : Field F_1
q_1 : ℕ
F : Type u_1
inst_1 : Field F
q : ℕ
hq : NeZero q
inst_2 : CharP F q
g' : F[X]
m : ℕ
hg' : g'.Separable
s : ℕ
hm : m ≤ m + s
hg : Separable.{u_1} (R := F) ((expand F (q ^ s) : (a : F[X]) → F[X]) g')
h : IsUnit g'
inl : g'.natDegree * q ^ s = g'.natDegree
⊢ natDegree.{u_1} (R := F) ((expand F (q ^ s) : (a : F[X]) → F[X]) g') = g'.natDegree
have inl₁ : 0 * q ^ s = 0
Tactic: rw [natDegree_expand, natDegree_eq_zero_of_isUnit h, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F_1 : Type u_1
inst : Field F_1
q_1 : ℕ
F : Type u_1
inst_1 : Field F
q : ℕ
hq : NeZero q
inst_2 : CharP F q
g' : F[X]
m : ℕ
hg' : g'.Separable
s : ℕ
hm : m ≤ m + s
hg : Separable.{u_1} (R := F) ((expand F (q ^ s) : (a : F[X]) → F[X]) g')
h : IsUnit g'
inl : g'.natDegree * q ^ s = g'.natDegree
inl₁ : 0 * q ^ s = 0
⊢ natDegree.{u_1} (R := F) ((expand F (q ^ s) : (a : F[X]) → F[X]) g') = g'.natDegree
have inl₂ : Eq (α := ℕ) 0 0
Tactic: rw [natDegree_expand, natDegree_eq_zero_of_isUnit h, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F_1 : Type u_1
inst : Field F_1
q_1 : ℕ
F : Type u_1
inst_1 : Field F
q : ℕ
hq : NeZero q
inst_2 : CharP F q
g' : F[X]
m : ℕ
hg' : g'.Separable
hm : m ≤ m + 0
hg : Separable.{u_1} (R := F) ((expand F (HPow.hPow (β := ℕ) q 0) : (a : F[X]) → F[X]) g')
⊢ natDegree.{u_1} (R := F) ((expand F (HPow.hPow (β := ℕ) q 0) : (a : F[X]) → F[X]) g') = g'.natDegree
have inr : g'.natDegree * HPow.hPow (β := ℕ) q 0 = g'.natDegree
Tactic: rw [natDegree_expand, pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F_1 : Type u_1
inst : Field F_1
q_1 : ℕ
F : Type u_1
inst_1 : Field F
q : ℕ
hq : NeZero q
inst_2 : CharP F q
g' : F[X]
m : ℕ
hg' : g'.Separable
hm : m ≤ m + 0
hg : Separable.{u_1} (R := F) ((expand F (HPow.hPow (β := ℕ) q 0) : (a : F[X]) → F[X]) g')
inr : g'.natDegree * HPow.hPow (β := ℕ) q 0 = g'.natDegree
⊢ natDegree.{u_1} (R := F) ((expand F (HPow.hPow (β := ℕ) q 0) : (a : F[X]) → F[X]) g') = g'.natDegree
have inr₁ : g'.natDegree * 1 = g'.natDegree
Tactic: rw [natDegree_expand, pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F_1 : Type u_1
inst : Field F_1
q_1 : ℕ
F : Type u_1
inst_1 : Field F
q : ℕ
hq : NeZero q
inst_2 : CharP F q
g' : F[X]
m : ℕ
hg' : g'.Separable
hm : m ≤ m + 0
hg : Separable.{u_1} (R := F) ((expand F (HPow.hPow (β := ℕ) q 0) : (a : F[X]) → F[X]) g')
inr : g'.natDegree * HPow.hPow (β := ℕ) q 0 = g'.natDegree
inr₁ : g'.natDegree * 1 = g'.natDegree
⊢ natDegree.{u_1} (R := F) ((expand F (HPow.hPow (β := ℕ) q 0) : (a : F[X]) → F[X]) g') = g'.natDegree
have inr₂ : g'.natDegree = g'.natDegree
Tactic: rw [natDegree_expand, pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
hF : ExpChar F q
g : F[X]
hg : IsSeparableContraction q f g
⊢ g.natDegree = hf.degree
have zero : ∀ [CharZero F] (hf : HasSeparableContraction 1 f) (hg : IsSeparableContraction 1 f g), g.natDegree = hf.degree
Tactic: cases hF
Cleared hypotheses: q, hf, hF, hg
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
hF : ExpChar F q
g : F[X]
hg : IsSeparableContraction q f g
zero : ∀ [CharZero F] (hf : HasSeparableContraction 1 f) (hg : IsSeparableContraction 1 f g), g.natDegree = hf.degree
⊢ g.natDegree = hf.degree
have prime : Nat.Prime q → ∀ [CharP F q], g.natDegree = hf.degree
Tactic: cases hF
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
f g : F[X]
inst_1 : CharZero F
hf : HasSeparableContraction 1 f
hg : IsSeparableContraction 1 f g
⊢ g.natDegree = hf.degree
have zero : g.Separable → ∀ (m : ℕ) (hm : (expand F (HPow.hPow (α := ℕ) 1 m) : (a : F[X]) → F[X]) g = f), g.natDegree = hf.degree
Tactic: rcases hg with ⟨_, m, hm⟩
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (hypothesis)
Goal:
F : Type u_1
inst : Field F
f g : F[X]
inst_1 : CharZero F
hf : HasSeparableContraction 1 f
left : g.Separable
m : ℕ
hm : (expand F (HPow.hPow (α := ℕ) 1 m) : (a : F[X]) → F[X]) g = f
⊢ g.natDegree = hf.degree
have hm₁ : g = f
Tactic: rw [one_pow, expand_one] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
f g : F[X]
inst_1 : CharZero F
hf : HasSeparableContraction 1 f
left : g.Separable
m : ℕ
hm : g = f
⊢ g.natDegree = hf.degree
have zero : g.natDegree = f.natDegree
Tactic: rw [hf.eq_degree, hm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
f g : F[X]
inst_1 : CharZero F
hf : HasSeparableContraction 1 f
left : g.Separable
m : ℕ
hm : g = f
zero : g.natDegree = f.natDegree
⊢ g.natDegree = hf.degree
have zero₁ : f.natDegree = f.natDegree
Tactic: rw [hf.eq_degree, hm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hg : IsSeparableContraction q f g
hprime : Nat.Prime q
hchar : CharP F q
⊢ g.natDegree = hf.degree
have prime : ∀ (hg : g.Separable) (m : ℕ) (hm : (expand F (q ^ m) : (a : F[X]) → F[X]) g = f), g.natDegree = hf.degree
Tactic: rcases hg with ⟨hg, m, hm⟩
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime : Nat.Prime q
hchar : CharP F q
hg : g.Separable
m : ℕ
hm : (expand F (q ^ m) : (a : F[X]) → F[X]) g = f
g' : F[X] := Classical.choose (p := IsSeparableContraction q f) hf
⊢ g.natDegree = hf.degree
have prime : ∀ (hg' : (Classical.choose (p := IsSeparableContraction q f) hf).Separable) (m' : ℕ)
  (hm' : (expand F (q ^ m') : (a : F[X]) → F[X]) (Classical.choose (p := IsSeparableContraction q f) hf) = f),
  g.natDegree = hf.degree
Tactic: obtain ⟨hg', m', hm'⟩ := Classical.choose_spec hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (hypothesis)
Goal:
F : Type u_1
inst : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime : Nat.Prime q
hchar : CharP F q
hg : g.Separable
m : ℕ
hm : (expand F (q ^ m) : (a : F[X]) → F[X]) g = f
g' : F[X] := Classical.choose (p := IsSeparableContraction q f) hf
hg' : (Classical.choose (p := IsSeparableContraction q f) hf).Separable
m' : ℕ
hm' : (expand F (q ^ m') : (a : F[X]) → F[X]) (Classical.choose (p := IsSeparableContraction q f) hf) = f
⊢ g.natDegree = hf.degree
have this : Fact (Nat.Prime q)
Tactic: haveI : Fact q.Prime := ⟨by assumption⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime : Nat.Prime q
hchar : CharP F q
hg : g.Separable
m : ℕ
hm : (expand F (q ^ m) : (a : F[X]) → F[X]) g = f
g' : F[X] := Classical.choose (p := IsSeparableContraction q f) hf
hg' : (Classical.choose (p := IsSeparableContraction q f) hf).Separable
m' : ℕ
hm' : (expand F (q ^ m') : (a : F[X]) → F[X]) (Classical.choose (p := IsSeparableContraction q f) hf) = f
this : Fact (Nat.Prime q)
⊢ g.natDegree = hf.degree
have prime : Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X]) ((expand F (q ^ m') : (a : F[X]) → F[X]) g' : F[X])
Tactic: refine contraction_degree_eq_or_insep q g g' m m' ?_ hg hg'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime : Nat.Prime q
hchar : CharP F q
hg : g.Separable
m : ℕ
hm : (expand F (q ^ m) : (a : F[X]) → F[X]) g = f
g' : F[X] := Classical.choose (p := IsSeparableContraction q f) hf
hg' : (Classical.choose (p := IsSeparableContraction q f) hf).Separable
m' : ℕ
hm' : (expand F (q ^ m') : (a : F[X]) → F[X]) (Classical.choose (p := IsSeparableContraction q f) hf) = f
this : Fact (Nat.Prime q)
⊢ Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X]) ((expand F (q ^ m') : (a : F[X]) → F[X]) g' : F[X])
have prime : f = (expand F (q ^ m') : (a : F[X]) → F[X]) g'
Tactic: rw [hm, hm']
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime : Nat.Prime q
hchar : CharP F q
hg : g.Separable
m : ℕ
hm : (expand F (q ^ m) : (a : F[X]) → F[X]) g = f
g' : F[X] := Classical.choose (p := IsSeparableContraction q f) hf
hg' : (Classical.choose (p := IsSeparableContraction q f) hf).Separable
m' : ℕ
hm' : (expand F (q ^ m') : (a : F[X]) → F[X]) (Classical.choose (p := IsSeparableContraction q f) hf) = f
this : Fact (Nat.Prime q)
prime : f = (expand F (q ^ m') : (a : F[X]) → F[X]) g'
⊢ Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X]) ((expand F (q ^ m') : (a : F[X]) → F[X]) g' : F[X])
have prime₁ : f = f
Tactic: rw [hm, hm']
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SmallDegreeVieta (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : p.degree ≤ 2
⊢ p =
    HAdd.hAdd (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 2) : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
have rw : ∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i) =
  (C : (a : R) → R[X])
          (coeff
            (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i))
            2) *
        HPow.hPow (α := R[X]) (β := ℕ) X 2 +
      HMul.hMul (α := R[X])
        ((C : (a : R) → R[X])
          (coeff
            (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i))
            1))
        X +
    (C : (a : R) → R[X])
      (coeff
        (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i))
        0)
Tactic: rw [p.as_sum_range_C_mul_X_pow'
    (Nat.lt_of_le_of_lt (natDegree_le_iff_degree_le.mpr hp) (Nat.lt_add_one 2))]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SmallDegreeVieta (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : p.degree ≤ 2
⊢ ∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i) =
    (C : (a : R) → R[X])
            (coeff
              (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i))
              2) *
          HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        HMul.hMul (α := R[X])
          ((C : (a : R) → R[X])
            (coeff
              (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i))
              1))
          X +
      (C : (a : R) → R[X])
        (coeff
          (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i))
          0)
have simp : HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X) +
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 2) : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) =
  HAdd.hAdd (β := R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 2) : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
    ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
Tactic: simp [Finset.sum_range_succ]