no goals
R : Type u
inst✝ : CommRing R
x✝¹ x✝ : MaximalSpectrum R
asIdeal✝¹ : Ideal R
IsMaximal✝¹ : Ideal.IsMaximal asIdeal✝¹
asIdeal✝ : Ideal R
IsMaximal✝ : Ideal.IsMaximal asIdeal✝
h :
  toPrimeSpectrum { asIdeal := asIdeal✝¹, IsMaximal := IsMaximal✝¹ } =
    toPrimeSpectrum { asIdeal := asIdeal✝, IsMaximal := IsMaximal✝ }
⊢ { asIdeal := asIdeal✝¹, IsMaximal := IsMaximal✝¹ } = { asIdeal := asIdeal✝, IsMaximal := IsMaximal✝ }
simpa only [MaximalSpectrum.mk.injEq] using (PrimeSpectrum.ext_iff _ _).mp h