∀ {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],
  Algebra.Generators.localizationAway S r =
    { val := fun x => IsLocalization.Away.invSelf r,
      σ' := fun s =>
        MvPolynomial.C (IsLocalization.Away.sec r s).1 * MvPolynomial.X () ^ (IsLocalization.Away.sec r s).2,
      aeval_val_σ' := ⋯, algebraMap_eq := ⋯ }