rw [← Ideal.mem_span_singleton (y := x), ← eq_intCast (algebraMap ℤ R), ← Ideal.mem_comap,
  ← Ideal.span_singleton_absNorm, Ideal.mem_span_singleton, Ideal.absNorm_span_singleton,
  Int.natAbs_dvd]
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Infinite R
inst✝¹ : Module.Free ℤ R
inst✝ : Module.Finite ℤ R
x : R
hx : Prime ((Algebra.norm ℤ) x)
y : ℤ
⊢ (Algebra.norm ℤ) x ∣ y ↔ x ∣ ↑y
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Infinite R
inst✝¹ : Module.Free ℤ R
inst✝ : Module.Finite ℤ R
x : R
hx : Prime ((Algebra.norm ℤ) x)
y : ℤ
⊢ (Ideal.absNorm (Ideal.span {x})).Prime