awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
this : NeZero (finrank K L)
tfae_1_to_3 :
  ∀ (a : IsGalois K L ∧ IsCyclic.{u_2} Gal(L/K)),
    ∃ (α : L),
      Membership.mem (γ := Set L) (Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
          (α ^ finrank K L) ∧
        Eq (α := IntermediateField K L) K⟮α⟯ ⊤
tfae_3_to_2 :
  ∀
    (a :
      ∃ (α : L),
        Membership.mem (γ := Set L) (Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
            (α ^ finrank K L) ∧
          Eq (α := IntermediateField K L) K⟮α⟯ ⊤),
    ∃ (a : K),
      Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) ∧
        IsSplittingField K L
          (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]))
⊢ ∃ (a : K),
    Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) ∧
      IsSplittingField K L
        (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]))

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
this : NeZero (finrank K L)
tfae_1_to_3 :
  ∀ (a : IsGalois K L ∧ IsCyclic.{u_2} Gal(L/K)),
    ∃ (α : L),
      Membership.mem (γ := Set L) (Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
          (α ^ finrank K L) ∧
        Eq (α := IntermediateField K L) K⟮α⟯ ⊤
tfae_3_to_2 :
  ∀
    (a :
      ∃ (α : L),
        Membership.mem (γ := Set L) (Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
            (α ^ finrank K L) ∧
          Eq (α := IntermediateField K L) K⟮α⟯ ⊤),
    ∃ (a : K),
      Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) ∧
        IsSplittingField K L
          (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]))
⊢ IsGalois K L ∧ IsCyclic.{u_2} Gal(L/K)

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
this : NeZero (finrank K L)
tfae_1_to_3 :
  ∀ (a : IsGalois K L ∧ IsCyclic.{u_2} Gal(L/K)),
    ∃ (α : L),
      Membership.mem (γ := Set L) (Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
          (α ^ finrank K L) ∧
        Eq (α := IntermediateField K L) K⟮α⟯ ⊤
tfae_3_to_2 :
  ∀
    (a :
      ∃ (α : L),
        Membership.mem (γ := Set L) (Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
            (α ^ finrank K L) ∧
          Eq (α := IntermediateField K L) K⟮α⟯ ⊤),
    ∃ (a : K),
      Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) ∧
        IsSplittingField K L
          (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]))
⊢ ∀
    (a :
      ∃ (a : K),
        Irreducible
            (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) ∧
          IsSplittingField K L
            (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]))),
    IsGalois K L ∧ IsCyclic.{u_2} Gal(L/K)

Tactic:
2 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
this : NeZero (finrank K L)
tfae_1_to_3 :
  ∀ (a : IsGalois K L ∧ IsCyclic.{u_2} Gal(L/K)),
    ∃ (α : L),
      Membership.mem (γ := Set L) (Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
          (α ^ finrank K L) ∧
        Eq (α := IntermediateField K L) K⟮α⟯ ⊤
tfae_3_to_2 :
  ∀
    (a :
      ∃ (α : L),
        Membership.mem (γ := Set L) (Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
            (α ^ finrank K L) ∧
          Eq (α := IntermediateField K L) K⟮α⟯ ⊤),
    ∃ (a : K),
      Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) ∧
        IsSplittingField K L
          (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]))
⊢ ∀
    (a :
      ∃ (a : K),
        Irreducible
            (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) ∧
          IsSplittingField K L
            (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]))),
    IsGalois K L ∧ IsCyclic.{u_2} Gal(L/K)

Tactic:
tfae_have 2 → 1
  | ⟨a, H, inst⟩ => ⟨isGalois_of_isSplittingField_X_pow_sub_C hK H L,
      isCyclic_of_isSplittingField_X_pow_sub_C hK H L⟩
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
this : NeZero (finrank K L)
tfae_1_to_3 :
  ∀ (a : IsGalois K L ∧ IsCyclic.{u_2} Gal(L/K)),
    ∃ (α : L),
      Membership.mem (γ := Set L) (Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
          (α ^ finrank K L) ∧
        Eq (α := IntermediateField K L) K⟮α⟯ ⊤
tfae_3_to_2 :
  ∀
    (a :
      ∃ (α : L),
        Membership.mem (γ := Set L) (Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
            (α ^ finrank K L) ∧
          Eq (α := IntermediateField K L) K⟮α⟯ ⊤),
    ∃ (a : K),
      Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) ∧
        IsSplittingField K L
          (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]))
tfae_2_to_1 :
  ∀
    (a :
      ∃ (a : K),
        Irreducible
            (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) ∧
          IsSplittingField K L
            (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X]))),
    IsGalois K L ∧ IsCyclic.{u_2} Gal(L/K)
⊢ [IsGalois K L ∧ IsCyclic.{u_2} Gal(L/K),
      ∃ (a : K),
        Irreducible
            (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])) ∧
          IsSplittingField K L
            (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X (finrank K L)) ((C : (a : K) → K [X]) a : K [X])),
      ∃ (α : L),
        Membership.mem (γ := Set L) (Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
            (α ^ finrank K L) ∧
          Eq (α := IntermediateField K L) K⟮α⟯ ⊤].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.FieldTheory.KummerPolynomial
Goal:
K : Type u
inst : Field K
n : ℕ
hn : 1 < n
a : K
rwa : natDegree.{u} (R := K) X < n
rwa₁ rwa₂ rwa₃ rwa₄ : 1 < n
⊢ natDegree.{u} (R := K) X <
    (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).natDegree

Tactic:
rwa [natDegree_X_pow_sub_C, natDegree_X]

Premises used: Polynomial.natDegree_X, Polynomial.natDegree_X_pow_sub_C
-- Module: Mathlib.FieldTheory.KummerPolynomial
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
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
⊢ 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

Premises used: Iff.mpr, LE.le.eq_or_lt, Nat.succ_le_iff, rfl
-- Module: Mathlib.FieldTheory.KummerPolynomial
Goal:
K : Type u
inst : Field K
a : K
ha : a ≠ 0
hn : 0 < Nat.succ 0
inl : root (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) ≠ 0
⊢ root (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (Nat.succ 0)) ((C : (a : K) → K[X]) a : K[X])) ≠ 0

Tactic:
rw [pow_one]

Premises used: pow_one
-- Module: Mathlib.FieldTheory.KummerPolynomial
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
⊢ natDegree.{u} (R := K) ((C : (a : K) → K[X]) a) <
    (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])).natDegree

Tactic:
simp
-- Module: Mathlib.FieldTheory.KummerPolynomial
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
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])))
⊢ False

Tactic:
refine mk_ne_zero_of_natDegree_lt (monic_X_sub_C a) (C_ne_zero.mpr ha) (by simp) ?_

Premises used: Iff.mpr, Polynomial.monic_X_sub_C, AdjoinRoot.mk_ne_zero_of_natDegree_lt, Polynomial.C_ne_zero
-- Module: Mathlib.FieldTheory.KummerPolynomial
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])))
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])))
⊢ 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:
trans AdjoinRoot.mk (X - C a) (X - (X - C a))

Premises used: Polynomial.C, HSub.hSub, AdjoinRoot.mk, Polynomial.X, DFunLike.coe
-- Module: Mathlib.FieldTheory.KummerPolynomial
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 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])))
⊢ 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:
rw [sub_sub_cancel]

Premises used: sub_sub_cancel
-- Module: Mathlib.FieldTheory.KummerPolynomial
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
rw₄ rw₅ : Eq.{u + 1} (α := AdjoinRoot (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[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])))

Tactic:
rw [map_sub, mk_self, sub_zero, mk_X, e]

Premises used: map_sub, sub_zero, AdjoinRoot.mk_X, AdjoinRoot.mk_self
-- Module: Mathlib.FieldTheory.KummerPolynomial
Goal:
K : Type u
inst : Field K
n : ℕ
a : K
hn_1 : 0 < n
ha : a ≠ 0
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:
root_X_pow_sub_C_ne_zero hn a

Premises used: root_X_pow_sub_C_ne_zero
-- Module: Mathlib.FieldTheory.KummerPolynomial
Goal:
K : Type u
inst : Field K
n : ℕ
a : K
hn_1 : 0 < n
ha : a ≠ 0
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:
exact root_X_pow_sub_C_ne_zero hn a

Premises used: root_X_pow_sub_C_ne_zero
-- Module: Mathlib.FieldTheory.KummerPolynomial
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]))
⊢ Irreducible (M := K[X]) ((C : (a : K) → K[X]) (1 - a) : K[X])

Tactic:
rw [pow_zero, ← C.map_one, ← map_sub] at H

Premises used: Polynomial.C, map_sub, RingHom.map_one, pow_zero
-- Module: Mathlib.FieldTheory.KummerPolynomial
Goal:
K : Type u
inst : Field K
a : K
H : Irreducible (M := K[X]) ((C : (a : K) → K[X]) (1 - a) : K[X])
⊢ False

Tactic:
not_irreducible_C _ H

Premises used: Polynomial.not_irreducible_C
-- Module: Mathlib.FieldTheory.KummerPolynomial
Goal:
K : Type u
inst : Field K
a : K
H : Irreducible (M := K[X]) ((C : (a : K) → K[X]) (1 - a) : K[X])
⊢ False

Tactic:
exact not_irreducible_C _ H

Premises used: Polynomial.not_irreducible_C
-- Module: Mathlib.FieldTheory.KummerPolynomial
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)
⊢ Irreducible (HPow.hPow (α := K[X]) X n)

Tactic:
rw [map_zero, sub_zero] at H

Premises used: sub_zero, map_zero
-- Module: Mathlib.FieldTheory.KummerPolynomial
Goal:
K : Type u
inst : Field K
n : ℕ
hn : n ≠ 1
H : Irreducible (HPow.hPow (α := K[X]) X n)
⊢ False

Tactic:
not_irreducible_pow hn H

Premises used: not_irreducible_pow
-- Module: Mathlib.FieldTheory.KummerPolynomial
Goal:
K : Type u
inst : Field K
n : ℕ
hn : n ≠ 1
H : Irreducible (HPow.hPow (α := K[X]) X n)
⊢ False

Tactic:
exact not_irreducible_pow hn H

Premises used: not_irreducible_pow
-- Module: Mathlib.FieldTheory.KummerPolynomial
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]))
⊢ 0 < n

Tactic:
have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
-- Module: Mathlib.FieldTheory.KummerPolynomial
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

Tactic:
⟨not_imp_not.mp (root_X_pow_sub_C_ne_zero' hn), ?_⟩

Premises used: root_X_pow_sub_C_ne_zero', Iff.intro, Iff.mp, not_imp_not
-- Module: Mathlib.FieldTheory.KummerPolynomial
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
refine : a = 0 → root (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])) = 0 ↔ a = 0

Tactic:
refine ⟨not_imp_not.mp (root_X_pow_sub_C_ne_zero' hn), ?_⟩
-- Module: Mathlib.FieldTheory.KummerPolynomial
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)
⊢ n = 1

Tactic:
have := not_imp_not.mp (fun hn ↦ ne_zero_of_irreducible_X_pow_sub_C' hn H) rfl
-- Module: Mathlib.FieldTheory.KummerPolynomial
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
rw₅ rw₆ : Eq.{u + 1} (α := AdjoinRoot (R := K) X) 0 0
⊢ root (HPow.hPow (α := K[X]) X n - (C : (a : K) → K[X]) 0) = 0

Tactic:
rw [this, pow_one, map_zero, sub_zero, ← mk_X, mk_self]

Premises used: sub_zero, map_zero, pow_one, AdjoinRoot.mk_X, AdjoinRoot.mk_self
-- Module: Mathlib.FieldTheory.KummerPolynomial
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

Tactic:
(root_X_pow_sub_C_eq_zero_iff H).not

Premises used: root_X_pow_sub_C_eq_zero_iff, Iff.not
-- Module: Mathlib.FieldTheory.KummerPolynomial
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
e : n = 0
⊢ Irreducible (M := K[X]) ((C : (a : K) → K[X]) (1 - a) : K[X])

Tactic:
simpa only [e, pow_zero, ← C.map_one, ← map_sub] using H

Premises used: Polynomial.C, map_sub, RingHom.map_one, pow_zero
-- Module: Mathlib.FieldTheory.KummerPolynomial
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
⊢ 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)
-- Module: Mathlib.FieldTheory.KummerPolynomial
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
hn : n ≠ 0
obtain :
  ∀ (k : ℕ) (H : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (m * k)) ((C : (a : K) → K[X]) a : K[X])))
    (hn : m * k ≠ 0), b ^ m ≠ a
⊢ b ^ m ≠ a

Tactic:
obtain ⟨k, rfl⟩ := hm

Premises used: rfl
-- Module: Mathlib.FieldTheory.KummerPolynomial
Goal:
K : Type u
inst : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
H : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (m * k)) ((C : (a : K) → K[X]) (b ^ m) : K[X]))
obtain :
  ∀ (q : K[X])
    (hq :
      HPow.hPow (α := K[X]) X k ^ m - HPow.hPow (α := K[X]) ((C : (a : K) → K[X]) b : K[X]) m =
        HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X k) ((C : (a : K) → K[X]) b : K[X]) * q),
    False
⊢ False

Tactic:
obtain ⟨q, hq⟩ := sub_dvd_pow_sub_pow (X ^ k) (C b) m

Premises used: Polynomial.C, HPow.hPow, Polynomial.X, sub_dvd_pow_sub_pow, DFunLike.coe
-- Module: Mathlib.FieldTheory.KummerPolynomial
Goal:
K : Type u
inst : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
H : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (m * k)) ((C : (a : K) → K[X]) (b ^ m) : K[X]))
q : K[X]
hq :
  HPow.hPow (α := K[X]) X k ^ m - HPow.hPow (α := K[X]) ((C : (a : K) → K[X]) b : K[X]) m =
    HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X k) ((C : (a : K) → K[X]) b : K[X]) * q
rw :
  ∀ (q : K[X]) (H : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X k) ((C : (a : K) → K[X]) b : K[X]) * q))
    (hq :
      HPow.hPow (α := K[X]) X k ^ m - HPow.hPow (α := K[X]) ((C : (a : K) → K[X]) b : K[X]) m =
        HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X k) ((C : (a : K) → K[X]) b : K[X]) * q),
    False
⊢ False

Tactic:
rw [mul_comm, pow_mul, map_pow, hq] at H

Premises used: map_pow, pow_mul, mul_comm
-- Module: Mathlib.FieldTheory.KummerPolynomial
Goal:
K : Type u
inst : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
q : K[X]
H : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X k) ((C : (a : K) → K[X]) b : K[X]) * q)
hq :
  HPow.hPow (α := K[X]) X k ^ m - HPow.hPow (α := K[X]) ((C : (a : K) → K[X]) b : K[X]) m =
    HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X k) ((C : (a : K) → K[X]) b : K[X]) * q
⊢ q.degree = 0

Tactic:
simpa [isUnit_iff_degree_eq_zero, degree_X_pow_sub_C,
      Nat.pos_iff_ne_zero, (mul_ne_zero_iff.mp hn).2] using H.2 rfl

Premises used: Nat.pos_iff_ne_zero, Polynomial.degree_X_pow_sub_C, And.right, Irreducible.isUnit_or_isUnit, Iff.mp, Polynomial.isUnit_iff_degree_eq_zero, rfl, mul_ne_zero_iff