awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
hn : 0 < n
e : α ^ n = a
K : Type u_1 := FractionRing R
i : R →+* K := algebraMap R K
h : Function.Injective (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
⊢ HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X]) =
    ∏ i ∈ Finset.range n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (ζ ^ i * α) : R[X])
have apply_fun : Polynomial.map i (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])) =
  Polynomial.map i (∏ i ∈ Finset.range n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (ζ ^ i * α) : R[X]))
Tactic: apply_fun Polynomial.map i using map_injective i h
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
Goal:
K : Type u
inst : Field K
n : ℕ
a : K
hm : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) (β := ℕ) X 0) ((C : (a : K) → K[X]) a : K[X]))
hn :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) (β := ℕ) X 0) ((C : (a : K) → K[X]) a : K[X]) →
      Irreducible
        (HSub.hSub (β := (↥K⟮x⟯)[X]) (HPow.hPow (α := (↥K⟮x⟯)[X]) X n)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
⊢ False
have hm₁ : Irreducible (M := K[X]) ((C : (a : K) → K[X]) (1 - a) : K[X])
Tactic: rw [pow_zero, ← C.map_one, ← map_sub] at hm
Cleared hypotheses: hm, hn
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
Goal:
K : Type u
inst : Field K
n m : ℕ
a : K
hm : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X m) ((C : (a : K) → K[X]) a : K[X]))
hn :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X m) ((C : (a : K) → K[X]) a : K[X]) →
      Irreducible
        (HSub.hSub (β := (↥K⟮x⟯)[X]) (HPow.hPow (α := (↥K⟮x⟯)[X]) X n)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
⊢ Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (n * m)) ((C : (a : K) → K[X]) a : K[X]))
have hm' : m ≠ 0
Tactic: have hm' : m ≠ 0 := by
    rintro rfl
    rw [pow_zero, ← C.map_one, ← map_sub] at hm
    exact not_irreducible_C _ hm
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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
⊢ Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (p * n)) ((C : (a : K) → K[X]) a : K[X]))
have prime_mul : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (n * p)) ((C : (a : K) → K[X]) a : K[X]))
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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
⊢ Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (n * p)) ((C : (a : K) → K[X]) a : K[X]))
have prime_mul : ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
  minpoly K x = HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]) →
    Irreducible
      (HSub.hSub (β := (↥K⟮x⟯)[X]) (HPow.hPow (α := (↥K⟮x⟯)[X]) X n)
        ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
Tactic: apply X_pow_mul_sub_C_irreducible
      (X_pow_sub_C_irreducible_of_prime hp (ha p hp (dvd_mul_right _ _)))
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
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])
⊢ Irreducible
    (HSub.hSub (β := (↥K⟮x⟯)[X]) (HPow.hPow (α := (↥K⟮x⟯)[X]) X n)
      ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
have this : IsIntegral K x
Tactic: 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))
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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
⊢ Irreducible
    (HSub.hSub (β := (↥K⟮x⟯)[X]) (HPow.hPow (α := (↥K⟮x⟯)[X]) X n)
      ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
have prime_mul : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : ↥K⟮x⟯), b ^ p ≠ AdjoinSimple.gen K x
Tactic: apply IH (Nat.odd_mul.mp hn).2
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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
⊢ False
have prime_mul : HPow.hPow (α := K) ((Algebra.norm K : (a : ↥K⟮x⟯) → K) b : K) q = a
Tactic: apply ha q hq (dvd_mul_of_dvd_right hqn p) (Algebra.norm _ b)
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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
⊢ HPow.hPow (α := K) ((Algebra.norm K : (a : ↥K⟮x⟯) → K) b : K) q = a
have prime_mul : HPow.hPow (α := K) (-1) (adjoin.powerBasis this).dim * coeff (minpoly K (adjoin.powerBasis this).gen) 0 = a
Tactic: rw [← map_pow, hb, ← adjoin.powerBasis_gen this,
      Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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
⊢ Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))
have 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]))
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]
Cleared hypotheses: K, inst, n, hn, a, ha
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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]))
⊢ Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))
have 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]))
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]
Cleared hypotheses: K, inst, n, hn, a, ha
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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]))
⊢ Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))
have 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]))
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]
Cleared hypotheses: K, inst, n, hn, a, ha
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
p : ℕ
hp : Nat.Prime p
hp' : p ≠ 2
n : ℕ
a : K
ha : ∀ (b : K), b ^ p ≠ a
⊢ Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (p ^ n)) ((C : (a : K) → K[X]) a : K[X]))
have apply : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p ^ n → ∀ (b : K), b ^ p_1 ≠ a
Tactic: apply X_pow_sub_C_irreducible_of_odd (hp.odd_of_ne_two hp').pow
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
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
⊢ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])).Separable
have hn : 0 < n
Tactic: have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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
⊢ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])).Separable
have pos : ∀ (hn' : n = 1), (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
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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
⊢ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])).Separable
have neg : ∀ (hn' : ¬n = 1), (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
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])).Separable
have pos : (HSub.hSub (α := K [X]) (β := K [X]) X ((C : (a : K) → K [X]) a : K [X])).Separable
Tactic: rw [hn', pow_one]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])).Separable
have 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
Tactic: have ⟨ζ, hζ⟩ := hζ
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
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
⊢ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])).Separable
have hζ₁ : IsPrimitiveRoot ζ n
Tactic: rw [mem_primitiveRoots (Nat.pos_of_ne_zero <| ne_zero_of_irreducible_X_pow_sub_C H)] at hζ
Cleared hypotheses: hζ
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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
⊢ (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])).Separable
have 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
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']
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
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)
⊢ eval₂ (↑(Algebra.ofId K K[n√a]) : 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])))
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])) =
    0
have this : (↑(↑η : Kˣ) : K) ^ n = 1
Tactic: have := (mem_rootsOfUnity' _ _).mp η.prop
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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)
this : (↑(↑η : Kˣ) : K) ^ n = 1
⊢ Eq (α := K[n√a])
    ((aeval
          ((↑(↑η : Kˣ) : K) •
            root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
        (a_1 : K [X]) → K[n√a])
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
    0
have rw : HSub.hSub (α := K[n√a]) (β := K[n√a])
    ((aeval
            ((↑(↑η : Kˣ) : K) •
              root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
          (a_1 : K [X]) → K[n√a])
        (HPow.hPow (α := K [X]) X n) :
      K[n√a])
    ((aeval
            ((↑(↑η : Kˣ) : K) •
              root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
          (a_1 : K [X]) → K[n√a])
        ((C : (a : K) → K [X]) a) :
      K[n√a]) =
  0
Tactic: rw [map_sub, map_pow, aeval_C, aeval_X, Algebra.smul_def, mul_pow, root_X_pow_sub_C_pow,
      AdjoinRoot.algebraMap_eq, ← map_pow, this, map_one, one_mul, sub_self]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
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)
this : (↑(↑η : Kˣ) : K) ^ n = 1
rw :
  HSub.hSub (α := K[n√a]) (β := K[n√a])
      ((aeval
              ((↑(↑η : Kˣ) : K) •
                root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
            (a_1 : K [X]) → K[n√a])
          (HPow.hPow (α := K [X]) X n) :
        K[n√a])
      ((aeval
              ((↑(↑η : Kˣ) : K) •
                root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
            (a_1 : K [X]) → K[n√a])
          ((C : (a : K) → K [X]) a) :
        K[n√a]) =
    0
⊢ Eq (α := K[n√a])
    ((aeval
          ((↑(↑η : Kˣ) : K) •
            root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
        (a_1 : K [X]) → K[n√a])
      (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X])))
    0
have rw₁ : HSub.hSub (β := K[n√a])
    (HPow.hPow (α := K[n√a])
      ((aeval
            ((↑(↑η : Kˣ) : K) •
              root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
          (a_1 : K [X]) → K[n√a])
        X)
      n)
    ((aeval
            ((↑(↑η : Kˣ) : K) •
              root (HSub.hSub (β := K [X]) (HPow.hPow (α := K [X]) X n) ((C : (a : K) → K [X]) a : K [X]))) :
          (a_1 : K [X]) → K[n√a])
        ((C : (a : K) → K [X]) a) :
      K[n√a]) =
  0
Tactic: rw [map_sub, map_pow, aeval_C, aeval_X, Algebra.smul_def, mul_pow, root_X_pow_sub_C_pow,
      AdjoinRoot.algebraMap_eq, ← map_pow, this, map_one, one_mul, sub_self]