∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (x : R)
  [inst_3 : IsLocalization.Away x S] (s : S), Associated ((algebraMap R S) (IsLocalization.Away.sec x s).1) s