simp only [RingEquiv.toMulEquiv_eq_coe, RingEquiv.coe_toMulEquiv,
  (equiv p).map_sub, (equiv p).map_one, equiv_zeta]
p : ℕ
hpri : Fact p.Prime
⊢ Prime ((equiv p).toMulEquiv (zeta p - 1))
p : ℕ
hpri : Fact p.Prime
⊢ Prime (⋯.toInteger - 1)