awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h_1 : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n
h : ∃ i < n, zeta n K L ^ i = μ
pf : h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ).Coprime n
hμ :
  IsPrimitiveRoot
    (zeta n K L ^ (↑(ZMod.unitOfCoprime (h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ)) pf) : ZMod n).val) n
pf_1 :
  Eq (α := K[X]) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))
    (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)))
h₁ :
  (↑(ZMod.unitOfCoprime (h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ)) pf) : ZMod n).val =
    h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ)
⊢ zeta n K L ^ (↑(ZMod.unitOfCoprime (h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ)) pf) : ZMod n).val = μ

Tactic:
convert! h.choose_spec.2

Premises used: Exists.choose_spec, And.right
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h_1 : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n
h : ∃ i < n, zeta n K L ^ i = μ
pf : h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ).Coprime n
hμ :
  IsPrimitiveRoot
    (zeta n K L ^ (↑(ZMod.unitOfCoprime (h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ)) pf) : ZMod n).val) n
pf_1 :
  Eq (α := K[X]) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))
    (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)))
⊢ (↑(ZMod.unitOfCoprime (h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ)) pf) : ZMod n).val =
    h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ)

Tactic:
ZMod.val_cast_of_lt h.choose_spec.1

Premises used: Exists.choose_spec, ZMod.val_cast_of_lt, And.left
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h_1 : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n
h : ∃ i < n, zeta n K L ^ i = μ
pf : h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ).Coprime n
hμ :
  IsPrimitiveRoot
    (zeta n K L ^ (↑(ZMod.unitOfCoprime (h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ)) pf) : ZMod n).val) n
pf_1 :
  Eq (α := K[X]) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))
    (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)))
⊢ (↑(ZMod.unitOfCoprime (h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ)) pf) : ZMod n).val =
    h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ)

Tactic:
exact ZMod.val_cast_of_lt h.choose_spec.1

Premises used: Exists.choose_spec, ZMod.val_cast_of_lt, And.left
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
A : Type w
B : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension {n} A B
⊢ IsPrimitiveRoot (zeta n A B) n

Tactic:
(exists_isPrimitiveRoot A B (Set.mem_singleton n) (NeZero.ne _) :
    ∃ r : B, IsPrimitiveRoot r n).choose_spec

Premises used: Set.mem_singleton, Exists.choose_spec, IsCyclotomicExtension.exists_isPrimitiveRoot, NeZero.ne, IsCyclotomicExtension.zeta
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
A : Type w
B : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension {n} A B
inst_5 : IsDomain B
inst_6 : NeZero.{z} (R := B) (↑n : B)
rw : IsPrimitiveRoot (zeta n A B) n
⊢ Eq.{z + 1} (α := B) ((aeval (zeta n A B) : (a : A[X]) → B) (cyclotomic n A) : B) (0 : B)

Tactic:
rw [← eval_map_algebraMap, ← IsRoot.def, map_cyclotomic, isRoot_cyclotomic_iff]

Premises used: Polynomial.IsRoot.def, Polynomial.eval_map_algebraMap, Polynomial.map_cyclotomic, Polynomial.isRoot_cyclotomic_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
A : Type w
B : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension {n} A B
inst_5 : IsDomain B
inst_6 : NeZero.{z} (R := B) (↑n : B)
⊢ IsPrimitiveRoot (zeta n A B) n

Tactic:
zeta_spec n A B

Premises used: IsCyclotomicExtension.zeta_spec
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
A : Type w
B : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension {n} A B
inst_5 : IsDomain B
inst_6 : NeZero.{z} (R := B) (↑n : B)
⊢ IsPrimitiveRoot (zeta n A B) n

Tactic:
exact zeta_spec n A B

Premises used: IsCyclotomicExtension.zeta_spec
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
A : Type w
B : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension {n} A B
inst_5 : IsDomain B
inst_6 : NeZero.{z} (R := B) (↑n : B)
⊢ Eq.{z + 1} (α := B) ((aeval (zeta n A B) : (a : A[X]) → B) (cyclotomic n A) : B) (0 : B)

Tactic:
aeval_zeta n A B

Premises used: IsCyclotomicExtension.aeval_zeta
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
A : Type w
B : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension {n} A B
inst_5 : IsDomain B
inst_6 : NeZero.{z} (R := B) (↑n : B)
a :
  IsRoot (cyclotomic n B) (zeta n A B) ↔
    Eq.{z + 1} (α := B) ((aeval (zeta n A B) : (a : A[X]) → B) (cyclotomic n A) : B) (0 : B)
⊢ IsRoot (cyclotomic n B) (zeta n A B)

Tactic:
convert! aeval_zeta n A B using 0

Premises used: IsCyclotomicExtension.aeval_zeta
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
A : Type w
B : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension {n} A B
inst_5 : IsDomain B
inst_6 : NeZero.{z} (R := B) (↑n : B)
a :
  eval (zeta n A B) (cyclotomic n B) = 0 ↔
    Eq.{z + 1} (α := B) ((aeval (zeta n A B) : (a : A[X]) → B) (cyclotomic n A) : B) (0 : B)
a₁ : eval (zeta n A B) (cyclotomic n B) = 0 ↔ eval₂ (algebraMap A B) (zeta n A B) (cyclotomic n A) = 0
a₂ : eval (zeta n A B) (cyclotomic n B) = 0 ↔ eval (zeta n A B) (Polynomial.map (algebraMap A B) (cyclotomic n A)) = 0
a₃ a₄ : eval (zeta n A B) (cyclotomic n B) = 0 ↔ eval (zeta n A B) (cyclotomic n B) = 0
⊢ IsRoot (cyclotomic n B) (zeta n A B) ↔
    Eq.{z + 1} (α := B) ((aeval (zeta n A B) : (a : A[X]) → B) (cyclotomic n A) : B) (0 : B)

Tactic:
rw [IsRoot.def, aeval_def, eval₂_eq_eval_map, map_cyclotomic]

Premises used: Polynomial.IsRoot.def, Polynomial.aeval_def, Polynomial.map_cyclotomic, Polynomial.eval₂_eq_eval_map
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
A : Type w
B : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension {n} A B
⊢ zeta n A B ^ n = 1

Tactic:
(zeta_spec n A B).pow_eq_one

Premises used: IsCyclotomicExtension.zeta_spec, IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field K
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
rw : ∃ (x : K[X]), (aeval (ζ - 1) : (a : K[X]) → L) x = ζ
⊢ Membership.mem (γ := Subalgebra K L) K[ζ - 1] (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))

Tactic:
rw [powerBasis_gen, adjoin_singleton_eq_range_aeval, AlgHom.mem_range]

Premises used: IsPrimitiveRoot.powerBasis_gen, Algebra.adjoin_singleton_eq_range_aeval, AlgHom.mem_range
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field K
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
⊢ (aeval (ζ - 1) : (a : K[X]) → L) (HAdd.hAdd (α := K[X]) X 1) = ζ

Tactic:
simp
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field K
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
⊢ ∃ (x : K[X]), (aeval (ζ - 1) : (a : K[X]) → L) x = ζ

Tactic:
exact ⟨X + 1, by simp⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
p n : ℕ
inst : NeZero n
A : Type w
B : Type z
K : Type u
L : Type v
C : Type w
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension {n} A B
inst_5 : Field K
inst_6 : CommRing L
inst_7 : IsDomain L
inst_8 : Algebra K L
inst_9 : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
apply : Eq (α := Subalgebra K L) K[ζ - 1] ⊤
⊢ PowerBasis K L

Tactic:
apply PowerBasis.ofAdjoinEqTop (((integral {n} K L).isIntegral ζ).sub isIntegral_one)

Premises used: Algebra.IsIntegral.isIntegral, PowerBasis.ofAdjoinEqTop, IsIntegral.sub, isIntegral_one
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
p n : ℕ
inst : NeZero n
A : Type w
B : Type z
K : Type u
L : Type v
C : Type w
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension {n} A B
inst_5 : Field K
inst_6 : CommRing L
inst_7 : IsDomain L
inst_8 : Algebra K L
inst_9 : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
⊢ Eq (α := Subalgebra K L) K[ζ - 1] ⊤

Tactic:
PowerBasis.adjoin_eq_top_of_gen_mem_adjoin (hζ.powerBasis_gen_mem_adjoin_zeta_sub_one _)

Premises used: IsPrimitiveRoot.powerBasis_gen_mem_adjoin_zeta_sub_one, PowerBasis.adjoin_eq_top_of_gen_mem_adjoin
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
p n : ℕ
inst : NeZero n
A : Type w
B : Type z
K : Type u
L : Type v
C : Type w
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension {n} A B
inst_5 : Field K
inst_6 : CommRing L
inst_7 : IsDomain L
inst_8 : Algebra K L
inst_9 : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
⊢ Eq (α := Subalgebra K L) K[ζ - 1] ⊤

Tactic:
exact PowerBasis.adjoin_eq_top_of_gen_mem_adjoin (hζ.powerBasis_gen_mem_adjoin_zeta_sub_one _)

Premises used: IsPrimitiveRoot.powerBasis_gen_mem_adjoin_zeta_sub_one, PowerBasis.adjoin_eq_top_of_gen_mem_adjoin
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
p n : ℕ
inst : NeZero n
A : Type w
B : Type z
K : Type u
L : Type v
C_1 : Type w
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension {n} A B
inst_5 : Field K
inst_6 : CommRing L
inst_7 : IsDomain L
inst_8 : Algebra K L
inst_9 : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
C : Type u_1
inst_10 : CommRing C
inst_11 : IsDomain C
inst_12 : Algebra K C
hirr : Irreducible (M := K[X]) (cyclotomic n K)
x :
  { y : C //
    Eq.{u_1 + 1} (α := C)
      ((aeval y : (a : K[X]) → C) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))) : C) (0 : C) }
⊢ NeZero.{u} (R := K) (↑n : K)

Tactic:
haveI := IsCyclotomicExtension.neZero' n K L
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
p n : ℕ
inst : NeZero n
A : Type w
B : Type z
K : Type u
L : Type v
C_1 : Type w
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension {n} A B
inst_5 : Field K
inst_6 : CommRing L
inst_7 : IsDomain L
inst_8 : Algebra K L
inst_9 : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
C : Type u_1
inst_10 : CommRing C
inst_11 : IsDomain C
inst_12 : Algebra K C
hirr : Irreducible (M := K[X]) (cyclotomic n K)
x :
  { y : C //
    Eq.{u_1 + 1} (α := C)
      ((aeval y : (a : K[X]) → C) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))) : C) (0 : C) }
this : NeZero.{u} (R := K) (↑n : K)
⊢ NeZero.{u_1} (R := C) (↑n : C)

Tactic:
haveI hn := NeZero.of_faithfulSMul K C n
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
p n : ℕ
inst : NeZero n
A : Type w
B : Type z
K : Type u
L : Type v
C_1 : Type w
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension {n} A B
inst_5 : Field K
inst_6 : CommRing L
inst_7 : IsDomain L
inst_8 : Algebra K L
inst_9 : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
C : Type u_1
inst_10 : CommRing C
inst_11 : IsDomain C
inst_12 : Algebra K C
hirr : Irreducible (M := K[X]) (cyclotomic n K)
x :
  { y : C //
    Eq.{u_1 + 1} (α := C)
      ((aeval y : (a : K[X]) → C) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))) : C) (0 : C) }
this : NeZero.{u} (R := K) (↑n : K)
hn : NeZero.{u_1} (R := C) (↑n : C)
refine : (↑x : C) ∈ primitiveRoots n C
⊢ ↥(primitiveRoots n C)

Tactic:
refine ⟨x.1, ?_⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
p n : ℕ
inst : NeZero n
A : Type w
B : Type z
K : Type u
L : Type v
C_1 : Type w
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension {n} A B
inst_5 : Field K
inst_6 : CommRing L
inst_7 : IsDomain L
inst_8 : Algebra K L
inst_9 : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
C : Type u_1
inst_10 : CommRing C
inst_11 : IsDomain C
inst_12 : Algebra K C
hirr : Irreducible (M := K[X]) (cyclotomic n K)
x :
  { y : C //
    Eq.{u_1 + 1} (α := C)
      ((aeval y : (a : K[X]) → C) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))) : C) (0 : C) }
this : NeZero.{u} (R := K) (↑n : K)
hn : NeZero.{u_1} (R := C) (↑n : C)
mk :
  ∀ (val : C)
    (property :
      Eq.{u_1 + 1} (α := C)
        ((aeval val : (a : K[X]) → C) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))) : C) (0 : C)),
    (↑(Subtype.mk (p := fun (y : C) ↦
            Eq.{u_1 + 1} (α := C)
              ((aeval y : (a : K[X]) → C) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))) : C) (0 : C))
            val property) :
        C) ∈
      primitiveRoots n C
⊢ (↑x : C) ∈ primitiveRoots n C

Tactic:
cases x
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
p n : ℕ
inst : NeZero n
A : Type w
B : Type z
K : Type u
L : Type v
C_1 : Type w
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension {n} A B
inst_5 : Field K
inst_6 : CommRing L
inst_7 : IsDomain L
inst_8 : Algebra K L
inst_9 : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
C : Type u_1
inst_10 : CommRing C
inst_11 : IsDomain C
inst_12 : Algebra K C
hirr : Irreducible (M := K[X]) (cyclotomic n K)
x : ↥(primitiveRoots n C)
⊢ NeZero.{u} (R := K) (↑n : K)

Tactic:
haveI := IsCyclotomicExtension.neZero' n K L
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
p n : ℕ
inst : NeZero n
A : Type w
B : Type z
K : Type u
L : Type v
C_1 : Type w
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension {n} A B
inst_5 : Field K
inst_6 : CommRing L
inst_7 : IsDomain L
inst_8 : Algebra K L
inst_9 : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
C : Type u_1
inst_10 : CommRing C
inst_11 : IsDomain C
inst_12 : Algebra K C
hirr : Irreducible (M := K[X]) (cyclotomic n K)
x : ↥(primitiveRoots n C)
this : NeZero.{u} (R := K) (↑n : K)
⊢ NeZero.{u_1} (R := C) (↑n : C)

Tactic:
haveI hn := NeZero.of_faithfulSMul K C n
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
p n : ℕ
inst : NeZero n
A : Type w
B : Type z
K : Type u
L : Type v
C_1 : Type w
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension {n} A B
inst_5 : Field K
inst_6 : CommRing L
inst_7 : IsDomain L
inst_8 : Algebra K L
inst_9 : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
C : Type u_1
inst_10 : CommRing C
inst_11 : IsDomain C
inst_12 : Algebra K C
hirr : Irreducible (M := K[X]) (cyclotomic n K)
x : ↥(primitiveRoots n C)
this : NeZero.{u} (R := K) (↑n : K)
hn : NeZero.{u_1} (R := C) (↑n : C)
refine :
  Eq.{u_1 + 1} (α := C)
    ((aeval (↑x : C) : (a : K[X]) → C) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))) : C) (0 : C)
⊢ { y : C //
    Eq.{u_1 + 1} (α := C)
      ((aeval y : (a : K[X]) → C) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))) : C) (0 : C) }

Tactic:
refine ⟨x.1, ?_⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
p n : ℕ
inst : NeZero n
A : Type w
B : Type z
K : Type u
L : Type v
C_1 : Type w
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension {n} A B
inst_5 : Field K
inst_6 : CommRing L
inst_7 : IsDomain L
inst_8 : Algebra K L
inst_9 : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
C : Type u_1
inst_10 : CommRing C
inst_11 : IsDomain C
inst_12 : Algebra K C
hirr : Irreducible (M := K[X]) (cyclotomic n K)
x : ↥(primitiveRoots n C)
this : NeZero.{u} (R := K) (↑n : K)
hn : NeZero.{u_1} (R := C) (↑n : C)
mk :
  ∀ (val : C) (property : val ∈ primitiveRoots n C),
    Eq.{u_1 + 1} (α := C)
      ((aeval (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ primitiveRoots n C) val property) : C) : (a : K[X]) → C)
          (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))) :
        C)
      (0 : C)
⊢ Eq.{u_1 + 1} (α := C)
    ((aeval (↑x : C) : (a : K[X]) → C) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))) : C) (0 : C)

Tactic:
cases x
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
p n : ℕ
inst : NeZero n
A : Type w
B : Type z
K : Type u
L : Type v
C_1 : Type w
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension {n} A B
inst_5 : Field K
inst_6 : CommRing L
inst_7 : IsDomain L
inst_8 : Algebra K L
inst_9 : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
C : Type u_1
inst_10 : CommRing C
inst_11 : IsDomain C
inst_12 : Algebra K C
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
hn : NeZero.{u_1} (R := C) (↑n : C)
val : C
property : val ∈ primitiveRoots n C
mk :
  eval₂ (algebraMap K C) (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ primitiveRoots n C) val property) : C)
      (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))) =
    0
mk₁ :
  eval (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ primitiveRoots n C) val property) : C)
      (Polynomial.map (algebraMap K C) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))) =
    0
mk₂ :
  eval (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ primitiveRoots n C) val property) : C)
      (Polynomial.map (algebraMap K C) (minpoly K ζ)) =
    0
mk₃ :
  eval (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ primitiveRoots n C) val property) : C)
      (Polynomial.map (algebraMap K C) (cyclotomic n K)) =
    0
mk₄ : eval (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ primitiveRoots n C) val property) : C) (cyclotomic n C) = 0
mk₅ : IsRoot (cyclotomic n C) (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ primitiveRoots n C) val property) : C)
mk₆ : IsPrimitiveRoot (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ primitiveRoots n C) val property) : C) n
mk₇ mk₈ mk₉ mk₁₀ : (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ primitiveRoots n C) val property) : C) ∈ primitiveRoots n C
⊢ Eq.{u_1 + 1} (α := C)
    ((aeval (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ primitiveRoots n C) val property) : C) : (a : K[X]) → C)
        (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))) :
      C)
    (0 : C)

Tactic:
rwa [aeval_def, eval₂_eq_eval_map, hζ.powerBasis_gen K, ←
          hζ.minpoly_eq_cyclotomic_of_irreducible hirr, map_cyclotomic, ← IsRoot.def,
          isRoot_cyclotomic_iff, ← mem_primitiveRoots (NeZero.pos _)]

Premises used: IsPrimitiveRoot.powerBasis_gen, Polynomial.IsRoot.def, Polynomial.aeval_def, IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible, mem_primitiveRoots, NeZero.pos, Polynomial.map_cyclotomic, Polynomial.eval₂_eq_eval_map, Polynomial.isRoot_cyclotomic_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field K
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
C : Type u_1
inst_6 : CommRing C
inst_7 : IsDomain C
inst_8 : Algebra K C
hirr : Irreducible (M := K[X]) (cyclotomic n K)
φ' : L →ₐ[K] C
⊢ Eq.{u_1 + 1} (α := C)
    ((↑((hζ.embeddingsEquivPrimitiveRoots C hirr : (a : L →ₐ[K] C) → ↥(primitiveRoots n C)) φ') : C) : C)
    ((φ' : (a : L) → C) ζ : C)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field K
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
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 K
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
rw : PowerBasis.dim (IsPrimitiveRoot.powerBasis K (ζ := zeta n K L) ⋯) = φ n
rw₁ : natDegree (minpoly K (zeta n K L)) = φ n
rw₂ : natDegree (cyclotomic n K) = φ n
rw₃ rw₄ : φ n = φ n
⊢ Module.finrank K L = φ n

Tactic:
rw [((zeta_spec n K L).powerBasis K).finrank, IsPrimitiveRoot.powerBasis_dim, ←
    (zeta_spec n K L).minpoly_eq_cyclotomic_of_irreducible hirr, natDegree_cyclotomic]

Premises used: IsPrimitiveRoot.powerBasis_dim, Polynomial.natDegree_cyclotomic, PowerBasis.finrank, IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible, IsCyclotomicExtension.zeta_spec, IsPrimitiveRoot.powerBasis
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
inst_4 : FiniteDimensional K L
p q : ℕ
x y : L
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hirr : Irreducible (M := K[X]) (cyclotomic (p.lcm q) K)
inl :
  ∀ (hx : IsPrimitiveRoot x 0) (hirr : Irreducible (M := K[X]) (cyclotomic (Nat.lcm 0 q) K)),
    φ (Nat.lcm 0 q) ≤ Module.finrank K L
inr : ∀ (hppos : p > 0), φ (p.lcm q) ≤ Module.finrank K L
⊢ φ (p.lcm q) ≤ Module.finrank K L

Tactic:
rcases Nat.eq_zero_or_pos p with (rfl | hppos)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
inst_4 : FiniteDimensional K L
q : ℕ
x y : L
hy : IsPrimitiveRoot y q
hx : IsPrimitiveRoot x 0
hirr : Irreducible (M := K[X]) (cyclotomic (Nat.lcm 0 q) K)
⊢ φ (Nat.lcm 0 q) ≤ Module.finrank K L

Tactic:
simp
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
inst_4 : FiniteDimensional K L
p q : ℕ
x y : L
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hirr : Irreducible (M := K[X]) (cyclotomic (p.lcm q) K)
hppos : p > 0
inr :
  ∀ (hy : IsPrimitiveRoot y 0) (hirr : Irreducible (M := K[X]) (cyclotomic (p.lcm 0) K)),
    φ (p.lcm 0) ≤ Module.finrank K L
inr₁ : ∀ (hqpos : q > 0), φ (p.lcm q) ≤ Module.finrank K L
⊢ φ (p.lcm q) ≤ Module.finrank K L

Tactic:
rcases Nat.eq_zero_or_pos q with (rfl | hqpos)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
inst_4 : FiniteDimensional K L
p : ℕ
x y : L
hx : IsPrimitiveRoot x p
hppos : p > 0
hy : IsPrimitiveRoot y 0
hirr : Irreducible (M := K[X]) (cyclotomic (p.lcm 0) K)
⊢ φ (p.lcm 0) ≤ Module.finrank K L

Tactic:
simp