∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (y : R) [inst_2 : Algebra R S]
  [IsLocalization.Away y S] [IsJacobsonRing R] (I : Ideal R),
  I.IsMaximal → y ∉ I → (Ideal.map (algebraMap R S) I).IsMaximal