[GOAL]
⊢ IsPrincipalIdealRing { x // x ∈ 𝓞 ℚ }
[PROOFSTEP]
convert
  IsPrincipalIdealRing.of_surjective (Rat.ringOfIntegersEquiv.symm : ℤ →+* ringOfIntegers ℚ)
    Rat.ringOfIntegersEquiv.symm.surjective
