∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S],
  (∀ m ∈ M, IsRegular m) → ∀ {r : R} {m : ↥M}, IsRegular (IsLocalization.mk' S r m) = IsRegular r