∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {P : Type u_3}
  [inst_3 : CommSemiring P] (x : R) [inst_4 : IsLocalization.Away x S] (y : R) [inst_5 : Algebra R P]
  [inst_6 : IsLocalization.Away (y * x) P] (a : R),
  (IsLocalization.Away.awayToAwayLeft x y) ((algebraMap R S) a) = (algebraMap R P) a