∀ {R : Type u} (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [inst_3 : IsLocalization.Away r S] (x : Unit),
  (Algebra.Generators.localizationAway S r).val x = IsLocalization.Away.invSelf r