-- 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 :
  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
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
mk₆ mk₇ mk₈ mk₉ :
  Eq.{u_1 + 1} (α := C)
    ((aeval
            (↑(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) :
          (a : K[X]) → C)
        (minpoly K ζ) :
      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:
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]

Premises used: Algebra.algebraMap, 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