no goals
R : Type u_2
inst✝⁶ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
P : Type ?u.46855
inst✝³ : CommSemiring P
A : Type ?u.46861
inst✝² : CommRing A
inst✝¹ : IsDomain A
I : Ideal R
hI : Ideal.IsPrime I
inst✝ : IsLocalization.AtPrime S I
x : R
h : optParam (LocalRing S) (_ : LocalRing S)
⊢ ¬↑(algebraMap R S) x ∈ LocalRing.maximalIdeal S ↔ ¬x ∈ I
simpa only [LocalRing.mem_maximalIdeal, mem_nonunits_iff, Classical.not_not] using
  isUnit_to_map_iff S I x