awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K] (hn : Odd n) {a : K} (ha : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a),
    Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))
K : Type u
inst : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
E : Type u
inst_1 : Field E
inst_2 : Algebra K E
x : E
hx : minpoly K x = HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X])
this : IsIntegral K x
q : ℕ
hq : Nat.Prime q
hqn : q ∣ n
b : ↥K⟮x⟯
hb : b ^ q = AdjoinSimple.gen K x
prime_mul : HPow.hPow (α := K) (-1) (adjoin.powerBasis this).dim * coeff (minpoly K (adjoin.powerBasis this).gen) 0 = a
⊢ HPow.hPow (α := K) ((Algebra.norm K : (a : ↥K⟮x⟯) → K) b : K) q = a

Tactic:
rw [← map_pow, hb, ← adjoin.powerBasis_gen this,
      Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly]

Premises used: Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly, IntermediateField.adjoin.powerBasis_gen, map_pow
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hn : Odd n
a : K
ha : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a
zero :
  ∀ {K : Type u} [inst : Field K] (hn : Odd (α := ℕ) 0) {a : K}
    (ha : ∀ (p : ℕ), Nat.Prime p → p ∣ 0 → ∀ (b : K), b ^ p ≠ a),
    Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) (β := ℕ) X 0) ((C : (a : K) → K[X]) a : K[X]))
one :
  ∀ {K : Type u} [inst : Field K] (hn : Odd (α := ℕ) 1) {a : K}
    (ha : ∀ (p : ℕ), Nat.Prime p → p ∣ 1 → ∀ (b : K), b ^ p ≠ a),
    Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) (β := ℕ) X 1) ((C : (a : K) → K[X]) a : K[X]))
prime_mul :
  ∀ (p n : ℕ) (hp : Nat.Prime p)
    (IH :
      ∀ {K : Type u} [inst : Field K] (hn : Odd n) {a : K} (ha : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a),
        Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])))
    {K : Type u} [inst : Field K] (hn : Odd (p * n)) {a : K}
    (ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a),
    Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (p * n)) ((C : (a : K) → K[X]) a : K[X]))
⊢ Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))

Tactic:
induction n using induction_on_primes generalizing K a with
  | zero => simp [← Nat.not_even_iff_odd] at hn
  | one => simpa using irreducible_X_sub_C a
  | prime_mul p n hp IH =>
    rw [mul_comm]
    apply X_pow_mul_sub_C_irreducible
      (X_pow_sub_C_irreducible_of_prime hp (ha p hp (dvd_mul_right _ _)))
    intro E _ _ x hx
    have : IsIntegral K x := not_not.mp fun h ↦ by
      simpa only [degree_zero, degree_X_pow_sub_C hp.pos,
        WithBot.natCast_ne_bot] using congr_arg degree (hx.symm.trans (dif_neg h))
    apply IH (Nat.odd_mul.mp hn).2
    intro q hq hqn b hb
    apply ha q hq (dvd_mul_of_dvd_right hqn p) (Algebra.norm _ b)
    rw [← map_pow, hb, ← adjoin.powerBasis_gen this,
      Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly]
    simp [minpoly_gen, hx, hp.ne_zero.symm, (Nat.odd_mul.mp hn).1.neg_pow]

Premises used: Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly, IntermediateField.minpoly_gen, Nat.not_even_iff_odd, map_pow, induction_on_primes, mul_comm, Polynomial.irreducible_X_sub_C
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hn : Odd n
a : K
⊢ Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) ↔
    ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a

Tactic:
⟨fun e _ hp hpn ↦ pow_ne_of_irreducible_X_pow_sub_C e hpn hp.ne_one,
    X_pow_sub_C_irreducible_of_odd hn⟩

Premises used: X_pow_sub_C_irreducible_of_odd, Nat.Prime.ne_one, Iff.intro, pow_ne_of_irreducible_X_pow_sub_C
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
hn : Odd n
a : K
⊢ Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])) ↔
    ∀ (d : ℕ), d ∣ n → d ≠ 1 → ∀ (b : K), b ^ d ≠ a

Tactic:
⟨fun e _ ↦ pow_ne_of_irreducible_X_pow_sub_C e,
    fun H ↦ X_pow_sub_C_irreducible_of_odd hn fun p hp hpn ↦ (H p hpn hp.ne_one)⟩

Premises used: X_pow_sub_C_irreducible_of_odd, Nat.Prime.ne_one, Iff.intro, pow_ne_of_irreducible_X_pow_sub_C
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
p : ℕ
hp : Nat.Prime p
hp' : p ≠ 2
n : ℕ
a : K
ha : ∀ (b : K), b ^ p ≠ a
apply : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p ^ n → ∀ (b : K), b ^ p_1 ≠ a
⊢ Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (p ^ n)) ((C : (a : K) → K[X]) a : K[X]))

Tactic:
apply X_pow_sub_C_irreducible_of_odd (hp.odd_of_ne_two hp').pow

Premises used: X_pow_sub_C_irreducible_of_odd, Nat.Prime.odd_of_ne_two, Odd.pow
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
p : ℕ
hp : Nat.Prime p
hp' : p ≠ 2
n : ℕ
a : K
ha : ∀ (b : K), b ^ p ≠ a
q : ℕ
hq : Nat.Prime q
hq' : q ∣ p ^ n
⊢ ∀ (b : K), b ^ q ≠ a

Tactic:
simpa [(Nat.prime_dvd_prime_iff_eq hq hp).mp (hq.dvd_of_dvd_pow hq')] using ha

Premises used: Nat.Prime.dvd_of_dvd_pow, Nat.prime_dvd_prime_iff_eq, Iff.mp
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
p : ℕ
hp : Nat.Prime p
hp' : p ≠ 2
n : ℕ
hn : n ≠ 0
a : K
⊢ Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (p ^ n)) ((C : (a : K) → K[X]) a : K[X])) ↔
    ∀ (b : K), b ^ p ≠ a

Tactic:
⟨(pow_ne_of_irreducible_X_pow_sub_C · (dvd_pow dvd_rfl hn) hp.ne_one),
    X_pow_sub_C_irreducible_of_prime_pow hp hp' n⟩

Premises used: dvd_pow, Nat.Prime.ne_one, Iff.intro, X_pow_sub_C_irreducible_of_prime_pow, dvd_rfl, pow_ne_of_irreducible_X_pow_sub_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
⊢ 0 < n

Tactic:
have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C 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
hn : 0 < n
pos : ∀ (hn' : n = 1), (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])).Separable
neg :
  ∀ (hn' : ¬n = 1), (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])).Separable
⊢ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])).Separable

Tactic:
by_cases hn' : n = 1
-- 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
hn : 0 < n
hn' : n = 1
pos : (HSub.hSub (α := K [X]) (β := K [X]) X ((C : (a : K) → K [X]) a : K [X])).Separable
⊢ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])).Separable

Tactic:
rw [hn', pow_one]

Premises used: pow_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]))
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
hn : 0 < n
hn' : n = 1
⊢ (HSub.hSub (α := K [X]) (β := K [X]) X ((C : (a : K) → K [X]) a : K [X])).Separable

Tactic:
separable_X_sub_C

Premises used: Polynomial.separable_X_sub_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
hn : 0 < n
hn' : n = 1
⊢ (HSub.hSub (α := K [X]) (β := K [X]) X ((C : (a : K) → K [X]) a : K [X])).Separable

Tactic:
exact separable_X_sub_C

Premises used: Polynomial.separable_X_sub_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
hn : 0 < n
hn' : ¬n = 1
neg :
  ∀ (ζ : K) (hζ : ζ ∈ primitiveRoots n K),
    (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])).Separable
⊢ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])).Separable

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
hn : 0 < n
hn' : ¬n = 1
ζ : K
hζ : ζ ∈ primitiveRoots n K
⊢ IsPrimitiveRoot ζ 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
hn : 0 < n
hn' : ¬n = 1
ζ : K
hζ : IsPrimitiveRoot ζ n
neg :
  ∀ x ∈ Finset.range n,
    ∀ y ∈ Finset.range n,
      HPow.hPow (α := K[n√a]) (((algebraMap K K[n√a] : K →+* K[n√a]) : (a_3 : K) → K[n√a]) ζ : K[n√a]) x *
            root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) =
          HPow.hPow (α := K[n√a]) (((algebraMap K K[n√a] : K →+* K[n√a]) : (a_3 : K) → K[n√a]) ζ : K[n√a]) y *
            root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) →
        x = y
⊢ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])).Separable

Tactic:
rw [← separable_map (algebraMap K K[n√a]), Polynomial.map_sub, Polynomial.map_pow, map_C, map_X,
    AdjoinRoot.algebraMap_eq,
    X_pow_sub_C_eq_prod (hζ.map_of_injective (algebraMap K _).injective) hn
    (root_X_pow_sub_C_pow n a), separable_prod_X_sub_C_iff']

Premises used: Polynomial.C, X_pow_sub_C_eq_prod, AdjoinRoot, Algebra.algebraMap, HSub.hSub, AdjoinRoot.algebraMap_eq, Polynomial.map_pow, Polynomial.map_X, Polynomial.separable_prod_X_sub_C_iff', RingHom.injective, root_X_pow_sub_C_pow, HPow.hPow, Polynomial.map_sub, IsPrimitiveRoot.map_of_injective, Polynomial.map_C, Polynomial.X, DFunLike.coe, Polynomial.separable_map
-- 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
hn : 0 < n
hn' : ¬n = 1
ζ : K
hζ : IsPrimitiveRoot ζ n
⊢ ∀ x ∈ Finset.range n,
    ∀ y ∈ Finset.range n,
      HPow.hPow (α := K[n√a]) (((algebraMap K K[n√a] : K →+* K[n√a]) : (a_3 : K) → K[n√a]) ζ : K[n√a]) x *
            root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) =
          HPow.hPow (α := K[n√a]) (((algebraMap K K[n√a] : K →+* K[n√a]) : (a_3 : K) → K[n√a]) ζ : K[n√a]) y *
            root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) →
        x = y

Tactic:
(hζ.map_of_injective (algebraMap K K[n√a]).injective).injOn_pow_mul
    (root_X_pow_sub_C_ne_zero (lt_of_le_of_ne (show 1 ≤ n from hn) (Ne.symm hn')) _)

Premises used: Ne.symm, IsPrimitiveRoot.injOn_pow_mul, root_X_pow_sub_C_ne_zero, Set.InjOn, lt_of_le_of_ne
-- 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
hn : 0 < n
hn' : ¬n = 1
ζ : K
hζ : IsPrimitiveRoot ζ n
⊢ ∀ x ∈ Finset.range n,
    ∀ y ∈ Finset.range n,
      HPow.hPow (α := K[n√a]) (((algebraMap K K[n√a] : K →+* K[n√a]) : (a_3 : K) → K[n√a]) ζ : K[n√a]) x *
            root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) =
          HPow.hPow (α := K[n√a]) (((algebraMap K K[n√a] : K →+* K[n√a]) : (a_3 : K) → K[n√a]) ζ : K[n√a]) y *
            root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) →
        x = y

Tactic:
exact (hζ.map_of_injective (algebraMap K K[n√a]).injective).injOn_pow_mul
    (root_X_pow_sub_C_ne_zero (lt_of_le_of_ne (show 1 ≤ n from hn) (Ne.symm hn')) _)

Premises used: IsPrimitiveRoot.injOn_pow_mul
-- 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]))
η : ↥(rootsOfUnity n K)
⊢ (↑(↑η : Kˣ) : K) ^ n = 1

Tactic:
have := (mem_rootsOfUnity' _ _).mp η.prop
-- 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]))
⊢ Eq (α := K[n√a])
    ((liftAlgHom (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
            (Algebra.ofId K K[n√a])
            (HSMul.hSMul (α := K) (↑(↑1 : 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]))) :
      K[n√a])
    ((1 : (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
-- 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]))
ε η : ↥(rootsOfUnity n K)
⊢ Eq (α := K[n√a])
    ((liftAlgHom (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
            (Algebra.ofId K K[n√a])
            ((↑(↑(ε * η) : 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]))) :
      K[n√a])
    ((liftAlgHom (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
              (Algebra.ofId K K[n√a])
              ((↑(↑ε : Kˣ) : K) •
                root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
              ⋯ *
            liftAlgHom (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
              (Algebra.ofId K K[n√a])
              ((↑(↑η : 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]))) :
      K[n√a])

Tactic:
simp [mul_smul, smul_comm ((ε : Kˣ) : K)]

Premises used: Units.val, SMulCommClass.smul_comm, Subtype.val, SemigroupAction.mul_smul
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
a : K
η : ↥(rootsOfUnity n K)
⊢ (liftAlgHom (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
          (Algebra.ofId K K[n√a])
          ((↑(↑η : 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]))) =
    (↑(↑η : Kˣ) : K) • root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))

Tactic:
liftAlgHom_root _ (Algebra.ofId _ _) ..

Premises used: Algebra.ofId, AdjoinRoot.liftAlgHom_root
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
a : K
η : ↥(rootsOfUnity n K)
⊢ (liftAlgHom (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))
          (Algebra.ofId K K[n√a])
          ((↑(↑η : 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]))) =
    (↑(↑η : Kˣ) : K) • root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))

Tactic:
exact liftAlgHom_root _ (Algebra.ofId _ _) ..

Premises used: Algebra.ofId, AdjoinRoot.liftAlgHom_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
σ : 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
isTrue : a = 0 → HPow.hPow (α := K[n√a]) 1 n = 1
isFalse :
  ¬a = 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]))) ^
        n =
      1
⊢ (if a = 0 then 1
      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])))) ^
      n =
    1

Tactic:
split
-- 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
⊢ HPow.hPow (α := K[n√a]) 1 n = 1

Tactic:
one_pow _

Premises used: one_pow
-- 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
⊢ HPow.hPow (α := K[n√a]) 1 n = 1

Tactic:
exact one_pow _

Premises used: one_pow
-- 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 :
  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])) ^ n) :
        K[n√a])
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) ^ n) =
    1
⊢ 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]))) ^
      n =
    1

Tactic:
rw [div_pow, ← map_pow]

Premises used: map_pow, div_pow
-- 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 :
  HDiv.hDiv (α := K[n√a]) (β := K[n√a]) ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a])
      ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) =
    1
⊢ 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])) ^ n) :
        K[n√a])
      (root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) ^ n) =
    1

Tactic:
simp only [root_X_pow_sub_C_pow, ← AdjoinRoot.algebraMap_eq, AlgEquiv.commutes]

Premises used: AdjoinRoot.algebraMap_eq, AlgEquiv.commutes, root_X_pow_sub_C_pow
-- 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 : Ne (α := K[n√a]) ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) (0 : K[n√a])
⊢ HDiv.hDiv (α := K[n√a]) (β := K[n√a]) ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a])
      ((algebraMap K K[n√a] : (a_1 : K) → K[n√a]) a : K[n√a]) =
    1

Tactic:
rw [div_self]

Premises used: div_self