awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
⊢ 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)
have 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
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 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
⊢ 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)
have 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
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 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
⊢ 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)
have mk₂ : eval (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ primitiveRoots n C) val property) : C)
    (Polynomial.map (algebraMap K C) (minpoly K ζ)) =
  0
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 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
⊢ 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)
have mk₃ : eval (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ primitiveRoots n C) val property) : C)
    (Polynomial.map (algebraMap K C) (cyclotomic n K)) =
  0
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 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
⊢ 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)
have mk₄ : eval (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ primitiveRoots n C) val property) : C) (cyclotomic n C) = 0
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 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
⊢ 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)
have mk₅ : IsRoot (cyclotomic n C) (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ primitiveRoots n C) val property) : 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 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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)
⊢ 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)
have mk₆ : IsPrimitiveRoot (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ primitiveRoots n C) val property) : C) n
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 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
⊢ 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)
have mk₇ : (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ primitiveRoots n C) val property) : C) ∈ primitiveRoots n 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 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
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)
⊢ Module.finrank K L = φ n
have this : NeZero.{u} (R := K) (↑n : K)
Tactic: haveI := IsCyclotomicExtension.neZero' n K L
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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)
⊢ Module.finrank K L = φ n
have rw : PowerBasis.dim (IsPrimitiveRoot.powerBasis K (ζ := zeta n K L) sorry) = φ 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
⊢ Module.finrank K L = φ n
have rw₁ : natDegree (minpoly K (zeta n 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
⊢ Module.finrank K L = φ n
have rw₂ : natDegree (cyclotomic n K) = φ 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
⊢ Module.finrank K L = φ n
have rw₃ : φ n = φ 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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)
⊢ φ (p.lcm q) ≤ Module.finrank K L
have inl : ∀ (hx : IsPrimitiveRoot x 0) (hirr : Irreducible (M := K[X]) (cyclotomic (Nat.lcm 0 q) K)),
  φ (Nat.lcm 0 q) ≤ Module.finrank K L
Tactic: rcases Nat.eq_zero_or_pos p with (rfl | hppos)
Cleared hypotheses: p, hx, hirr
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
⊢ φ (p.lcm q) ≤ Module.finrank K L
have inr : ∀ (hppos : p > 0), φ (p.lcm q) ≤ Module.finrank K L
Tactic: rcases Nat.eq_zero_or_pos p with (rfl | hppos)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
⊢ φ (p.lcm q) ≤ Module.finrank K L
have inr : ∀ (hy : IsPrimitiveRoot y 0) (hirr : Irreducible (M := K[X]) (cyclotomic (p.lcm 0) K)), φ (p.lcm 0) ≤ Module.finrank K L
Tactic: rcases Nat.eq_zero_or_pos q with (rfl | hqpos)
Cleared hypotheses: q, hy, hirr
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
⊢ φ (p.lcm q) ≤ Module.finrank K L
have inr₁ : ∀ (hqpos : q > 0), φ (p.lcm q) ≤ Module.finrank K L
Tactic: rcases Nat.eq_zero_or_pos q with (rfl | hqpos)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
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
hqpos : q > 0
z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)
k : ℕ+ := PNat.lcm (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p hppos) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) q hqpos)
⊢ φ (p.lcm q) ≤ Module.finrank K L
have this : IsPrimitiveRoot z (↑k : ℕ)
Tactic: have : IsPrimitiveRoot z k := hx.pow_mul_pow_lcm hy hppos.ne' hqpos.ne'
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
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
hqpos : q > 0
z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)
k : ℕ+ := PNat.lcm (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p hppos) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) q hqpos)
this : IsPrimitiveRoot z (↑k : ℕ)
⊢ φ (p.lcm q) ≤ Module.finrank K L
have this₁ : IsCyclotomicExtension.{u, v} {(↑k : ℕ)} K ↥K[z]
Tactic: haveI := IsPrimitiveRoot.adjoin_isCyclotomicExtension K this
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
hqpos : q > 0
z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)
k : ℕ+ := PNat.lcm (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p hppos) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) q hqpos)
this_1 : IsPrimitiveRoot z (↑k : ℕ)
this : IsCyclotomicExtension.{u, v} {(↑k : ℕ)} K ↥K[z]
⊢ φ (p.lcm q) ≤ Module.finrank K L
have h : φ (p.lcm q) =
  Module.finrank.{u, v} K ↥((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) K[z] : Submodule K L)
Tactic: convert! Submodule.finrank_le (Subalgebra.toSubmodule (adjoin K { z }))
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
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
hqpos : q > 0
z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)
k : ℕ+ := PNat.lcm (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p hppos) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) q hqpos)
this_1 : IsPrimitiveRoot z (↑k : ℕ)
this : IsCyclotomicExtension.{u, v} {(↑k : ℕ)} K ↥K[z]
⊢ φ (p.lcm q) =
    Module.finrank.{u, v} K ↥((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) K[z] : Submodule K L)
have hirr₁ : Irreducible (M := K[X]) (cyclotomic (↑k : ℕ) K)
Tactic: rw [show Nat.lcm p q = (k : ℕ) from rfl] at hirr
Cleared hypotheses: hirr, this_1, this
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl : l ≠ 0
⊢ l ∣ 2 * n
have hl₁ : NeZero l
Tactic: have hl : NeZero l := ⟨hl⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
⊢ l ∣ 2 * n
have hroot : IsPrimitiveRoot (zeta n ℚ K) n
Tactic: have hroot := IsCyclotomicExtension.zeta_spec n ℚ K