fix

Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

@@ -226,7 +226,7 @@ theorem discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical :
     letI s := {I : Ideal R | I.IsMaximal}
     DiscreteTopology (PrimeSpectrum R) ↔ Finite s ∧ sInf s ≤ nilradical R :=
   discreteTopology_iff_finite_and_isPrime_imp_isMaximal.trans <| by
-    simp_rw [(equivSetOfIsPrime R).finite_iff, Set.finite_coe_iff]
+    rw [(equivSetOfIsPrime R).finite_iff, ← Set.coe_setOf, Set.finite_coe_iff, Set.finite_coe_iff]
     refine ⟨fun h ↦ ⟨h.1.subset fun _ h ↦ h.isPrime, nilradical_eq_sInf R ▸ sInf_le_sInf h.2⟩,
       fun ⟨fin, le⟩ ↦ ?_⟩
     have hpm (I : Ideal R) (hI : I.IsPrime): I.IsMaximal := by

Mathlib/RingTheory/PrimeSpectrum.lean

@@ -85,9 +85,9 @@ variable (R S)
 
 /-- The prime spectrum is in bijection with the set of prime ideals. -/
 @[simps]
-def equivSetOfIsPrime : PrimeSpectrum R ≃ {I : Ideal R | I.IsPrime} where
-  toFun I := ⟨I.1, I.2⟩
-  invFun I := ⟨I.1, I.2⟩
+def equivSetOfIsPrime : PrimeSpectrum R ≃ {I : Ideal R // I.IsPrime} where
+  toFun I := ⟨I.asIdeal, I.2⟩
+  invFun I := ⟨I, I.2⟩
   left_inv _ := rfl
   right_inv _ := rfl