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.70150
inst✝³ : CommSemiring P
A : Type ?u.70156
inst✝² : CommRing A
inst✝¹ : IsDomain A
I : Ideal R
hI : Ideal.IsPrime I
inst✝ : IsLocalization.AtPrime S I
h : optParam (LocalRing S) (_ : LocalRing S)
x : R
⊢ x ∈ Ideal.comap (algebraMap R S) (LocalRing.maximalIdeal S) ↔ x ∈ I
simpa only [Ideal.mem_comap] using to_map_mem_maximal_iff _ I x