case h.e'_3
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type ?u.79647
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type ?u.79827
inst✝ : CommSemiring P
I : Ideal R
hI : Ideal.IsPrime I
⊢ LocalRing.maximalIdeal (Localization (Ideal.primeCompl I)) =
    Ideal.map (algebraMap R (Localization.AtPrime I))
      (Ideal.comap (algebraMap R (Localization.AtPrime I)) (LocalRing.maximalIdeal (Localization (Ideal.primeCompl I))))
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type ?u.79647
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type ?u.79827
inst✝ : CommSemiring P
I : Ideal R
hI : Ideal.IsPrime I
⊢ Ideal.map (algebraMap R (Localization.AtPrime I)) I = LocalRing.maximalIdeal (Localization (Ideal.primeCompl I))
convert congr_arg (Ideal.map (algebraMap R (Localization.AtPrime I)))
(AtPrime.comap_maximalIdeal (hI := hI)).symm
no goals
case h.e'_3
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type ?u.79647
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type ?u.79827
inst✝ : CommSemiring P
I : Ideal R
hI : Ideal.IsPrime I
⊢ LocalRing.maximalIdeal (Localization (Ideal.primeCompl I)) =
    Ideal.map (algebraMap R (Localization.AtPrime I))
      (Ideal.comap (algebraMap R (Localization.AtPrime I)) (LocalRing.maximalIdeal (Localization (Ideal.primeCompl I))))
rw [map_comap I.primeCompl]