awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this_1 : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
z : E
hz : IsRoot (cyclotomic n E) z
this_2 : FiniteDimensional K L := ⋯
this_3 : IsGalois K L := ⋯
Hprod : ∏ σ : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((σ : (a : L) → E) ζ : E) = eval 1 (cyclotomic' n E)
this : NeZero.{v} (R := E) (↑n : E)
a : eval 1 (cyclotomic' n E) = ((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K)
a₁ :
  Eq (α := E) (eval 1 (∏ μ ∈ primitiveRoots n E, HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) μ : E[X])))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
⊢ Eq.{v + 1} (α := E) (∏ x : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((x : (a : L) → E) ζ : E))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
have a₂ : eval 1 (cyclotomic n E) = ((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K)
Tactic: rw [Hprod, cyclotomic', ← cyclotomic_eq_prod_X_sub_primitiveRoots (isRoot_cyclotomic_iff.1 hz),
    ← map_cyclotomic_int, _root_.map_intCast, ← Int.cast_one, eval_intCast_map, eq_intCast,
    Int.cast_id]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this_1 : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
z : E
hz : IsRoot (cyclotomic n E) z
this_2 : FiniteDimensional K L := ⋯
this_3 : IsGalois K L := ⋯
Hprod : ∏ σ : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((σ : (a : L) → E) ζ : E) = eval 1 (cyclotomic' n E)
this : NeZero.{v} (R := E) (↑n : E)
a : eval 1 (cyclotomic' n E) = ((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K)
a₁ :
  Eq (α := E) (eval 1 (∏ μ ∈ primitiveRoots n E, HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) μ : E[X])))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
a₂ : eval 1 (cyclotomic n E) = ((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K)
⊢ Eq.{v + 1} (α := E) (∏ x : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((x : (a : L) → E) ζ : E))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
have a₃ : eval 1 (Polynomial.map (Int.castRingHom E) (cyclotomic n ℤ)) =
  ((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K)
Tactic: rw [Hprod, cyclotomic', ← cyclotomic_eq_prod_X_sub_primitiveRoots (isRoot_cyclotomic_iff.1 hz),
    ← map_cyclotomic_int, _root_.map_intCast, ← Int.cast_one, eval_intCast_map, eq_intCast,
    Int.cast_id]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this_1 : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
z : E
hz : IsRoot (cyclotomic n E) z
this_2 : FiniteDimensional K L := ⋯
this_3 : IsGalois K L := ⋯
Hprod : ∏ σ : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((σ : (a : L) → E) ζ : E) = eval 1 (cyclotomic' n E)
this : NeZero.{v} (R := E) (↑n : E)
a : eval 1 (cyclotomic' n E) = ((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K)
a₁ :
  Eq (α := E) (eval 1 (∏ μ ∈ primitiveRoots n E, HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) μ : E[X])))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
a₂ : eval 1 (cyclotomic n E) = ((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K)
a₃ :
  eval 1 (Polynomial.map (Int.castRingHom E) (cyclotomic n ℤ)) =
    ((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K)
⊢ Eq.{v + 1} (α := E) (∏ x : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((x : (a : L) → E) ζ : E))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
have a₄ : eval 1 (Polynomial.map (Int.castRingHom E) (cyclotomic n ℤ)) = (↑(eval 1 (cyclotomic n ℤ)) : E)
Tactic: rw [Hprod, cyclotomic', ← cyclotomic_eq_prod_X_sub_primitiveRoots (isRoot_cyclotomic_iff.1 hz),
    ← map_cyclotomic_int, _root_.map_intCast, ← Int.cast_one, eval_intCast_map, eq_intCast,
    Int.cast_id]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this_1 : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
z : E
hz : IsRoot (cyclotomic n E) z
this_2 : FiniteDimensional K L := ⋯
this_3 : IsGalois K L := ⋯
Hprod : ∏ σ : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((σ : (a : L) → E) ζ : E) = eval 1 (cyclotomic' n E)
this : NeZero.{v} (R := E) (↑n : E)
a : eval 1 (cyclotomic' n E) = ((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K)
a₁ :
  Eq (α := E) (eval 1 (∏ μ ∈ primitiveRoots n E, HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) μ : E[X])))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
a₂ : eval 1 (cyclotomic n E) = ((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K)
a₃ :
  eval 1 (Polynomial.map (Int.castRingHom E) (cyclotomic n ℤ)) =
    ((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K)
a₄ : eval 1 (Polynomial.map (Int.castRingHom E) (cyclotomic n ℤ)) = (↑(eval 1 (cyclotomic n ℤ)) : E)
⊢ Eq.{v + 1} (α := E) (∏ x : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((x : (a : L) → E) ζ : E))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
have a₅ : eval (↑1 : E) (Polynomial.map (Int.castRingHom E) (cyclotomic n ℤ)) = (↑(eval 1 (cyclotomic n ℤ)) : E)
Tactic: rw [Hprod, cyclotomic', ← cyclotomic_eq_prod_X_sub_primitiveRoots (isRoot_cyclotomic_iff.1 hz),
    ← map_cyclotomic_int, _root_.map_intCast, ← Int.cast_one, eval_intCast_map, eq_intCast,
    Int.cast_id]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this_1 : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
z : E
hz : IsRoot (cyclotomic n E) z
this_2 : FiniteDimensional K L := ⋯
this_3 : IsGalois K L := ⋯
Hprod : ∏ σ : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((σ : (a : L) → E) ζ : E) = eval 1 (cyclotomic' n E)
this : NeZero.{v} (R := E) (↑n : E)
a : eval 1 (cyclotomic' n E) = ((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K)
a₁ :
  Eq (α := E) (eval 1 (∏ μ ∈ primitiveRoots n E, HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) μ : E[X])))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
a₂ : eval 1 (cyclotomic n E) = ((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K)
a₃ :
  eval 1 (Polynomial.map (Int.castRingHom E) (cyclotomic n ℤ)) =
    ((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K)
a₄ : eval 1 (Polynomial.map (Int.castRingHom E) (cyclotomic n ℤ)) = (↑(eval 1 (cyclotomic n ℤ)) : E)
a₅ : eval (↑1 : E) (Polynomial.map (Int.castRingHom E) (cyclotomic n ℤ)) = (↑(eval 1 (cyclotomic n ℤ)) : E)
⊢ Eq.{v + 1} (α := E) (∏ x : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((x : (a : L) → E) ζ : E))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
have a₆ : Eq (α := E) ((Int.castRingHom E : (a : ℤ) → E) (eval (↑1 : ℤ) (cyclotomic n ℤ)) : E)
  ((↑(eval 1 (cyclotomic n ℤ)) : E) : E)
Tactic: rw [Hprod, cyclotomic', ← cyclotomic_eq_prod_X_sub_primitiveRoots (isRoot_cyclotomic_iff.1 hz),
    ← map_cyclotomic_int, _root_.map_intCast, ← Int.cast_one, eval_intCast_map, eq_intCast,
    Int.cast_id]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this_1 : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
z : E
hz : IsRoot (cyclotomic n E) z
this_2 : FiniteDimensional K L := ⋯
this_3 : IsGalois K L := ⋯
Hprod : ∏ σ : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((σ : (a : L) → E) ζ : E) = eval 1 (cyclotomic' n E)
this : NeZero.{v} (R := E) (↑n : E)
a : eval 1 (cyclotomic' n E) = ((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K)
a₁ :
  Eq (α := E) (eval 1 (∏ μ ∈ primitiveRoots n E, HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) μ : E[X])))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
a₂ : eval 1 (cyclotomic n E) = ((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K)
a₃ :
  eval 1 (Polynomial.map (Int.castRingHom E) (cyclotomic n ℤ)) =
    ((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K)
a₄ : eval 1 (Polynomial.map (Int.castRingHom E) (cyclotomic n ℤ)) = (↑(eval 1 (cyclotomic n ℤ)) : E)
a₅ : eval (↑1 : E) (Polynomial.map (Int.castRingHom E) (cyclotomic n ℤ)) = (↑(eval 1 (cyclotomic n ℤ)) : E)
a₆ :
  Eq (α := E) ((Int.castRingHom E : (a : ℤ) → E) (eval (↑1 : ℤ) (cyclotomic n ℤ)) : E)
    ((↑(eval 1 (cyclotomic n ℤ)) : E) : E)
⊢ Eq.{v + 1} (α := E) (∏ x : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((x : (a : L) → E) ζ : E))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
have a₇ : Eq.{v + 1} (α := E) (↑(eval (↑1 : ℤ) (cyclotomic n ℤ)) : E) (↑(eval 1 (cyclotomic n ℤ)) : E)
Tactic: rw [Hprod, cyclotomic', ← cyclotomic_eq_prod_X_sub_primitiveRoots (isRoot_cyclotomic_iff.1 hz),
    ← map_cyclotomic_int, _root_.map_intCast, ← Int.cast_one, eval_intCast_map, eq_intCast,
    Int.cast_id]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this_1 : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
z : E
hz : IsRoot (cyclotomic n E) z
this_2 : FiniteDimensional K L := ⋯
this_3 : IsGalois K L := ⋯
Hprod : ∏ σ : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((σ : (a : L) → E) ζ : E) = eval 1 (cyclotomic' n E)
this : NeZero.{v} (R := E) (↑n : E)
a : eval 1 (cyclotomic' n E) = ((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K)
a₁ :
  Eq (α := E) (eval 1 (∏ μ ∈ primitiveRoots n E, HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) μ : E[X])))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
a₂ : eval 1 (cyclotomic n E) = ((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K)
a₃ :
  eval 1 (Polynomial.map (Int.castRingHom E) (cyclotomic n ℤ)) =
    ((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K)
a₄ : eval 1 (Polynomial.map (Int.castRingHom E) (cyclotomic n ℤ)) = (↑(eval 1 (cyclotomic n ℤ)) : E)
a₅ : eval (↑1 : E) (Polynomial.map (Int.castRingHom E) (cyclotomic n ℤ)) = (↑(eval 1 (cyclotomic n ℤ)) : E)
a₆ :
  Eq (α := E) ((Int.castRingHom E : (a : ℤ) → E) (eval (↑1 : ℤ) (cyclotomic n ℤ)) : E)
    ((↑(eval 1 (cyclotomic n ℤ)) : E) : E)
a₇ : Eq.{v + 1} (α := E) (↑(eval (↑1 : ℤ) (cyclotomic n ℤ)) : E) (↑(eval 1 (cyclotomic n ℤ)) : E)
⊢ Eq.{v + 1} (α := E) (∏ x : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((x : (a : L) → E) ζ : E))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
have a₈ : Eq.{v + 1} (α := E) (↑(eval 1 (cyclotomic n ℤ)) : E) (↑(eval 1 (cyclotomic n ℤ)) : E)
Tactic: rw [Hprod, cyclotomic', ← cyclotomic_eq_prod_X_sub_primitiveRoots (isRoot_cyclotomic_iff.1 hz),
    ← map_cyclotomic_int, _root_.map_intCast, ← Int.cast_one, eval_intCast_map, eq_intCast,
    Int.cast_id]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
hn : IsPrimePow n
inst_4 : IsCyclotomicExtension {n} K L
hirr : Irreducible (M := K[X]) (cyclotomic n K)
h : n ≠ 2
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ - 1) : K) ((↑n.minFac : K) : K)
have this : succ 1 < n
Tactic: have := (lt_of_le_of_ne (succ_le_of_lt (IsPrimePow.one_lt hn)) h.symm)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
hn : IsPrimePow n
inst_4 : IsCyclotomicExtension {n} K L
hirr : Irreducible (M := K[X]) (cyclotomic n K)
h : n ≠ 2
this : succ 1 < n
hprime : Fact (Nat.Prime n.minFac) := ⋯
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ - 1) : K) ((↑n.minFac : K) : K)
have rw : Eq.{u + 1} (α := K) (↑(eval 1 (cyclotomic n ℤ)) : K) (↑n.minFac : K)
Tactic: rw [sub_one_norm_eq_eval_cyclotomic hζ this hirr]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
hn : IsPrimePow n
inst_4 : IsCyclotomicExtension {n} K L
hirr : Irreducible (M := K[X]) (cyclotomic n K)
h : n ≠ 2
this : succ 1 < n
hprime : Fact (Nat.Prime n.minFac) := ⋯
⊢ Eq.{u + 1} (α := K) (↑(eval 1 (cyclotomic n ℤ)) : K) (↑n.minFac : K)
have nth_rw : Eq.{u + 1} (α := K)
  (↑(eval 1 (cyclotomic (HPow.hPow (β := ℕ) n.minFac ((n.factorization : (a : ℕ) → ℕ) n.minFac : ℕ)) ℤ)) : K)
  (↑n.minFac : K)
Tactic: nth_rw 1 [← IsPrimePow.minFac_pow_factorization_eq hn]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
hn : IsPrimePow n
inst_4 : IsCyclotomicExtension {n} K L
hirr : Irreducible (M := K[X]) (cyclotomic n K)
h : n ≠ 2
this : succ 1 < n
hprime : Fact (Nat.Prime n.minFac) := ⋯
⊢ Eq.{u + 1} (α := K)
    (↑(eval 1 (cyclotomic (HPow.hPow (β := ℕ) n.minFac ((n.factorization : (a : ℕ) → ℕ) n.minFac : ℕ)) ℤ)) : K)
    (↑n.minFac : K)
have obtain : ∀ (k : ℕ) (hk : (n.factorization : (a : ℕ) → ℕ) n.minFac = k + 1),
  Eq.{u + 1} (α := K)
    (↑(eval 1 (cyclotomic (HPow.hPow (β := ℕ) n.minFac ((n.factorization : (a : ℕ) → ℕ) n.minFac : ℕ)) ℤ)) : K)
    (↑n.minFac : K)
Tactic: obtain ⟨k, hk⟩ : ∃ k, n.factorization n.minFac = k + 1 :=
    exists_eq_succ_of_ne_zero
      ((n.factorization.mem_support_toFun n.minFac).1 <|
        mem_primeFactors_iff_mem_primeFactorsList.2 <|
          (mem_primeFactorsList (IsPrimePow.ne_zero hn)).2 ⟨hprime.out, minFac_dvd _⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
n : ℕ
inst : NeZero n
A : Type w
K : Type u
inst_1 : CommRing A
inst_2 : Field K
inst_3 : Algebra K A
inst_4 : IsDomain A
ζ : A
inst_5 : IsCyclotomicExtension {n} K A
hζ : IsPrimitiveRoot ζ n
h : Irreducible (M := K[X]) (cyclotomic n K)
⊢ minpoly K (ζ - 1) = comp (cyclotomic n K) (HAdd.hAdd (α := K[X]) X 1)
have this : NeZero.{u} (R := K) (↑n : K)
Tactic: haveI := IsCyclotomicExtension.neZero' n K A
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
A : Type w
K : Type u
inst_1 : CommRing A
inst_2 : Field K
inst_3 : Algebra K A
inst_4 : IsDomain A
ζ : A
inst_5 : IsCyclotomicExtension {n} K A
hζ : IsPrimitiveRoot ζ n
h : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
⊢ minpoly K (ζ - 1) = comp (cyclotomic n K) (HAdd.hAdd (α := K[X]) X 1)
have rw : comp (minpoly K ζ) (HSub.hSub (α := K[X]) X ((C : (a : K) → K[X]) (-1))) =
  comp (minpoly K ζ) (HAdd.hAdd (α := K[X]) X 1)
Tactic: rw [show ζ - 1 = ζ + algebraMap K A (-1) by simp [sub_eq_add_neg],
    minpoly.add_algebraMap ζ,
    hζ.minpoly_eq_cyclotomic_of_irreducible h]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ p ^ s - 1) = HPow.hPow (α := K) (↑p : K) (p ^ s)
have hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
Tactic: have hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K) :=
    cyclotomic_irreducible_pow_of_irreducible_pow hpri.1 (by lia) hirr
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
⊢ IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
have rw : IsPrimitiveRoot (ζ ^ p ^ s) (p ^ (k + 1 - s))
Tactic: rw [sub_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
⊢ IsPrimitiveRoot (ζ ^ p ^ s) (p ^ (k + 1 - s))
have refine : p ^ (k + 1) = p ^ s * p ^ (k + 1 - s)
Tactic: refine IsPrimitiveRoot.pow (pos_of_neZero (p ^ (k + 1))) hζ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
⊢ p ^ (k + 1) = p ^ s * p ^ (k + 1 - s)
have rw : p ^ (k + 1) = p ^ (s + (k + 1 - s))
Tactic: rw [← pow_add, add_comm s, Nat.sub_add_cancel (le_trans hs (Nat.le_succ k))]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
rw : p ^ (k + 1) = p ^ (s + (k + 1 - s))
⊢ p ^ (k + 1) = p ^ s * p ^ (k + 1 - s)
have rw₁ : p ^ (k + 1) = p ^ (k + 1 - s + s)
Tactic: rw [← pow_add, add_comm s, Nat.sub_add_cancel (le_trans hs (Nat.le_succ k))]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
rw : p ^ (k + 1) = p ^ (s + (k + 1 - s))
rw₁ : p ^ (k + 1) = p ^ (k + 1 - s + s)
⊢ p ^ (k + 1) = p ^ s * p ^ (k + 1 - s)
have rw₂ : p ^ (k + 1) = p ^ k.succ
Tactic: rw [← pow_add, add_comm s, Nat.sub_add_cancel (le_trans hs (Nat.le_succ k))]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
⊢ (Algebra.norm K : (a : L) → K) η = HPow.hPow (α := K) (↑p : K) (p ^ s)
have hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
Tactic: have hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s)) := by
    rw [sub_add_cancel]
    refine IsPrimitiveRoot.pow (pos_of_neZero (p ^ (k + 1))) hζ ?_
    rw [← pow_add, add_comm s, Nat.sub_add_cancel (le_trans hs (Nat.le_succ k))]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
⊢ Eq (α := IntermediateField K L) K⟮η⟯ K⟮η + 1⟯
have refine_1 : LE.le (α := IntermediateField K L) K⟮η⟯ K⟮η + 1⟯
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
refine_1 : LE.le (α := IntermediateField K L) K⟮η⟯ K⟮η + 1⟯
⊢ Eq (α := IntermediateField K L) K⟮η⟯ K⟮η + 1⟯
have refine_2 : LE.le (α := IntermediateField K L) K⟮η + 1⟯ K⟮η⟯
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
⊢ LE.le (α := IntermediateField K L) K⟮η⟯ K⟮η + 1⟯
have refine_1 : Membership.mem (γ := IntermediateField K L) K⟮η + 1⟯ η
Tactic: rw [IntermediateField.adjoin_simple_le_iff]