rw [← minpoly.isIntegrallyClosed_eq_field_fractions ℚ (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ),
  ← cyclotomic_eq_minpoly_rat (n := p), map_cyclotomic]
case a
p : ℕ
hpri : Fact p.Prime
x : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hx : IsPrimitiveRoot (↑x) p
⊢ map (algebraMap ℤ ℚ) (minpoly ℤ x) = map (algebraMap ℤ ℚ) (cyclotomic p ℤ)
case a.h
p : ℕ
hpri : Fact p.Prime
x : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hx : IsPrimitiveRoot (↑x) p
⊢ IsPrimitiveRoot ((algebraMap (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) (CyclotomicField ⟨p, ⋯⟩ ℚ)) x) p

case a.hpos
p : ℕ
hpri : Fact p.Prime
x : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hx : IsPrimitiveRoot (↑x) p
⊢ 0 < p

case a
p : ℕ
hpri : Fact p.Prime
x : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hx : IsPrimitiveRoot (↑x) p
⊢ IsIntegral ℤ x