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
σ : 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_2 : IsDomain.{u} K[n√a] := ⋯
this : DecidableEq K := Classical.decEq K
h : ¬a = 0
isFalse : ¬Eq (α := K[n√a]) ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) (0 : K[n√a])
isFalse₁ isFalse₂ isFalse₃ isFalse₄ : ¬a = 0
⊢ Ne (α := K[n√a]) ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) (0 : K[n√a])

Tactic:
rwa [Ne, map_eq_zero_iff _ (algebraMap K _).injective]

Premises used: Algebra.algebraMap, Ne, RingHom.injective, map_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
η : ↥(rootsOfUnity n K)
⊢ 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
η : ↥(rootsOfUnity n K)
this : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
⊢ IsDomain.{u} K[n√a]

Tactic:
have : IsDomain K[n√a] := inferInstance
-- 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)
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this_2 : IsDomain.{u} K[n√a]
this : Algebra K K[n√a] := inferInstance
a₁ :
  Eq (α := ↥(rootsOfUnity n K[n√a]))
    ((rootsOfUnityEquivOfPrimitiveRoots (F := K →+* K[n√a]) (f := algebraMap K K[n√a]) ⋯ hζ :
          (a_1 : ↥(rootsOfUnity n K)) → ↥(rootsOfUnity n K[n√a]))
        (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H
          (OneHom.toFun (↑(autAdjoinRootXPowSubC n a) : OneHom ↥(rootsOfUnity n K) Gal(K[n√a]/K)) η)) :
      ↥(rootsOfUnity n K[n√a]))
    ((rootsOfUnityEquivOfPrimitiveRoots (F := K →+* K[n√a]) (f := algebraMap K K[n√a]) ⋯ hζ :
          (a_1 : ↥(rootsOfUnity n K)) → ↥(rootsOfUnity n K[n√a]))
        η :
      ↥(rootsOfUnity n K[n√a]))
⊢ AdjoinRootXPowSubCEquivToRootsOfUnity hζ H
      (OneHom.toFun (↑(autAdjoinRootXPowSubC n a) : OneHom ↥(rootsOfUnity n K) Gal(K[n√a]/K)) η) =
    η

Tactic:
apply (rootsOfUnityEquivOfPrimitiveRoots (algebraMap K K[n√a]).injective hζ).injective

Premises used: Polynomial.C, AdjoinRoot, Algebra.algebraMap, HSub.hSub, RingHom.injective, HPow.hPow, rootsOfUnityEquivOfPrimitiveRoots, Polynomial.X, DFunLike.coe, MulEquiv.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]))
inst_1 : NeZero n
η : ↥(rootsOfUnity n K)
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this_2 : IsDomain.{u} K[n√a]
this : Algebra K K[n√a] := inferInstance
a₁ :
  Eq.{u + 1} (α := K[n√a])
    (↑(↑((rootsOfUnityEquivOfPrimitiveRoots (F := K →+* K[n√a]) (f := algebraMap K K[n√a]) ⋯ hζ :
                (a_1 : ↥(rootsOfUnity n K)) → ↥(rootsOfUnity n K[n√a]))
              (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H
                (OneHom.toFun (↑(autAdjoinRootXPowSubC n a) : OneHom ↥(rootsOfUnity n K) Gal(K[n√a]/K)) η))) :
          K[n√a]ˣ) :
      K[n√a])
    (↑(↑((rootsOfUnityEquivOfPrimitiveRoots (F := K →+* K[n√a]) (f := algebraMap K K[n√a]) ⋯ hζ :
                (a_1 : ↥(rootsOfUnity n K)) → ↥(rootsOfUnity n K[n√a]))
              η) :
          K[n√a]ˣ) :
      K[n√a])
⊢ Eq (α := ↥(rootsOfUnity n K[n√a]))
    ((rootsOfUnityEquivOfPrimitiveRoots (F := K →+* K[n√a]) (f := algebraMap K K[n√a]) ⋯ hζ :
          (a_1 : ↥(rootsOfUnity n K)) → ↥(rootsOfUnity n K[n√a]))
        (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H
          (OneHom.toFun (↑(autAdjoinRootXPowSubC n a) : OneHom ↥(rootsOfUnity n K) Gal(K[n√a]/K)) η)) :
      ↥(rootsOfUnity n K[n√a]))
    ((rootsOfUnityEquivOfPrimitiveRoots (F := K →+* K[n√a]) (f := algebraMap K K[n√a]) ⋯ hζ :
          (a_1 : ↥(rootsOfUnity n K)) → ↥(rootsOfUnity n K[n√a]))
        η :
      ↥(rootsOfUnity n K[n√a]))

Tactic:
ext
-- 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)
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this_2 : IsDomain.{u} K[n√a]
this : Algebra K K[n√a] := inferInstance
a₁ :
  (if a = 0 then 1
    else
      HMul.hMul (α := K[n√a])
          ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) :
                (a_1 : K) → K[n√a])
              (↑(↑η : Kˣ) : K) :
            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]))) =
    (of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) : (a_1 : K) → K[n√a])
      (↑(↑η : Kˣ) : K)
⊢ Eq.{u + 1} (α := K[n√a])
    (↑(↑((rootsOfUnityEquivOfPrimitiveRoots (F := K →+* K[n√a]) (f := algebraMap K K[n√a]) ⋯ hζ :
                (a_1 : ↥(rootsOfUnity n K)) → ↥(rootsOfUnity n K[n√a]))
              (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H
                (OneHom.toFun (↑(autAdjoinRootXPowSubC n a) : OneHom ↥(rootsOfUnity n K) Gal(K[n√a]/K)) η))) :
          K[n√a]ˣ) :
      K[n√a])
    (↑(↑((rootsOfUnityEquivOfPrimitiveRoots (F := K →+* K[n√a]) (f := algebraMap K K[n√a]) ⋯ hζ :
                (a_1 : ↥(rootsOfUnity n K)) → ↥(rootsOfUnity n K[n√a]))
              η) :
          K[n√a]ˣ) :
      K[n√a])

Tactic:
simp only [AdjoinRoot.algebraMap_eq, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe,
      autAdjoinRootXPowSubC_root, Algebra.smul_def, MulEquiv.apply_symm_apply,
      rootsOfUnity.val_mkOfPowEq_coe, val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe,
      AdjoinRootXPowSubCEquivToRootsOfUnity]

Premises used: rootsOfUnity.val_mkOfPowEq_coe, AdjoinRoot.algebraMap_eq, MonoidHom.toOneHom_coe, AdjoinRootXPowSubCEquivToRootsOfUnity, Algebra.smul_def, val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe, autAdjoinRootXPowSubC_root, OneHom.toFun_eq_coe, MulEquiv.apply_symm_apply
-- 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)
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this_2 : IsDomain.{u} K[n√a]
this : Algebra K K[n√a] := inferInstance
pos :
  ∀ (h : a = 0),
    Eq (α := K[n√a]) (1 : K[n√a])
      ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) : (a_1 : K) → K[n√a])
          (↑(↑η : Kˣ) : K) :
        K[n√a])
neg :
  ∀ (h : ¬a = 0),
    HMul.hMul (α := K[n√a])
          ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) :
                (a_1 : K) → K[n√a])
              (↑(↑η : Kˣ) : K) :
            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])) =
      (of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) : (a_1 : K) → K[n√a])
        (↑(↑η : Kˣ) : K)
⊢ (if a = 0 then 1
    else
      HMul.hMul (α := K[n√a])
          ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) :
                (a_1 : K) → K[n√a])
              (↑(↑η : Kˣ) : K) :
            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]))) =
    (of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) : (a_1 : K) → K[n√a])
      (↑(↑η : Kˣ) : K)

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
η : ↥(rootsOfUnity n K)
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this_2 : IsDomain.{u} K[n√a]
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] (η : ↥(rootsOfUnity 1 K))
    (this :
      Fact
        (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X]))))
    (this_3 : IsDomain.{u} K[1√a]),
    Eq (α := 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])
          (↑(↑η : Kˣ) : K) :
        K[1√a])
⊢ Eq (α := K[n√a]) (1 : K[n√a])
    ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) : (a_1 : K) → K[n√a])
        (↑(↑η : Kˣ) : K) :
      K[n√a])

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
η : ↥(rootsOfUnity 1 K)
this_1 :
  Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])))
this_2 : IsDomain.{u} K[1√a]
this : Algebra K K[1√a] := inferInstance
⊢ (↑η : Kˣ) = 1

Tactic:
have : (η : Kˣ) = 1 := (pow_one _).symm.trans η.prop
-- 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
η : ↥(rootsOfUnity 1 K)
this_1 :
  Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) (β := ℕ) X 1) ((C : (a : K) → K [X]) a : K [X])))
this_2 : IsDomain.{u} K[1√a]
this_3 : Algebra K K[1√a] := inferInstance
this : (↑η : Kˣ) = 1
⊢ Eq (α := 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])
        (↑(↑η : Kˣ) : K) :
      K[1√a])

Tactic:
simp only [this, Units.val_one, map_one]

Premises used: map_one, Units.val_one
-- 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)
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this_2 : IsDomain.{u} K[n√a]
this : Algebra K K[n√a] := inferInstance
h : ¬a = 0
⊢ HMul.hMul (α := K[n√a])
        ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) :
              (a_1 : K) → K[n√a])
            (↑(↑η : Kˣ) : K) :
          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])) =
    (of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) : (a_1 : K) → K[n√a])
      (↑(↑η : Kˣ) : K)

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

Premises used: root_X_pow_sub_C_ne_zero', mul_div_cancel_right₀, 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)
this_1 : Fact (Irreducible (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
this_2 : IsDomain.{u} K[n√a]
this : Algebra K K[n√a] := inferInstance
h : ¬a = 0
⊢ HMul.hMul (α := K[n√a])
        ((of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) :
              (a_1 : K) → K[n√a])
            (↑(↑η : Kˣ) : K) :
          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])) =
    (of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) : (a_1 : K) → K[n√a])
      (↑(↑η : Kˣ) : K)

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

Premises used: root_X_pow_sub_C_ne_zero', mul_div_cancel_right₀, 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 : 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
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
a₁ :
  (↑(OneHom.toFun (↑(autAdjoinRootXPowSubC n a) : OneHom ↥(rootsOfUnity n K) Gal(K[n√a]/K))
          (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H e)) :
      K[n√a] →ₐ[K] K[n√a]) =
    (↑e : K[n√a] →ₐ[K] K[n√a])
⊢ OneHom.toFun (↑(autAdjoinRootXPowSubC n a) : OneHom ↥(rootsOfUnity n K) Gal(K[n√a]/K))
      (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H e) =
    e

Tactic:
apply AlgEquiv.coe_algHom_injective

Premises used: AlgEquiv.coe_algHom_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]))
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
a₁ :
  Eq (α := K[n√a])
    (((↑(OneHom.toFun (↑(autAdjoinRootXPowSubC n a) : OneHom ↥(rootsOfUnity n K) Gal(K[n√a]/K))
                (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H e)) :
            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[n√a])
    (((↑e : 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[n√a])
⊢ (↑(OneHom.toFun (↑(autAdjoinRootXPowSubC n a) : OneHom ↥(rootsOfUnity n K) Gal(K[n√a]/K))
          (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H e)) :
      K[n√a] →ₐ[K] K[n√a]) =
    (↑e : K[n√a] →ₐ[K] K[n√a])

Tactic:
apply AdjoinRoot.algHom_ext

Premises used: AdjoinRoot.algHom_ext
-- 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
a₁ :
  (of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) : (a_1 : K) → K[n√a])
        (↑(↑((MulEquiv.symm
                      (rootsOfUnityEquivOfPrimitiveRoots (F := K →+* K[n√a]) (f :=
                        of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) ⋯
                        hζ) :
                    (a : ↥(rootsOfUnity n K[n√a])) → ↥(rootsOfUnity n K))
                  (rootsOfUnity.mkOfPowEq
                    (if a = 0 then 1
                    else
                      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]))))
                    ⋯)) :
              Kˣ) :
          K) *
      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])))
⊢ Eq (α := K[n√a])
    (((↑(OneHom.toFun (↑(autAdjoinRootXPowSubC n a) : OneHom ↥(rootsOfUnity n K) Gal(K[n√a]/K))
                (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H e)) :
            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[n√a])
    (((↑e : 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[n√a])

Tactic:
simp only [AdjoinRootXPowSubCEquivToRootsOfUnity, AdjoinRoot.algebraMap_eq, OneHom.toFun_eq_coe,
      MonoidHom.toOneHom_coe, AlgEquiv.coe_algHom, autAdjoinRootXPowSubC_root, Algebra.smul_def]

Premises used: AdjoinRoot.algebraMap_eq, MonoidHom.toOneHom_coe, AdjoinRootXPowSubCEquivToRootsOfUnity, AlgEquiv.coe_algHom, Algebra.smul_def, autAdjoinRootXPowSubC_root, 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
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
a₁ :
  (if a = 0 then 1
      else
        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])))
⊢ (of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) : (a_1 : K) → K[n√a])
        (↑(↑((MulEquiv.symm
                      (rootsOfUnityEquivOfPrimitiveRoots (F := K →+* K[n√a]) (f :=
                        of (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) ⋯
                        hζ) :
                    (a : ↥(rootsOfUnity n K[n√a])) → ↥(rootsOfUnity n K))
                  (rootsOfUnity.mkOfPowEq
                    (if a = 0 then 1
                    else
                      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]))))
                    ⋯)) :
              Kˣ) :
          K) *
      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:
rw [rootsOfUnityEquivOfPrimitiveRoots_symm_apply, rootsOfUnity.val_mkOfPowEq_coe]

Premises used: rootsOfUnity.val_mkOfPowEq_coe, rootsOfUnityEquivOfPrimitiveRoots_symm_apply
-- 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
pos :
  ∀ (h : a = 0),
    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])))
neg :
  ∀ (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])))
⊢ (if a = 0 then 1
      else
        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:
split_ifs with h