∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R] (s : Submonoid R) {a : R},
  a ≠ 0 → (∀ b ∈ PrincipalIdealRing.factors a, b ∈ s) → (∀ (c : Rˣ), ↑c ∈ s) → a ∈ s