awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
inst_1 : NeZero n
e : Gal(K[n√a]/K)
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this : Algebra K K[n√a] := inferInstance
h : a = 0
pos :
  ∀ (hζ : (primitiveRoots 1 K).Nonempty)
    (H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])))
    [NeZero (R := ℕ) 1] (e : K[1√a] ≃ₐ[K] K[1√a])
    (this :
      Fact
        (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])))),
    1 * root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) =
      (e : (a_1 : K[1√a]) → K[1√a])
        (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])))
⊢ 1 * root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) =
    (e : (a_1 : K[n√a]) → K[n√a])
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))

Tactic:
obtain rfl := not_imp_not.mp (fun hn ↦ ne_zero_of_irreducible_X_pow_sub_C' hn H) h

Premises used: ne_zero_of_irreducible_X_pow_sub_C', Iff.mp, rfl, not_imp_not
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
a : K
h : a = 0
hζ : (primitiveRoots 1 K).Nonempty
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X]))
inst_1 : NeZero (R := ℕ) 1
__spread.0 : ↥(rootsOfUnity 1 K) →* Gal(K[1√a]/K) := autAdjoinRootXPowSubC 1 a
e : Gal(K[1√a]/K)
this_1 :
  Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])))
this : Algebra K K[1√a] := inferInstance
pos :
  HMul.hMul (α := K[1√a]) (β := K[1√a]) (1 : K[1√a])
      ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) :
            (a_1 : K) → K[1√a])
          a :
        K[1√a]) =
    (e : (a_1 : K[1√a]) → K[1√a])
      ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) :
          (a_1 : K) → K[1√a])
        a)
pos₁ :
  Eq (α := K[1√a])
    ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) :
          (a_1 : K) → K[1√a])
        a :
      K[1√a])
    ((e : (a_1 : K[1√a]) → K[1√a])
        ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) :
            (a_1 : K) → K[1√a])
          a) :
      K[1√a])
pos₂ :
  Eq (α := K[1√a]) ((algebraMap K K[1√a] : (a_1 : K) → K[1√a]) a : K[1√a])
    ((e : (a_1 : K[1√a]) → K[1√a]) ((algebraMap K K[1√a] : (a_1 : K) → K[1√a]) a) : K[1√a])
pos₃ pos₄ :
  Eq (α := K[1√a]) ((algebraMap K K[1√a] : (a_1 : K) → K[1√a]) a : K[1√a])
    ((algebraMap K K[1√a] : (a_1 : K) → K[1√a]) a : K[1√a])
⊢ 1 * root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])) =
    (e : (a_1 : K[1√a]) → K[1√a])
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])))

Tactic:
rw [(pow_one _).symm.trans (root_X_pow_sub_C_pow 1 a), one_mul,
        ← AdjoinRoot.algebraMap_eq, AlgEquiv.commutes]

Premises used: AdjoinRoot.algebraMap_eq, AlgEquiv.commutes, root_X_pow_sub_C_pow, pow_one, OfNat.ofNat, Eq.symm, one_mul, Eq.trans
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
inst_1 : NeZero n
e : Gal(K[n√a]/K)
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this : Algebra K K[n√a] := inferInstance
h : ¬a = 0
⊢ HDiv.hDiv (α := K[n√a])
        ((e : (a_1 : K[n√a]) → K[n√a])
            (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
          K[n√a])
        (root (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])) =
    (e : (a_1 : K[n√a]) → K[n√a])
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))

Tactic:
div_mul_cancel₀ _ (root_X_pow_sub_C_ne_zero' (NeZero.pos n) h)

Premises used: div_mul_cancel₀, root_X_pow_sub_C_ne_zero', NeZero.pos
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
inst_1 : NeZero n
e : Gal(K[n√a]/K)
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this : Algebra K K[n√a] := inferInstance
h : ¬a = 0
⊢ HDiv.hDiv (α := K[n√a])
        ((e : (a_1 : K[n√a]) → K[n√a])
            (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
          K[n√a])
        (root (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])) =
    (e : (a_1 : K[n√a]) → K[n√a])
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))

Tactic:
refine div_mul_cancel₀ _ (root_X_pow_sub_C_ne_zero' (NeZero.pos n) h)

Premises used: div_mul_cancel₀, root_X_pow_sub_C_ne_zero', NeZero.pos
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
inst_1 : NeZero n
η : ↥(rootsOfUnity n K)
⊢ (((autAdjoinRootXPowSubCEquiv hζ H : (a_1 : ↥(rootsOfUnity n K)) → K[n√a] ≃ₐ[K] K[n√a]) η : K[n√a] ≃ₐ[K] K[n√a]) :
        (a_1 : K[n√a]) → K[n√a])
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) =
    (↑(↑η : Kˣ) : K) • root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))

Tactic:
autAdjoinRootXPowSubC_root a η

Premises used: autAdjoinRootXPowSubC_root
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
inst_1 : NeZero n
σ : K[n√a] ≃ₐ[K] K[n√a]
⊢ Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))

Tactic:
have := Fact.mk H
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
inst_1 : NeZero n
σ : Gal(K[n√a]/K)
this : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
simp :
  (if a = 0 then root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
    else
      HDiv.hDiv (α := K[n√a])
          ((σ : (a_1 : K[n√a]) → K[n√a])
              (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
            K[n√a])
          (root (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]))) =
    (σ : (a_1 : K[n√a]) → K[n√a])
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
⊢ HSMul.hSMul (α := Kˣ) (↑(((autAdjoinRootXPowSubCEquiv hζ H).symm : (a : Gal(K[n√a]/K)) → ↥(rootsOfUnity n K)) σ) : Kˣ)
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) =
    (σ : (a_1 : K[n√a]) → K[n√a])
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))

Tactic:
simp only [autAdjoinRootXPowSubCEquiv, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe,
    MulEquiv.symm_mk, MulEquiv.coe_mk, Equiv.coe_fn_symm_mk, AdjoinRootXPowSubCEquivToRootsOfUnity,
    AdjoinRoot.algebraMap_eq, rootsOfUnity.mkOfPowEq, Units.smul_def, Algebra.smul_def,
    rootsOfUnityEquivOfPrimitiveRoots_symm_apply, Units.val_ofPowEqOne, ite_mul, one_mul]

Premises used: MulEquiv.symm_mk, Equiv.coe_fn_symm_mk, AdjoinRoot.algebraMap_eq, MonoidHom.toOneHom_coe, autAdjoinRootXPowSubCEquiv, MulEquiv.coe_mk, AdjoinRootXPowSubCEquivToRootsOfUnity, Units.smul_def, ite_mul, Algebra.smul_def, rootsOfUnity.mkOfPowEq, Units.val_ofPowEqOne, rootsOfUnityEquivOfPrimitiveRoots_symm_apply, one_mul, OneHom.toFun_eq_coe
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
inst_1 : NeZero n
σ : Gal(K[n√a]/K)
this : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
simp_rw :
  (if root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) = 0 then
      root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
    else
      HDiv.hDiv (α := K[n√a])
          ((σ : (a_1 : K[n√a]) → K[n√a])
              (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
            K[n√a])
          (root (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]))) =
    (σ : (a_1 : K[n√a]) → K[n√a])
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
⊢ (if a = 0 then root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
    else
      HDiv.hDiv (α := K[n√a])
          ((σ : (a_1 : K[n√a]) → K[n√a])
              (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
            K[n√a])
          (root (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]))) =
    (σ : (a_1 : K[n√a]) → K[n√a])
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))

Tactic:
simp_rw [← root_X_pow_sub_C_eq_zero_iff H]

Premises used: root_X_pow_sub_C_eq_zero_iff
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
inst_1 : NeZero n
σ : Gal(K[n√a]/K)
this : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
pos :
  ∀ (h : 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])) =
      (σ : (a_1 : K[n√a]) → K[n√a])
        (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
neg :
  ∀ (h : ¬root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) = 0),
    HDiv.hDiv (α := K[n√a])
          ((σ : (a_1 : K[n√a]) → K[n√a])
              (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
            K[n√a])
          (root (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])) =
      (σ : (a_1 : K[n√a]) → K[n√a])
        (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
⊢ (if root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) = 0 then
      root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
    else
      HDiv.hDiv (α := K[n√a])
          ((σ : (a_1 : K[n√a]) → K[n√a])
              (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
            K[n√a])
          (root (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]))) =
    (σ : (a_1 : K[n√a]) → K[n√a])
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))

Tactic:
split_ifs with h
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
inst_1 : NeZero n
σ : Gal(K[n√a]/K)
this : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
h : root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) = 0
pos : Eq (α := K[n√a]) 0 ((σ : (a_1 : K[n√a]) → K[n√a]) 0)
pos₁ pos₂ : Eq.{u + 1} (α := K[n√a]) 0 0
⊢ root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) =
    (σ : (a_1 : K[n√a]) → K[n√a])
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))

Tactic:
rw [h, map_zero]

Premises used: map_zero
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
inst_1 : NeZero n
σ : Gal(K[n√a]/K)
this : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
h : ¬root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) = 0
neg neg₁ :
  Eq (α := K[n√a])
    ((σ : (a_1 : K[n√a]) → K[n√a])
        (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
      K[n√a])
    ((σ : (a_1 : K[n√a]) → K[n√a])
        (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
      K[n√a])
⊢ HDiv.hDiv (α := K[n√a])
        ((σ : (a_1 : K[n√a]) → K[n√a])
            (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
          K[n√a])
        (root (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])) =
    (σ : (a_1 : K[n√a]) → K[n√a])
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))

Tactic:
rw [div_mul_cancel₀ _ h]

Premises used: div_mul_cancel₀
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
⊢ Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))

Tactic:
have := Fact.mk H
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this : Algebra K K[n√a] := inferInstance
splits' :
  Splits (R := K[n√a])
    (Polynomial.map (algebraMap K K[n√a])
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
adjoin_rootSet' :
  Eq (α := Subalgebra K K[n√a])
    (Algebra.adjoin K
      ((HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])).rootSet K[n√a]))
    ⊤
⊢ IsSplittingField K K[n√a] (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))

Tactic:
constructor
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this : Algebra K K[n√a] := inferInstance
splits' :
  (HSub.hSub (β := K[n√a][X]) (HPow.hPow (α := K[n√a][X]) X n)
      ((C : (a_1 : K[n√a]) → K[n√a][X]) (((algebraMap K K[n√a] : K →+* K[n√a]) : (a_1 : K) → K[n√a]) a) :
        K[n√a][X])).Splits
⊢ Splits (R := K[n√a])
    (Polynomial.map (algebraMap K K[n√a])
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))

Tactic:
rw [Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_C,
      Polynomial.map_X]

Premises used: Polynomial.map_pow, Polynomial.map_X, Polynomial.map_sub, Polynomial.map_C
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this : Algebra K K[n√a] := inferInstance
splits' :
  ∀ (w : K) (hζ : w ∈ primitiveRoots n K),
    (HSub.hSub (β := K[n√a][X]) (HPow.hPow (α := K[n√a][X]) X n)
        ((C : (a_1 : K[n√a]) → K[n√a][X]) (((algebraMap K K[n√a] : K →+* K[n√a]) : (a_1 : K) → K[n√a]) a) :
          K[n√a][X])).Splits
⊢ (HSub.hSub (β := K[n√a][X]) (HPow.hPow (α := K[n√a][X]) X n)
      ((C : (a_1 : K[n√a]) → K[n√a][X]) (((algebraMap K K[n√a] : K →+* K[n√a]) : (a_1 : K) → K[n√a]) a) :
        K[n√a][X])).Splits

Tactic:
have ⟨_, hζ⟩ := hζ
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ_1 : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this : Algebra K K[n√a] := inferInstance
w : K
hζ : w ∈ primitiveRoots n K
⊢ IsPrimitiveRoot w n

Tactic:
rw [mem_primitiveRoots (Nat.pos_of_ne_zero <| ne_zero_of_irreducible_X_pow_sub_C H)] at hζ

Premises used: ne_zero_of_irreducible_X_pow_sub_C, Nat.pos_of_ne_zero, mem_primitiveRoots
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ_1 : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this : Algebra K K[n√a] := inferInstance
w : K
hζ : IsPrimitiveRoot w n
⊢ (HSub.hSub (β := K[n√a][X]) (HPow.hPow (α := K[n√a][X]) X n)
      ((C : (a_1 : K[n√a]) → K[n√a][X]) (((algebraMap K K[n√a] : K →+* K[n√a]) : (a_1 : K) → K[n√a]) a) :
        K[n√a][X])).Splits

Tactic:
X_pow_sub_C_splits_of_isPrimitiveRoot (hζ.map_of_injective (algebraMap K _).injective)
      (root_X_pow_sub_C_pow n a)

Premises used: X_pow_sub_C_splits_of_isPrimitiveRoot, Algebra.algebraMap, RingHom.injective, root_X_pow_sub_C_pow, IsPrimitiveRoot.map_of_injective
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ_1 : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this : Algebra K K[n√a] := inferInstance
w : K
hζ : IsPrimitiveRoot w n
⊢ (HSub.hSub (β := K[n√a][X]) (HPow.hPow (α := K[n√a][X]) X n)
      ((C : (a_1 : K[n√a]) → K[n√a][X]) (((algebraMap K K[n√a] : K →+* K[n√a]) : (a_1 : K) → K[n√a]) a) :
        K[n√a][X])).Splits

Tactic:
exact X_pow_sub_C_splits_of_isPrimitiveRoot (hζ.map_of_injective (algebraMap K _).injective)
      (root_X_pow_sub_C_pow n a)

Premises used: X_pow_sub_C_splits_of_isPrimitiveRoot, Algebra.algebraMap, RingHom.injective, root_X_pow_sub_C_pow, IsPrimitiveRoot.map_of_injective
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this : Algebra K K[n√a] := inferInstance
adjoin_rootSet' :
  LE.le (α := Subalgebra K K[n√a])
    K [root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))]
    (Algebra.adjoin K
      ((HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])).rootSet K[n√a]))
⊢ Eq (α := Subalgebra K K[n√a])
    (Algebra.adjoin K
      ((HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])).rootSet K[n√a]))
    ⊤

Tactic:
rw [eq_top_iff, ← AdjoinRoot.adjoinRoot_eq_top]

Premises used: eq_top_iff, AdjoinRoot.adjoinRoot_eq_top
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this : Algebra K K[n√a] := inferInstance
adjoin_rootSet' :
  Subset (α := Set K[n√a])
    {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])).rootSet K[n√a])
⊢ LE.le (α := Subalgebra K K[n√a])
    K [root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))]
    (Algebra.adjoin K
      ((HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])).rootSet K[n√a]))

Tactic:
apply Algebra.adjoin_mono

Premises used: Algebra.adjoin_mono
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this : Algebra K K[n√a] := inferInstance
⊢ n ≠ 0

Tactic:
have := ne_zero_of_irreducible_X_pow_sub_C H