diff --git a/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean b/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
index 522e86af0016b4..a2b234c7a502c2 100644
--- a/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
@@ -467,6 +467,9 @@ instance isMaximal : v.asIdeal.IsMaximal := v.isPrime.isMaximal v.ne_bot
 
 theorem prime : Prime v.asIdeal := Ideal.prime_of_isPrime v.ne_bot v.isPrime
 
+instance : Coe (HeightOneSpectrum R) (Ideal R) where
+  coe P := P.asIdeal
+
 /--
 The (nonzero) prime elements of the monoid with zero `Ideal R` correspond
 to an element of type `HeightOneSpectrum R`.
diff --git a/Mathlib/RingTheory/Spectrum/Maximal/Defs.lean b/Mathlib/RingTheory/Spectrum/Maximal/Defs.lean
index 2cb491971a093e..0b276f45c56ae2 100644
--- a/Mathlib/RingTheory/Spectrum/Maximal/Defs.lean
+++ b/Mathlib/RingTheory/Spectrum/Maximal/Defs.lean
@@ -29,3 +29,6 @@ structure MaximalSpectrum (R : Type*) [CommSemiring R] where
   isMaximal : asIdeal.IsMaximal
 
 attribute [instance] MaximalSpectrum.isMaximal
+
+instance (R : Type*) [CommSemiring R] : Coe (MaximalSpectrum R) (Ideal R) where
+  coe P := P.asIdeal
diff --git a/Mathlib/RingTheory/Spectrum/Prime/Defs.lean b/Mathlib/RingTheory/Spectrum/Prime/Defs.lean
index 04f5f93f11f5bf..a8fca85db59474 100644
--- a/Mathlib/RingTheory/Spectrum/Prime/Defs.lean
+++ b/Mathlib/RingTheory/Spectrum/Prime/Defs.lean
@@ -49,6 +49,9 @@ See the corresponding section at `Mathlib/RingTheory/Spectrum/Prime/Topology.lea
 
 variable {R : Type*} [CommSemiring R]
 
+instance : Coe (PrimeSpectrum R) (Ideal R) where
+  coe P := P.asIdeal
+
 instance : PartialOrder (PrimeSpectrum R) :=
   PartialOrder.lift asIdeal (@PrimeSpectrum.ext _ _)