/-- **Euclid's lemma in a principal ideal domain**: irreducible elements are prime. Let `p` be
irreducible with `p ∣ a * b` and `p ∤ a`. The ideal `(p, a)` is principal, say `(d)`. From
`p = d * x`, either `x` is a unit — then `(d) = (p)` contains `a`, so `p ∣ a`, impossible — or `d`
is a unit, so `(p, a)` is everything: `1 = r * p + s * a`. Then `b = r * p * b + s * (a * b)` is
divisible by `p`. -/
theorem pid_irreducible_prime {R : Type*} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R]
{p : R} (hp : Irreducible p) : Prime p := by
refine ⟨hp.ne_zero, hp.not_isUnit, fun a b hab => ?_⟩
by_cases hpa : p ∣ a
· exact Or.inl hpa
right
obtain ⟨d, hd⟩ := (IsPrincipalIdealRing.principal (Ideal.span {p, a})).principal
have hd' : Ideal.span {p, a} = Ideal.span {d} := hd
have hpd : p ∈ Ideal.span {d} := by rw [← hd']; exact Ideal.subset_span (by simp)
have had : a ∈ Ideal.span {d} := by rw [← hd']; exact Ideal.subset_span (by simp)
obtain ⟨x, hx⟩ := Ideal.mem_span_singleton'.mp hpd
have hpdx : p = d * x := by rw [← hx, mul_comm]
rcases hp.isUnit_or_isUnit hpdx with hdu | hxu
· -- `d` is a unit, so `1 ∈ (p, a)`.
have h1 : (1 : R) ∈ Ideal.span {p, a} := by
rw [hd', eq_top_of_unit_mem _ hdu (Ideal.mem_span_singleton_self d)]
exact Submodule.mem_top
obtain ⟨r, s, hrs⟩ := Ideal.mem_span_pair.mp h1
obtain ⟨c, hc⟩ := hab
exact ⟨r * b + s * c, by
calc b = (r * p + s * a) * b := by rw [hrs, one_mul]
_ = p * (r * b + s * c) := by rw [add_mul, mul_assoc s, hc]; ring⟩
· -- `x` is a unit, so `d` divides `p` and `p` divides `d ∣ a`: contradiction.
exfalso
apply hpa
obtain ⟨y, hy⟩ := Ideal.mem_span_singleton'.mp had
obtain ⟨u, rfl⟩ := hxu
exact ⟨y * ↑u⁻¹, by rw [← hy, ← hx]; linear_combination (-(y * d)) * Units.mul_inv u⟩