theorem Finset.prod_ideal_ne_bot {A : Type u_1} [CommRing A] [IsDomain A] {ι : Type u_2} (s : Finset ι) (f : ι → Ideal A) (hf : ∀ i ∈ s, f i ≠ ⊥) : ∏ i ∈ s, f i ≠ ⊥

theorem Ideal.exists_elem_eq_valuation_at_primes {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] {ι : Type u_2} (s : Finset ι) (ps : ι → IsDedekindDomain.HeightOneSpectrum A) (I : Ideal A) (hI : I ≠ ⊥) : ∃ x ∈ I, x ≠ 0 ∧ ∀ i ∈ s, have e := Multiset.count (normalize (ps i).asIdeal) (UniqueFactorizationMonoid.normalizedFactors I); x ∈ (ps i).asIdeal ^ e ∧ x ∉ (ps i).asIdeal ^ (e + 1)