∀ {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] {x : R} {y : ↥M} {z : S},
  (z = IsLocalization.mk' S x y) = (z * (algebraMap R S) ↑y = (algebraMap R S) x)