awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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)
⊢ 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)
have a₁ : eval (zeta n A B) (cyclotomic n B) = 0 ↔ eval₂ (algebraMap A B) (zeta n A B) (cyclotomic n A) = 0
Tactic: rw [IsRoot.def, aeval_def, eval₂_eq_eval_map, map_cyclotomic]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
⊢ 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)
have a₂ : eval (zeta n A B) (cyclotomic n B) = 0 ↔ eval (zeta n A B) (Polynomial.map (algebraMap A B) (cyclotomic n A)) = 0
Tactic: rw [IsRoot.def, aeval_def, eval₂_eq_eval_map, map_cyclotomic]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
⊢ 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)
have a₃ : eval (zeta n A B) (cyclotomic n B) = 0 ↔ eval (zeta n A B) (cyclotomic n B) = 0
Tactic: rw [IsRoot.def, aeval_def, eval₂_eq_eval_map, map_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
ζ : L
hζ : IsPrimitiveRoot ζ n
⊢ Membership.mem (γ := Subalgebra K L) K[ζ - 1] (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))
have rw : ∃ (x : K[X]), (aeval (ζ - 1) : (a : K[X]) → L) x = ζ
Tactic: rw [powerBasis_gen, adjoin_singleton_eq_range_aeval, AlgHom.mem_range]
-- 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 : 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
⊢ PowerBasis K L
have apply : Eq (α := Subalgebra K L) K[ζ - 1] ⊤
Tactic: apply PowerBasis.ofAdjoinEqTop (((integral {n} K L).isIntegral ζ).sub isIntegral_one)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
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) }
⊢ ↥(primitiveRoots n C)
have this : NeZero.{u} (R := K) (↑n : K)
Tactic: haveI := IsCyclotomicExtension.neZero' n K L
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
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)
⊢ ↥(primitiveRoots n C)
have hn : NeZero.{u_1} (R := C) (↑n : C)
Tactic: haveI hn := NeZero.of_faithfulSMul K C n
-- 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)
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)
⊢ ↥(primitiveRoots n C)
have refine : (↑x : C) ∈ primitiveRoots n C
Tactic: refine ⟨x.1, ?_⟩
-- 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)
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)
⊢ (↑x : C) ∈ primitiveRoots n C
have 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
Tactic: cases x
Cleared hypotheses: x
-- 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 :
  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
have mk : IsPrimitiveRoot
  (↑(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)
  n
Tactic: rwa [mem_primitiveRoots (NeZero.pos _), ← isRoot_cyclotomic_iff, IsRoot.def,
          ← map_cyclotomic _ (algebraMap K C), hζ.minpoly_eq_cyclotomic_of_irreducible hirr,
          ← eval₂_eq_eval_map, ← aeval_def]
-- 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 :
  Eq.{u_1 + 1} (α := C)
    ((aeval val : (a : K[X]) → C) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))) : C) (0 : C)
mk :
  IsPrimitiveRoot
    (↑(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)
    n
⊢ (↑(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
have mk₁ : IsRoot (cyclotomic n 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)
Tactic: rwa [mem_primitiveRoots (NeZero.pos _), ← isRoot_cyclotomic_iff, IsRoot.def,
          ← map_cyclotomic _ (algebraMap K C), hζ.minpoly_eq_cyclotomic_of_irreducible hirr,
          ← eval₂_eq_eval_map, ← aeval_def]
-- 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 :
  Eq.{u_1 + 1} (α := C)
    ((aeval val : (a : K[X]) → C) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))) : C) (0 : C)
mk :
  IsPrimitiveRoot
    (↑(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)
    n
mk₁ :
  IsRoot (cyclotomic n 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)
⊢ (↑(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
have mk₂ : eval
    (↑(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)
    (cyclotomic n C) =
  0
Tactic: rwa [mem_primitiveRoots (NeZero.pos _), ← isRoot_cyclotomic_iff, IsRoot.def,
          ← map_cyclotomic _ (algebraMap K C), hζ.minpoly_eq_cyclotomic_of_irreducible hirr,
          ← eval₂_eq_eval_map, ← aeval_def]
-- 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 :
  Eq.{u_1 + 1} (α := C)
    ((aeval val : (a : K[X]) → C) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))) : C) (0 : C)
mk :
  IsPrimitiveRoot
    (↑(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)
    n
mk₁ :
  IsRoot (cyclotomic n 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)
mk₂ :
  eval
      (↑(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)
      (cyclotomic n C) =
    0
⊢ (↑(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
have mk₃ : eval
    (↑(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)
    (Polynomial.map (algebraMap K C : K →+* C) (cyclotomic n K)) =
  0
Tactic: rwa [mem_primitiveRoots (NeZero.pos _), ← isRoot_cyclotomic_iff, IsRoot.def,
          ← map_cyclotomic _ (algebraMap K C), hζ.minpoly_eq_cyclotomic_of_irreducible hirr,
          ← eval₂_eq_eval_map, ← aeval_def]
-- 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 :
  Eq.{u_1 + 1} (α := C)
    ((aeval val : (a : K[X]) → C) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))) : C) (0 : C)
mk :
  IsPrimitiveRoot
    (↑(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)
    n
mk₁ :
  IsRoot (cyclotomic n 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)
mk₂ :
  eval
      (↑(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)
      (cyclotomic n C) =
    0
mk₃ :
  eval
      (↑(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)
      (Polynomial.map (algebraMap K C : K →+* C) (cyclotomic n K)) =
    0
⊢ (↑(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
have mk₄ : eval
    (↑(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)
    (Polynomial.map (algebraMap K C) (minpoly K ζ)) =
  0
Tactic: rwa [mem_primitiveRoots (NeZero.pos _), ← isRoot_cyclotomic_iff, IsRoot.def,
          ← map_cyclotomic _ (algebraMap K C), hζ.minpoly_eq_cyclotomic_of_irreducible hirr,
          ← eval₂_eq_eval_map, ← aeval_def]
-- 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 :
  Eq.{u_1 + 1} (α := C)
    ((aeval val : (a : K[X]) → C) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))) : C) (0 : C)
mk :
  IsPrimitiveRoot
    (↑(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)
    n
mk₁ :
  IsRoot (cyclotomic n 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)
mk₂ :
  eval
      (↑(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)
      (cyclotomic n C) =
    0
mk₃ :
  eval
      (↑(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)
      (Polynomial.map (algebraMap K C : K →+* C) (cyclotomic n K)) =
    0
mk₄ :
  eval
      (↑(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)
      (Polynomial.map (algebraMap K C) (minpoly K ζ)) =
    0
⊢ (↑(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
have mk₅ : eval₂ (algebraMap K 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)
    (minpoly K ζ) =
  0
Tactic: rwa [mem_primitiveRoots (NeZero.pos _), ← isRoot_cyclotomic_iff, IsRoot.def,
          ← map_cyclotomic _ (algebraMap K C), hζ.minpoly_eq_cyclotomic_of_irreducible hirr,
          ← eval₂_eq_eval_map, ← aeval_def]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
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)
⊢ { y : C //
    Eq.{u_1 + 1} (α := C)
      ((aeval y : (a : K[X]) → C) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))) : C) (0 : C) }
have this : NeZero.{u} (R := K) (↑n : K)
Tactic: haveI := IsCyclotomicExtension.neZero' n K L
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
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)
⊢ { y : C //
    Eq.{u_1 + 1} (α := C)
      ((aeval y : (a : K[X]) → C) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))) : C) (0 : C) }
have hn : NeZero.{u_1} (R := C) (↑n : C)
Tactic: haveI hn := NeZero.of_faithfulSMul K C n
-- 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)
x : ↥(primitiveRoots n C)
this : NeZero.{u} (R := K) (↑n : K)
hn : NeZero.{u_1} (R := C) (↑n : 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) }
have refine : Eq.{u_1 + 1} (α := C)
  ((aeval (↑x : C) : (a : K[X]) → C) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))) : C) (0 : C)
Tactic: refine ⟨x.1, ?_⟩
-- 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)
x : ↥(primitiveRoots n C)
this : NeZero.{u} (R := K) (↑n : K)
hn : NeZero.{u_1} (R := C) (↑n : C)
⊢ Eq.{u_1 + 1} (α := C)
    ((aeval (↑x : C) : (a : K[X]) → C) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))) : C) (0 : C)
have 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)
Tactic: cases x
Cleared hypotheses: x