Prime avoidance in Lean with a non-prime ideal: Option-indexed family for subset_union_prime

Mathlib's Ideal.subset_union_prime (a b : ι) allows two members of the family to be non-prime, but they must come from the same indexing function f : ι → Ideal R. To avoid a non-prime ideal S together with finitely many primes q (e.g. to find π ∈ p with ord_p π = 1 and π ∉ other height-one primes), index by Option: f := fun i => i.elim S Subtype.val, s := insert none ((univ.filter (· ≠ p)).map Function.Embedding.some), and pass a = b = none; the primality side goal is discharged by Option.ne_none_iff_exists'. For the 'order < 2' condition use S := (span {(algebraMap R R_p t)^2}).comap (algebraMap R R_p) with t a uniformizer, which is an ideal without any symbolic-power API. Use: a Krull domain with finitely many height-one primes is a PID (IsPrincipalIdealRing.of_prime_ne_bot).