awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
K : Type u
L : Type v
inst : CommRing L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
inst_3 : IsDomain L
inst_4 : NeZero (R := ℕ) 2
hζ : IsPrimitiveRoot ζ 2
inst_5 : IsCyclotomicExtension {2} K L
hirr : Irreducible (M := K[X]) (cyclotomic 2 K)
pos pos₁ pos₂ pos₃ : Eq.{u + 1} (α := K) (↑(Int.negSucc 0 ^ φ 2) : K) (↑(Int.negSucc 0) : K)
⊢ HPow.hPow (α := K) (-1) (φ 2) = -1

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hirr : Irreducible (M := K[X]) (cyclotomic n K)
hn : ¬n = 2
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)

Tactic:
hζ.norm_eq_one hn hirr

Premises used: IsPrimitiveRoot.norm_eq_one
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hirr : Irreducible (M := K[X]) (cyclotomic n K)
hn : ¬n = 2
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)

Tactic:
exact hζ.norm_eq_one hn hirr

Premises used: IsPrimitiveRoot.norm_eq_one
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
⊢ NeZero.{u} (R := K) (↑n : K)

Tactic:
haveI := IsCyclotomicExtension.neZero' n K L
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
obtain :
  ∀ (z : E) (hz : IsRoot (cyclotomic n E) z),
    Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ - 1) : K) ((↑(eval 1 (cyclotomic n ℤ)) : K) : K)
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ - 1) : K) ((↑(eval 1 (cyclotomic n ℤ)) : K) : K)

Tactic:
obtain ⟨z, hz⟩ := IsAlgClosed.exists_root _ (degree_cyclotomic_pos n E (NeZero.pos _)).ne.symm

Premises used: Ne.symm, IsAlgClosed.exists_root, NeZero.pos, Polynomial.degree_cyclotomic_pos, LT.lt.ne
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
z : E
hz : IsRoot (cyclotomic n E) z
a :
  Eq.{v + 1} (α := E) (((algebraMap K E : K →+* E) : (a : K) → E) ((Algebra.norm K : (a : L) → K) (ζ - 1)) : E)
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K) : E)
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ - 1) : K) ((↑(eval 1 (cyclotomic n ℤ)) : K) : K)

Tactic:
apply (algebraMap K E).injective

Premises used: Algebra.algebraMap, RingHom.injective
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 : IsGalois K L := ⋯
a :
  Eq.{v + 1} (α := E) (∏ σ : L →ₐ[K] E, (σ : (a : L) → E) (ζ - 1))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
⊢ Eq.{v + 1} (α := E) (((algebraMap K E : K →+* E) : (a : K) → E) ((Algebra.norm K : (a : L) → K) (ζ - 1)) : E)
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K) : E)

Tactic:
rw [norm_eq_prod_embeddings]

Premises used: Algebra.norm_eq_prod_embeddings
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 : IsGalois K L := ⋯
s : Finset.univ
f : fun (σ : L →ₐ[K] E) ↦ (σ : (a : L) → E) (ζ - 1)
| ∏ σ : L →ₐ[K] E, (σ : (a : L) → E) (ζ - 1)

Tactic:
congr
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 : IsGalois K L := ⋯
| Finset.univ

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 : IsGalois K L := ⋯
f : ∀ (x : L →ₐ[K] E), (x : (a : L) → E) (ζ - 1)
| fun (σ : L →ₐ[K] E) ↦ (σ : (a : L) → E) (ζ - 1)

Tactic:
ext
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 : IsGalois K L := ⋯
x : L →ₐ[K] E
f : -1 * HSub.hSub (α := E) (β := E) (1 : E) ((x : (a : L) → E) ζ : E)
| (x : (a : L) → E) (ζ - 1)

Tactic:
rw [← neg_sub, map_neg, map_sub, map_one, neg_eq_neg_one_mul]

Premises used: neg_sub, map_sub, map_neg, map_one, neg_eq_neg_one_mul
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 : IsGalois K L := ⋯
f : ∀ (x : L →ₐ[K] E), -1 * HSub.hSub (α := E) (β := E) (1 : E) ((x : (a : L) → E) ζ : E)
| ∏ σ : L →ₐ[K] E, (σ : (a : L) → E) (ζ - 1)

Tactic:
congr
    rfl
    ext
    rw [← neg_sub, map_neg, map_sub, map_one, neg_eq_neg_one_mul]

Premises used: neg_sub, map_sub, map_neg, map_one, neg_eq_neg_one_mul
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 : IsGalois K L := ⋯
a :
  Eq.{v + 1} (α := E) (∏ x : L →ₐ[K] E, -1 * HSub.hSub (α := E) (β := E) (1 : E) ((x : (a : L) → E) ζ : E))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
⊢ Eq.{v + 1} (α := E) (∏ σ : L →ₐ[K] E, (σ : (a : L) → E) (ζ - 1))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))

Tactic:
conv_lhs =>
    congr
    rfl
    ext
    rw [← neg_sub, map_neg, map_sub, map_one, neg_eq_neg_one_mul]

Premises used: neg_sub, map_sub, map_neg, map_one, neg_eq_neg_one_mul
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 : IsGalois K L := ⋯
a :
  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))
⊢ Eq.{v + 1} (α := E) (∏ x : L →ₐ[K] E, -1 * HSub.hSub (α := E) (β := E) (1 : E) ((x : (a : L) → E) ζ : E))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))

Tactic:
rw [prod_mul_distrib, prod_const, Finset.card_univ, AlgHom.card,
    IsCyclotomicExtension.finrank L hirr, (totient_even h).neg_one_pow, one_mul]

Premises used: Finset.card_univ, Finset.prod_mul_distrib, IsCyclotomicExtension.finrank, Even.neg_one_pow, Finset.prod_const, AlgHom.card, one_mul, Nat.totient_even
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 : IsGalois K L := ⋯
rw :
  Eq.{v + 1} (α := E) (∏ σ : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((σ : (a : L) → E) ζ : E))
    (∏ x : ↥(primitiveRoots n E), eval 1 (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) (↑x : E) : E[X])))
⊢ ∏ σ : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((σ : (a : L) → E) ζ : E) = eval 1 (cyclotomic' n E)

Tactic:
rw [cyclotomic', eval_prod, ← @Finset.prod_attach E E, ← univ_eq_attach]

Premises used: Polynomial.eval_prod, Finset.univ_eq_attach, Polynomial.cyclotomic', Finset.prod_attach
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 : IsGalois K L := ⋯
⊢ Eq.{v + 1} (α := E) (∏ σ : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((σ : (a : L) → E) ζ : E))
    (∏ x : ↥(primitiveRoots n E), eval 1 (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) (↑x : E) : E[X])))

Tactic:
Fintype.prod_equiv (hζ.embeddingsEquivPrimitiveRoots E hirr) _ _ fun σ => ?_

Premises used: Fintype.prod_equiv, IsPrimitiveRoot.embeddingsEquivPrimitiveRoots
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 : IsGalois K L := ⋯
refine :
  ∀ (σ : L →ₐ[K] E),
    HSub.hSub (α := E) (β := E) (1 : E) ((σ : (a : L) → E) ζ : E) =
      eval 1
        (HSub.hSub (α := E[X]) X
          ((C : (a : E) → E[X])
            (↑((hζ.embeddingsEquivPrimitiveRoots E hirr : (a : L →ₐ[K] E) → ↥(primitiveRoots n E)) σ) : E)))
⊢ Eq.{v + 1} (α := E) (∏ σ : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((σ : (a : L) → E) ζ : E))
    (∏ x : ↥(primitiveRoots n E), eval 1 (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) (↑x : E) : E[X])))

Tactic:
refine Fintype.prod_equiv (hζ.embeddingsEquivPrimitiveRoots E hirr) _ _ fun σ => ?_

Premises used: Fintype.prod_equiv, IsPrimitiveRoot.embeddingsEquivPrimitiveRoots
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 : IsGalois K L := ⋯
σ : L →ₐ[K] E
⊢ HSub.hSub (α := E) (β := E) (1 : E) ((σ : (a : L) → E) ζ : E) =
    eval 1
      (HSub.hSub (α := E[X]) X
        ((C : (a : E) → E[X])
          (↑((hζ.embeddingsEquivPrimitiveRoots E hirr : (a : L →ₐ[K] E) → ↥(primitiveRoots n E)) σ) : E)))

Tactic:
simp
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 : IsGalois K L := ⋯
⊢ ∏ σ : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((σ : (a : L) → E) ζ : E) = eval 1 (cyclotomic' n E)

Tactic:
have Hprod : (Finset.univ.prod fun σ : L →ₐ[K] E => 1 - σ ζ) = eval 1 (cyclotomic' n E) := by
    rw [cyclotomic', eval_prod, ← @Finset.prod_attach E E, ← univ_eq_attach]
    refine Fintype.prod_equiv (hζ.embeddingsEquivPrimitiveRoots E hirr) _ _ fun σ => ?_
    simp
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 : IsGalois K L := ⋯
Hprod : ∏ σ : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((σ : (a : L) → E) ζ : E) = eval 1 (cyclotomic' n E)
⊢ NeZero.{v} (R := E) (↑n : E)

Tactic:
have : NeZero (n : E) := NeZero.of_faithfulSMul K _ n
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
a₈ 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))

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]

Premises used: Polynomial.cyclotomic_eq_prod_X_sub_primitiveRoots, map_intCast, eq_intCast, Polynomial.eval_intCast_map, Polynomial.cyclotomic', Polynomial.map_cyclotomic_int, Iff.mp, Int.cast_id, Int.cast_one, Polynomial.isRoot_cyclotomic_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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
⊢ succ 1 < n

Tactic:
have := (lt_of_le_of_ne (succ_le_of_lt (IsPrimePow.one_lt hn)) h.symm)
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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) := ⋯
rw : Eq.{u + 1} (α := K) (↑(eval 1 (cyclotomic n ℤ)) : K) (↑n.minFac : K)
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ - 1) : K) ((↑n.minFac : K) : K)

Tactic:
rw [sub_one_norm_eq_eval_cyclotomic hζ this hirr]

Premises used: IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomic
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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) := ⋯
nth_rw :
  Eq.{u + 1} (α := K)
    (↑(eval 1 (cyclotomic (HPow.hPow (β := ℕ) n.minFac ((n.factorization : (a : ℕ) → ℕ) n.minFac : ℕ)) ℤ)) : K)
    (↑n.minFac : K)
⊢ Eq.{u + 1} (α := K) (↑(eval 1 (cyclotomic n ℤ)) : K) (↑n.minFac : K)

Tactic:
nth_rw 1 [← IsPrimePow.minFac_pow_factorization_eq hn]

Premises used: IsPrimePow.minFac_pow_factorization_eq
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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) := ⋯
⊢ ∃ (k : ℕ), (n.factorization : (a : ℕ) → ℕ) n.minFac = k + 1

Tactic:
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 _⟩)

Premises used: Iff.mpr, Nat.minFac, Nat.minFac_dvd, Nat.mem_primeFactorsList, Nat.exists_eq_succ_of_ne_zero, And.intro, Nat.mem_primeFactors_iff_mem_primeFactorsList, IsPrimePow.ne_zero, Iff.mp, Finsupp.mem_support_toFun, Nat.factorization, Fact.out
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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) := ⋯
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)
⊢ 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 _⟩)

Premises used: Iff.mpr, Nat.minFac, Nat.minFac_dvd, Nat.mem_primeFactorsList, Nat.exists_eq_succ_of_ne_zero, And.intro, Nat.mem_primeFactors_iff_mem_primeFactorsList, IsPrimePow.ne_zero, Iff.mp, Finsupp.mem_support_toFun, DFunLike.coe, Nat.factorization, Fact.out
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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) := ⋯
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:
simp [hk]
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
⊢ NeZero.{u} (R := K) (↑n : K)

Tactic:
haveI := IsCyclotomicExtension.neZero' n K A
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
⊢ ζ - 1 = HAdd.hAdd (β := A) ζ ((algebraMap K A : (a : K) → A) (-1) : A)

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
rw :
  comp (minpoly K ζ) (HSub.hSub (α := K[X]) X ((C : (a : K) → K[X]) (-1))) =
    comp (minpoly K ζ) (HAdd.hAdd (α := K[X]) X 1)
⊢ minpoly K (ζ - 1) = comp (cyclotomic n 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]

Premises used: IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible, minpoly.add_algebraMap
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
⊢ comp (minpoly K ζ) (HSub.hSub (α := K[X]) X ((C : (a : K) → K[X]) (-1))) =
    comp (minpoly K ζ) (HAdd.hAdd (α := K[X]) X 1)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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
⊢ k - s + 1 ≤ k + 1

Tactic:
lia