simp only [ne_eq, Ideal.span_singleton_eq_top]
case hI
p✝ : ℕ
hpri : Fact p✝.Prime
p : ℕ
hp : p ≠ 0
⊢ Ideal.span {cyclotomic p ℤ} ≠ ⊤
case hI
p✝ : ℕ
hpri : Fact p✝.Prime
p : ℕ
hp : p ≠ 0
⊢ ¬IsUnit (cyclotomic p ℤ)