awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
a : K
rw :
  HSub.hSub (β := AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
      (root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) ^ n)
      ((of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) :
            (a_1 : K) → AdjoinRoot (X ^ n - (C : (a : K) → K[X]) a))
          a :
        AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))) =
    0
⊢ root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) ^ n =
    (of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) :
        (a_1 : K) → AdjoinRoot (X ^ n - (C : (a : K) → K[X]) a))
      a
have rw₁ : HSub.hSub (β := AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
    (root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) ^ n)
    ((of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) :
          (a_1 : K) → AdjoinRoot (X ^ n - (C : (a : K) → K[X]) a))
        a :
      AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))) =
  eval₂ (of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
    (root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
    (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))
Tactic: rw [← sub_eq_zero, ← AdjoinRoot.eval₂_root, eval₂_sub, eval₂_C, eval₂_pow, eval₂_X]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
a : K
rw :
  HSub.hSub (β := AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
      (root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) ^ n)
      ((of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) :
            (a_1 : K) → AdjoinRoot (X ^ n - (C : (a : K) → K[X]) a))
          a :
        AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))) =
    0
rw₁ :
  HSub.hSub (β := AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
      (root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) ^ n)
      ((of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) :
            (a_1 : K) → AdjoinRoot (X ^ n - (C : (a : K) → K[X]) a))
          a :
        AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))) =
    eval₂ (of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
      (root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
      (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))
⊢ root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) ^ n =
    (of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) :
        (a_1 : K) → AdjoinRoot (X ^ n - (C : (a : K) → K[X]) a))
      a
have rw₂ : HSub.hSub (β := AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
    (root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) ^ n)
    ((of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) :
          (a_1 : K) → AdjoinRoot (X ^ n - (C : (a : K) → K[X]) a))
        a :
      AdjoinRoot (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))) =
  eval₂ (of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
      (root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
      (HPow.hPow (α := K[X]) X n) -
    eval₂ (of (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
      (root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
      ((C : (a : K) → K[X]) a)
Tactic: rw [← sub_eq_zero, ← AdjoinRoot.eval₂_root, eval₂_sub, eval₂_C, eval₂_pow, eval₂_X]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
hn : 1 < n
a : K
⊢ natDegree.{u} (R := K) X <
    (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).natDegree
have rwa : natDegree.{u} (R := K) X < n
Tactic: rwa [natDegree_X_pow_sub_C, natDegree_X]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
a : K
hn : 0 < n
ha : a ≠ 0
⊢ root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) ≠ 0
have inl : ∀ (hn : 0 < Nat.succ 0),
  root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (Nat.succ 0)) ((C : (a : K) → K[X]) a : K[X])) ≠ 0
Tactic: obtain (rfl | hn) := (Nat.succ_le_iff.mpr hn).eq_or_lt
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
a : K
hn : 0 < n
ha : a ≠ 0
inl :
  ∀ (hn : 0 < Nat.succ 0),
    root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (Nat.succ 0)) ((C : (a : K) → K[X]) a : K[X])) ≠ 0
⊢ root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) ≠ 0
have inr : ∀ (hn : Nat.succ 0 < n), root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) ≠ 0
Tactic: obtain (rfl | hn) := (Nat.succ_le_iff.mpr hn).eq_or_lt
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
a : K
ha : a ≠ 0
hn : 0 < Nat.succ 0
⊢ root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (Nat.succ 0)) ((C : (a : K) → K[X]) a : K[X])) ≠ 0
have inl : root (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) ≠ 0
Tactic: rw [pow_one]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
a : K
ha : a ≠ 0
hn : 0 < Nat.succ 0
e : root (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) = 0
⊢ False
have inl : Eq (α := AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
  ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
        (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
      ((C : (a : K) → K[X]) a) :
    AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
  (0 : AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
Tactic: refine mk_ne_zero_of_natDegree_lt (monic_X_sub_C a) (C_ne_zero.mpr ha) (by simp) ?_
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
a : K
ha : a ≠ 0
hn : 0 < Nat.succ 0
e : root (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) = 0
⊢ Eq (α := AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
    ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
          (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
        ((C : (a : K) → K[X]) a) :
      AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
    (0 : AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
have trans : Eq (α := AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
  ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
        (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
      ((C : (a : K) → K[X]) a) :
    AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
  ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
        (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
      (X - HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
    AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
Tactic: trans AdjoinRoot.mk (X - C a) (X - (X - C a))
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
a : K
ha : a ≠ 0
hn : 0 < Nat.succ 0
e : root (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) = 0
trans :
  Eq (α := AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
    ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
          (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
        ((C : (a : K) → K[X]) a) :
      AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
    ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
          (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
        (X - HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
      AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
⊢ Eq (α := AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
    ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
          (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
        ((C : (a : K) → K[X]) a) :
      AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
    (0 : AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
have trans₁ : Eq (α := AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
  ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
        (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
      (X - HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
    AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
  (0 : AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
Tactic: trans AdjoinRoot.mk (X - C a) (X - (X - C a))
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
a : K
ha : a ≠ 0
hn : 0 < Nat.succ 0
e : root (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) = 0
⊢ Eq (α := AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
    ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
          (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
        ((C : (a : K) → K[X]) a) :
      AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
    ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
          (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
        (X - HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
      AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
have rw : Eq (α := AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
  ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
        (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
      ((C : (a : K) → K[X]) a) :
    AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
  ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
        (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
      ((C : (a : K) → K[X]) a) :
    AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
Tactic: rw [sub_sub_cancel]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
a : K
ha : a ≠ 0
hn : 0 < Nat.succ 0
e : root (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) = 0
⊢ Eq (α := AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
    ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
          (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
        (X - HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
      AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
    (0 : AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
have rw : HSub.hSub (α := AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
    ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
        (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
      X)
    ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
        (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
      (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))) =
  0
Tactic: rw [map_sub, mk_self, sub_zero, mk_X, e]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
a : K
ha : a ≠ 0
hn : 0 < Nat.succ 0
e : root (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) = 0
rw :
  HSub.hSub (α := AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
      ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
          (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
        X)
      ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
          (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
        (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))) =
    0
⊢ Eq (α := AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
    ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
          (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
        (X - HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
      AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
    (0 : AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
have rw₁ : HSub.hSub (α := AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
    ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
        (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
      X)
    0 =
  0
Tactic: rw [map_sub, mk_self, sub_zero, mk_X, e]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
a : K
ha : a ≠ 0
hn : 0 < Nat.succ 0
e : root (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) = 0
rw :
  HSub.hSub (α := AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
      ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
          (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
        X)
      ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
          (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
        (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))) =
    0
rw₁ :
  HSub.hSub (α := AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
      ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
          (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
        X)
      0 =
    0
⊢ Eq (α := AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
    ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
          (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
        (X - HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
      AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
    (0 : AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
have rw₂ : Eq (α := AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
  ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
      (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
    X)
  0
Tactic: rw [map_sub, mk_self, sub_zero, mk_X, e]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
a : K
ha : a ≠ 0
hn : 0 < Nat.succ 0
e : root (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) = 0
rw :
  HSub.hSub (α := AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
      ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
          (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
        X)
      ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
          (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
        (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))) =
    0
rw₁ :
  HSub.hSub (α := AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
      ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
          (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
        X)
      0 =
    0
rw₂ :
  Eq (α := AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
    ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
        (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
      X)
    0
rw₃ : root (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) = 0
⊢ Eq (α := AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
    ((mk (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
          (a_1 : K[X]) → AdjoinRoot (X - (C : (a : K) → K[X]) a))
        (X - HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
      AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
    (0 : AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])))
have rw₄ : Eq.{u + 1} (α := AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))) 0 0
Tactic: rw [map_sub, mk_self, sub_zero, mk_X, e]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (hypothesis)
Goal:
K : Type u
inst : Field K
a : K
H : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) (β := ℕ) X 0) ((C : (a : K) → K[X]) a : K[X]))
⊢ False
have H₁ : Irreducible (M := K[X]) ((C : (a : K) → K[X]) (1 - a) : K[X])
Tactic: rw [pow_zero, ← C.map_one, ← map_sub] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (hypothesis)
Goal:
K : Type u
inst : Field K
n : ℕ
hn : n ≠ 1
H : Irreducible (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 0)
⊢ False
have H₁ : Irreducible (HPow.hPow (α := K[X]) X n)
Tactic: rw [map_zero, sub_zero] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (hypothesis)
Goal:
K : Type u
inst : Field K
n : ℕ
a : K
H : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))
⊢ root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) = 0 ↔ a = 0
have hn : 0 < n
Tactic: have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
a : K
H : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))
hn : 0 < n
⊢ root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) = 0 ↔ a = 0
have refine : a = 0 → root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) = 0
Tactic: refine ⟨not_imp_not.mp (root_X_pow_sub_C_ne_zero' hn), ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (hypothesis)
Goal:
K : Type u
inst : Field K
n : ℕ
hn : 0 < n
H : Irreducible (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 0)
⊢ root (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 0) = 0
have this : n = 1
Tactic: have := not_imp_not.mp (fun hn ↦ ne_zero_of_irreducible_X_pow_sub_C' hn H) rfl
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
hn : 0 < n
H : Irreducible (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 0)
this : n = 1
⊢ root (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 0) = 0
have rw : root (HPow.hPow (α := K[X]) (β := ℕ) X 1 - (C : (a : K) → K[X]) 0) = 0
Tactic: rw [this, pow_one, map_zero, sub_zero, ← mk_X, mk_self]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
hn : 0 < n
H : Irreducible (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 0)
this : n = 1
rw : root (HPow.hPow (α := K[X]) (β := ℕ) X 1 - (C : (a : K) → K[X]) 0) = 0
⊢ root (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 0) = 0
have rw₁ : root (HSub.hSub (α := K[X]) X ((C : (a : K) → K[X]) 0)) = 0
Tactic: rw [this, pow_one, map_zero, sub_zero, ← mk_X, mk_self]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
hn : 0 < n
H : Irreducible (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 0)
this : n = 1
rw : root (HPow.hPow (α := K[X]) (β := ℕ) X 1 - (C : (a : K) → K[X]) 0) = 0
rw₁ : root (HSub.hSub (α := K[X]) X ((C : (a : K) → K[X]) 0)) = 0
⊢ root (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 0) = 0
have rw₂ : root (HSub.hSub (α := K[X]) X 0) = 0
Tactic: rw [this, pow_one, map_zero, sub_zero, ← mk_X, mk_self]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
hn : 0 < n
H : Irreducible (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 0)
this : n = 1
rw : root (HPow.hPow (α := K[X]) (β := ℕ) X 1 - (C : (a : K) → K[X]) 0) = 0
rw₁ : root (HSub.hSub (α := K[X]) X ((C : (a : K) → K[X]) 0)) = 0
rw₂ : root (HSub.hSub (α := K[X]) X 0) = 0
⊢ root (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 0) = 0
have rw₃ : Eq.{u + 1} (α := AdjoinRoot (R := K) X) (root X) 0
Tactic: rw [this, pow_one, map_zero, sub_zero, ← mk_X, mk_self]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
hn : 0 < n
H : Irreducible (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 0)
this : n = 1
rw : root (HPow.hPow (α := K[X]) (β := ℕ) X 1 - (C : (a : K) → K[X]) 0) = 0
rw₁ : root (HSub.hSub (α := K[X]) X ((C : (a : K) → K[X]) 0)) = 0
rw₂ : root (HSub.hSub (α := K[X]) X 0) = 0
rw₃ : Eq.{u + 1} (α := AdjoinRoot (R := K) X) (root X) 0
⊢ root (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 0) = 0
have rw₄ : Eq.{u + 1} (α := AdjoinRoot (R := K) X) ((mk X : (a : K[X]) → AdjoinRoot X) X) 0
Tactic: rw [this, pow_one, map_zero, sub_zero, ← mk_X, mk_self]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
hn : 0 < n
H : Irreducible (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 0)
this : n = 1
rw : root (HPow.hPow (α := K[X]) (β := ℕ) X 1 - (C : (a : K) → K[X]) 0) = 0
rw₁ : root (HSub.hSub (α := K[X]) X ((C : (a : K) → K[X]) 0)) = 0
rw₂ : root (HSub.hSub (α := K[X]) X 0) = 0
rw₃ : Eq.{u + 1} (α := AdjoinRoot (R := K) X) (root X) 0
rw₄ : Eq.{u + 1} (α := AdjoinRoot (R := K) X) ((mk X : (a : K[X]) → AdjoinRoot X) X) 0
⊢ root (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 0) = 0
have rw₅ : Eq.{u + 1} (α := AdjoinRoot (R := K) X) 0 0
Tactic: rw [this, pow_one, map_zero, sub_zero, ← mk_X, mk_self]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (hypothesis)
Goal:
K : Type u
inst : Field K
n : ℕ
a : K
H : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))
m : ℕ
hm : m ∣ n
hm' : m ≠ 1
b : K
⊢ b ^ m ≠ a
have hn : n ≠ 0
Tactic: have hn : n ≠ 0 := fun e ↦ not_irreducible_C
    (1 - a) (by simpa only [e, pow_zero, ← C.map_one, ← map_sub] using H)