theorem Ideal.exists_coprime_mul_principal {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (I I' : Ideal A) (hI : I ≠ ⊥) (hI' : I' ≠ ⊥) : ∃ (J : Ideal A), J ⊔ I' = ⊤ ∧ Submodule.IsPrincipal (I * J)

theorem ClassGroup.exists_mk0_coprime {A : Type u_1} [CommRing A] [IsDomain A] [IsDedekindDomain A] (c : ClassGroup A) (𝔞 : Ideal A) (h𝔞 : 𝔞 ≠ ⊥) : ∃ (K : Ideal A) (hK : K ≠ ⊥), mk0 ⟨K, ⋯⟩ = c ∧ K ⊔ 𝔞 = ⊤