-- 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
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
⊢ (↑(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₆ : 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)
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]