theorem RayClassField.exists_ringOfIntegers_cong_mod_primes {K : Type u} [Field K] [NumberField K] {ι : Type u_1} {s : Finset ι} (P : ι → FinitePlace K) (e : ι → ℕ) (hP_inj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j) (x : ↥s → NumberField.RingOfIntegers K) : ∃ (y : NumberField.RingOfIntegers K), ∀ (i : ι) (hi : i ∈ s), y - x ⟨i, hi⟩ ∈ (P i).asIdeal ^ e i