diff --git a/Mathlib/AlgebraicGeometry/Properties.lean b/Mathlib/AlgebraicGeometry/Properties.lean
index 764b571ba938f5..c37783d7f1fde8 100644
--- a/Mathlib/AlgebraicGeometry/Properties.lean
+++ b/Mathlib/AlgebraicGeometry/Properties.lean
@@ -354,10 +354,9 @@ lemma coheight_eq_of_isOpenImmersion {U X : Scheme} {x : U} (f : U ⟶ X) [IsOpe
 open Order in
 lemma idealHeight_eq_coheight (R : CommRingCat) (x : Spec R) :
     x.asIdeal.height = coheight x := by
-  rw [Ideal.height_eq_primeHeight x.asIdeal, Ideal.primeHeight,
+  rw [PrimeSpectrum.height_eq_orderHeight,
     ← Order.coheight_orderIso (specOrderIsoPrimeSpectrum R), ← height_ofDual,
     specOrderIsoPrimeSpectrum_apply, OrderDual.ofDual_toDual]
-  rfl
 
 open Order in
 @[stacks 02IZ]
diff --git a/Mathlib/RingTheory/Ideal/Height.lean b/Mathlib/RingTheory/Ideal/Height.lean
index 15d71475c438d0..52d06e6ec73e24 100644
--- a/Mathlib/RingTheory/Ideal/Height.lean
+++ b/Mathlib/RingTheory/Ideal/Height.lean
@@ -17,16 +17,12 @@ In this file, we define the height of a prime ideal and the height of an ideal.
 
 ## Main definitions
 
-* `Ideal.primeHeight` : The height of a prime ideal $\mathfrak{p}$. We define it as the supremum of
-  the lengths of strictly decreasing chains of prime ideals below it. This definition is implemented
-  via `Order.height`.
-
 * `Ideal.height` : The height of an ideal. We defined it as the infimum of the `primeHeight` of the
   minimal prime ideals of I.
 
 -/
 
-@[expose] public section
+public section
 
 variable {R : Type*} [CommRing R] (I : Ideal R)
 
@@ -34,7 +30,7 @@ open Ideal
 
 /-- The height of a prime ideal is defined as the supremum of the lengths of strictly decreasing
 chains of prime ideals below it. -/
-noncomputable def Ideal.primeHeight [hI : I.IsPrime] : ℕ∞ :=
+private noncomputable def Ideal.primeHeight [hI : I.IsPrime] : ℕ∞ :=
   Order.height (⟨I, hI⟩ : PrimeSpectrum R)
 
 /-- The height of an ideal is defined as the infimum of the heights of its minimal prime ideals. -/
@@ -42,10 +38,17 @@ noncomputable def Ideal.height : ℕ∞ :=
   ⨅ J ∈ I.minimalPrimes, @Ideal.primeHeight _ _ J ‹J ∈ I.minimalPrimes›.isPrime
 
 /-- For a prime ideal, its height equals its prime height. -/
-lemma Ideal.height_eq_primeHeight [I.IsPrime] : I.height = I.primeHeight := by
-  unfold height primeHeight
-  simp_rw [Ideal.minimalPrimes_eq_subsingleton_self]
-  simp
+private lemma Ideal.height_eq_primeHeight [I.IsPrime] : I.height = I.primeHeight := by
+  simp [height, primeHeight, Ideal.minimalPrimes_eq_subsingleton_self]
+
+lemma PrimeSpectrum.height_eq_orderHeight (p : PrimeSpectrum R) :
+    p.asIdeal.height = Order.height p :=
+  p.asIdeal.height_eq_primeHeight
+
+lemma Ideal.height_eq_inf_minimalPrimes : I.height = ⨅ J ∈ I.minimalPrimes, J.height := by
+  apply iInf_congr (fun p ↦ iInf_congr fun hp ↦ ?_)
+  have := hp.isPrime
+  exact (Ideal.height_eq_primeHeight _).symm
 
 /-- An ideal has finite height if it is either the unit ideal or its height is finite.
 We include the unit ideal in order to have the instance `IsNoetherianRing R → FiniteHeight I`. -/
@@ -65,12 +68,22 @@ lemma Ideal.height_lt_top {I : Ideal R} (hI : I ≠ ⊤) [I.FiniteHeight] :
     I.height < ⊤ :=
   (Ideal.height_ne_top hI).lt_top
 
-lemma Ideal.primeHeight_ne_top (I : Ideal R) [I.FiniteHeight] [I.IsPrime] :
+lemma Ideal.height_ne_top_of_isPrime {I : Ideal R} [I.FiniteHeight] [I.IsPrime] :
+    I.height ≠ ⊤ :=
+  Ideal.height_ne_top ‹I.IsPrime›.ne_top
+
+@[deprecated "Use `Ideal.height_ne_top_of_isPrime` instead." (since := "2026-04-04")]
+private lemma Ideal.primeHeight_ne_top (I : Ideal R) [I.FiniteHeight] [I.IsPrime] :
     I.primeHeight ≠ ⊤ := by
   rw [← I.height_eq_primeHeight]
   exact Ideal.height_ne_top ‹I.IsPrime›.ne_top
 
-lemma Ideal.primeHeight_lt_top (I : Ideal R) [I.FiniteHeight] [I.IsPrime] :
+lemma Ideal.height_lt_top_of_isPrime {I : Ideal R} [I.FiniteHeight] [I.IsPrime] :
+    I.height < ⊤ :=
+  Ideal.height_lt_top ‹I.IsPrime›.ne_top
+
+@[deprecated "Use `Ideal.height_lt_top_of_isPrime` instead." (since := "2026-04-04")]
+private lemma Ideal.primeHeight_lt_top (I : Ideal R) [I.FiniteHeight] [I.IsPrime] :
     I.primeHeight < ⊤ := by
   rw [← I.height_eq_primeHeight]
   exact Ideal.height_lt_top ‹I.IsPrime›.ne_top
@@ -85,69 +98,88 @@ lemma Ideal.exists_ltSeries_length_eq_height (p : Ideal R) [p.IsPrime] [p.Finite
   rw [hn]
   exact ⟨l, last, by rw [len, WithTop.some_eq_coe, ENat.some_eq_coe]⟩
 
-@[gcongr]
-lemma Ideal.primeHeight_mono {I J : Ideal R} [I.IsPrime] [J.IsPrime] (h : I ≤ J) :
-    I.primeHeight ≤ J.primeHeight := by
-  unfold primeHeight
+private lemma Ideal.height_mono_of_isPrime {I J : Ideal R} [I.IsPrime] [J.IsPrime] (h : I ≤ J) :
+    I.height ≤ J.height := by
+  simp only [Ideal.height_eq_primeHeight, Ideal.primeHeight]
   gcongr
   exact h
 
-lemma Ideal.primeHeight_add_one_le_of_lt {I J : Ideal R} [I.IsPrime] [J.IsPrime] (h : I < J) :
-    I.primeHeight + 1 ≤ J.primeHeight := by
-  unfold primeHeight
+@[deprecated "Use `Ideal.height_mono_of_isPrime` instead." (since := "2026-04-04")]
+private lemma Ideal.primeHeight_mono {I J : Ideal R} [I.IsPrime] [J.IsPrime] (h : I ≤ J) :
+    I.primeHeight ≤ J.primeHeight := by
+  simpa [Ideal.height_eq_primeHeight] using Ideal.height_mono_of_isPrime h
+
+lemma Ideal.height_add_one_le_of_lt_of_isPrime {I J : Ideal R} [I.IsPrime] [J.IsPrime] (h : I < J) :
+    I.height + 1 ≤ J.height := by
+  simp only [Ideal.height_eq_primeHeight, Ideal.primeHeight]
   exact Order.height_add_one_le h
 
+@[deprecated "Use `Ideal.height_add_one_le_of_lt_of_isPrime` instead." (since := "2026-04-04")]
+private lemma Ideal.primeHeight_add_one_le_of_lt {I J : Ideal R} [I.IsPrime] [J.IsPrime]
+    (h : I < J) : I.primeHeight + 1 ≤ J.primeHeight := by
+  simpa [Ideal.height_eq_primeHeight] using Ideal.height_add_one_le_of_lt_of_isPrime h
+
 @[simp]
 theorem Ideal.height_top : (⊤ : Ideal R).height = ⊤ := by
   simp [height, minimalPrimes_top]
 
-@[gcongr]
-lemma Ideal.primeHeight_strict_mono {I J : Ideal R} [I.IsPrime] [J.IsPrime]
-    (h : I < J) [J.FiniteHeight] :
-    I.primeHeight < J.primeHeight := by
-  rw [primeHeight]
-  have : I.FiniteHeight := by
-    rw [Ideal.finiteHeight_iff, ← lt_top_iff_ne_top, Ideal.height_eq_primeHeight]
-    right
-    exact lt_of_le_of_lt (Ideal.primeHeight_mono h.le) (Ideal.primeHeight_lt_top J)
-  exact Order.height_strictMono h (Ideal.primeHeight_lt_top _)
-
 @[gcongr]
 theorem Ideal.height_mono {I J : Ideal R} (h : I ≤ J) : I.height ≤ J.height := by
-  simp only [height]
+  simp only [I.height_eq_inf_minimalPrimes, J.height_eq_inf_minimalPrimes]
   refine le_iInf₂ (fun p hp ↦ ?_)
   have := hp.isPrime
   obtain ⟨q, hq, e⟩ := Ideal.exists_minimalPrimes_le (h.trans hp.le)
-  haveI := hq.isPrime
-  exact (iInf₂_le q hq).trans (Ideal.primeHeight_mono e)
+  have := hq.isPrime
+  exact (iInf₂_le q hq).trans (Ideal.height_mono_of_isPrime e)
 
 @[gcongr]
-lemma Ideal.height_strict_mono_of_is_prime {I J : Ideal R} [I.IsPrime]
+lemma Ideal.height_strict_mono_of_isPrime {I J : Ideal R} [I.IsPrime]
     (h : I < J) [I.FiniteHeight] : I.height < J.height := by
-  rw [Ideal.height_eq_primeHeight I]
   by_cases hJ : J = ⊤
-  · rw [hJ, height_top]
-    exact I.primeHeight_lt_top
-  · rw [← ENat.add_one_le_iff I.primeHeight_ne_top, Ideal.height]
+  · grw [hJ, height_top]
+    exact I.height_lt_top IsPrime.ne_top'
+  · rw [← ENat.add_one_le_iff (I.height_ne_top IsPrime.ne_top'), J.height_eq_inf_minimalPrimes]
     refine le_iInf₂ (fun K hK ↦ ?_)
     have := hK.isPrime
-    exact Ideal.primeHeight_add_one_le_of_lt (lt_of_lt_of_le h hK.le)
+    have : I < K := lt_of_lt_of_le h hK.le
+    exact Ideal.height_add_one_le_of_lt_of_isPrime this
+
+lemma Ideal.height_strict_mono_of_isPrime_of_isPrime {I J : Ideal R} [I.IsPrime] [J.IsPrime]
+    (h : I < J) [J.FiniteHeight] : I.height < J.height := by
+  have : I.FiniteHeight := I.finiteHeight_iff.mpr
+    (Or.inr (lt_of_le_of_lt (Ideal.height_mono h.le) (J.height_lt_top IsPrime.ne_top')).ne)
+  exact Ideal.height_strict_mono_of_isPrime h
+
+@[deprecated (since := "2026-04-02")]
+alias Ideal.height_strict_mono_of_isPrime_of_is_prime :=
+  Ideal.height_strict_mono_of_isPrime_of_isPrime
+
+@[deprecated "Use `Ideal.height_strict_mono_of_isPrime_of_isPrime` instead."
+  (since := "2026-04-02")]
+private lemma Ideal.primeHeight_strict_mono {I J : Ideal R} [I.IsPrime] [J.IsPrime] (h : I < J)
+    [J.FiniteHeight] : I.primeHeight < J.primeHeight := by
+  simpa [← Ideal.height_eq_primeHeight] using Ideal.height_strict_mono_of_isPrime_of_isPrime h
+
+lemma Ideal.height_le_ringKrullDim_of_isPrime {I : Ideal R} [I.IsPrime] :
+    I.height ≤ ringKrullDim R := by
+  rw [Ideal.height_eq_primeHeight, Ideal.primeHeight]
+  exact Order.height_le_krullDim _
 
 /-- A prime ideal of finite height is equal to any ideal that contains it with no greater height. -/
 lemma Ideal.eq_of_le_of_height_le [I.IsPrime] [I.FiniteHeight]
     {J : Ideal R} (h : I ≤ J) (h_height : J.height ≤ I.height) : I = J :=
-  eq_of_le_of_not_lt h fun hlt => not_le.mpr (Ideal.height_strict_mono_of_is_prime hlt) h_height
+  eq_of_le_of_not_lt h fun hlt => not_le.mpr (Ideal.height_strict_mono_of_isPrime hlt) h_height
 
-lemma Ideal.primeHeight_le_ringKrullDim {I : Ideal R} [I.IsPrime] :
+@[deprecated "Use `Ideal.height_le_ringKrullDim_of_isPrime` instead." (since := "2026-04-04")]
+private lemma Ideal.primeHeight_le_ringKrullDim {I : Ideal R} [I.IsPrime] :
     I.primeHeight ≤ ringKrullDim R := Order.height_le_krullDim _
 
 lemma Ideal.height_le_ringKrullDim_of_ne_top {I : Ideal R} (h : I ≠ ⊤) :
     I.height ≤ ringKrullDim R := by
-  rw [Ideal.height]
   obtain ⟨P, hP⟩ : Nonempty (I.minimalPrimes) := Ideal.nonempty_minimalPrimes h
+  rw [I.height_eq_inf_minimalPrimes]
   have := hP.isPrime
-  refine le_trans ?_ (Ideal.primeHeight_le_ringKrullDim (I := P))
-  simpa using iInf₂_le _ hP
+  refine (WithBot.coe_le_coe.mpr (iInf₂_le _ hP)).trans P.height_le_ringKrullDim_of_isPrime
 
 /-- If `R` has finite Krull dimension, there exists a maximal ideal `m` with `ht m = dim R`. -/
 lemma Ideal.exists_isMaximal_height [FiniteRingKrullDim R] :
@@ -164,17 +196,13 @@ lemma Ideal.exists_isMaximal_height [FiniteRingKrullDim R] :
 instance (priority := 900) Ideal.finiteHeight_of_finiteRingKrullDim {I : Ideal R}
     [FiniteRingKrullDim R] : I.FiniteHeight := by
   rw [finiteHeight_iff, or_iff_not_imp_left, ← lt_top_iff_ne_top, ← WithBot.coe_lt_coe]
-  intro h
-  have h1 := ringKrullDim_lt_top (R := R)
-  have h2 := Ideal.height_le_ringKrullDim_of_ne_top h
-  exact lt_of_le_of_lt h2 h1
+  exact fun h ↦ lt_of_le_of_lt (Ideal.height_le_ringKrullDim_of_ne_top h) ringKrullDim_lt_top
 
 /-- If J has finite height and I ≤ J, then I has finite height -/
 lemma Ideal.finiteHeight_of_le {I J : Ideal R} (e : I ≤ J) (hJ : J ≠ ⊤) [FiniteHeight J] :
     FiniteHeight I where
-  eq_top_or_height_ne_top := Or.inr <| by
-    rw [← lt_top_iff_ne_top]
-    exact (height_mono e).trans_lt (height_lt_top hJ)
+  eq_top_or_height_ne_top := Or.inr <|
+    lt_top_iff_ne_top.mp ((height_mono e).trans_lt (height_lt_top hJ))
 
 /-- If J is a prime ideal containing I, and its height is less than or equal to the height of I,
 then J is a minimal prime over I -/
@@ -185,27 +213,29 @@ lemma Ideal.mem_minimalPrimes_of_height_eq {I J : Ideal R} (e : I ≤ J) [J.IsPr
   refine (eq_of_le_of_not_lt h₂ fun h₃ ↦ ?_).symm
   have := h₁.isPrime
   have := finiteHeight_of_le h₂ IsPrime.ne_top'
-  exact lt_irrefl _ ((height_strict_mono_of_is_prime h₃).trans_le (e'.trans <| height_mono h₁.le))
+  exact lt_irrefl _ ((height_strict_mono_of_isPrime h₃).trans_le
+    (e'.trans <| height_mono h₁.le))
 
 /-- A prime ideal has height zero if and only if it is minimal -/
-lemma Ideal.primeHeight_eq_zero_iff {I : Ideal R} [I.IsPrime] :
+lemma Ideal.height_eq_zero_iff {I : Ideal R} [I.IsPrime] : height I = 0 ↔ I ∈ minimalPrimes R := by
+  rw [Ideal.height_eq_primeHeight, Ideal.primeHeight, Order.height_eq_zero,
+    minimalPrimes_eq_minimals]
+  refine ⟨fun h ↦ ⟨‹_›, ?_⟩, fun ⟨hI, hI'⟩ b hb ↦ hI' b.isPrime hb⟩
+  by_contra! ⟨P, ⟨hP₁, ⟨hP₂, hP₃⟩⟩⟩
+  exact hP₃ (h (b := ⟨P, hP₁⟩) hP₂)
+
+@[deprecated "Use `Ideal.height_eq_zero_iff` instead." (since := "2026-04-02")]
+private lemma Ideal.primeHeight_eq_zero_iff {I : Ideal R} [I.IsPrime] :
     primeHeight I = 0 ↔ I ∈ minimalPrimes R := by
-  rw [Ideal.primeHeight, Order.height_eq_zero, minimalPrimes_eq_minimals]
-  constructor
-  · intro h
-    refine ⟨inferInstance, ?_⟩
-    by_contra! ⟨P, ⟨hP₁, ⟨hP₂, hP₃⟩⟩⟩
-    exact hP₃ (h (b := ⟨P, hP₁⟩) hP₂)
-  · rintro ⟨hI, hI'⟩ b hb
-    exact hI' (y := b.asIdeal) b.isPrime hb
+  rw [← Ideal.height_eq_primeHeight, Ideal.height_eq_zero_iff]
 
 /-- If `x` is a non-zero-divisor, then `span {x}` has height at least 1. -/
 lemma Ideal.one_le_height_span_singleton_of_mem_nonZeroDivisors
     {x : R} (hx : x ∈ nonZeroDivisors R) : 1 ≤ (span {x}).height := by
-  dsimp [Ideal.height]
+  rw [Ideal.height_eq_inf_minimalPrimes]
   refine le_iInf₂ fun q hq => ?_
   have : q.IsPrime := hq.isPrime
-  rw [ENat.one_le_iff_ne_zero, Ne, primeHeight_eq_zero_iff]
+  rw [ENat.one_le_iff_ne_zero, Ne, height_eq_zero_iff]
   intro hmin
   exact absurd hx <| notMem_nonZeroDivisors_of_mem_mem_minimalPrimes
     (hq.1.2 <| Ideal.mem_span_singleton.mpr <| dvd_refl x) hmin
@@ -213,49 +243,58 @@ lemma Ideal.one_le_height_span_singleton_of_mem_nonZeroDivisors
 @[simp]
 lemma Ideal.height_bot [Nontrivial R] : (⊥ : Ideal R).height = 0 := by
   obtain ⟨p, hp⟩ := Ideal.nonempty_minimalPrimes (R := R) (I := ⊥) top_ne_bot.symm
-  simp only [Ideal.height, ENat.iInf_eq_zero]
-  exact ⟨p, hp, haveI := hp.isPrime; primeHeight_eq_zero_iff.mpr hp⟩
+  rw [Ideal.height_eq_inf_minimalPrimes]
+  simp only [ENat.iInf_eq_zero]
+  refine ⟨p, hp, haveI := hp.isPrime; height_eq_zero_iff.mpr hp⟩
 
 /-- In a trivial commutative ring, the height of any ideal is `∞`. -/
 @[simp, nontriviality]
 lemma Ideal.height_of_subsingleton [Subsingleton R] : I.height = ⊤ := by
   rw [Subsingleton.elim I ⊤, Ideal.height_top]
 
-theorem Ideal.isMaximal_of_primeHeight_eq_ringKrullDim {I : Ideal R} [I.IsPrime]
-    [FiniteRingKrullDim R] (e : I.primeHeight = ringKrullDim R) : I.IsMaximal := by
-  have h : I ≠ ⊤ := by
-    intro h
-    simp only [h, ← Ideal.height_eq_primeHeight, Ideal.height_top, WithBot.coe_top] at e
-    exact ringKrullDim_ne_top e.symm
+theorem Ideal.isMaximal_of_height_eq_ringKrullDim {I : Ideal R} [I.IsPrime]
+    [FiniteRingKrullDim R] (e : I.height = ringKrullDim R) : I.IsMaximal := by
+  have h : I ≠ ⊤ := Ideal.IsPrime.ne_top'
   obtain ⟨M, hM, hM'⟩ := Ideal.exists_le_maximal I h
   rcases lt_or_eq_of_le hM' with (hM' | hM')
-  · have h1 := Ideal.primeHeight_strict_mono hM'
-    have h2 := e ▸ M.primeHeight_le_ringKrullDim
+  · have h1 := Ideal.height_strict_mono_of_isPrime hM'
+    have h2 := e ▸ M.height_le_ringKrullDim_of_ne_top hM.ne_top
     simp [← not_lt, h1] at h2
   · exact hM' ▸ hM
 
-/-- The prime height of the maximal ideal equals the Krull dimension in a local ring -/
-@[simp]
-theorem IsLocalRing.maximalIdeal_primeHeight_eq_ringKrullDim [IsLocalRing R] :
-    (IsLocalRing.maximalIdeal R).primeHeight = ringKrullDim R := by
-  rw [ringKrullDim, Ideal.primeHeight, ← Order.height_top_eq_krullDim]
-  rfl
+@[deprecated "Use `Ideal.isMaximal_of_height_eq_ringKrullDim` instead." (since := "2026-04-02")]
+private theorem Ideal.isMaximal_of_primeHeight_eq_ringKrullDim {I : Ideal R} [I.IsPrime]
+    [FiniteRingKrullDim R] (e : I.primeHeight = ringKrullDim R) : I.IsMaximal :=
+  Ideal.isMaximal_of_height_eq_ringKrullDim (by simpa [Ideal.height_eq_primeHeight])
 
 /-- The height of the maximal ideal equals the Krull dimension in a local ring. -/
 @[simp]
 theorem IsLocalRing.maximalIdeal_height_eq_ringKrullDim [IsLocalRing R] :
     (IsLocalRing.maximalIdeal R).height = ringKrullDim R := by
-  rw [Ideal.height_eq_primeHeight, IsLocalRing.maximalIdeal_primeHeight_eq_ringKrullDim]
+  rw [Ideal.height_eq_primeHeight, Ideal.primeHeight]
+  exact Order.height_top_eq_krullDim
+
+@[deprecated "Use `IsLocalRing.maximalIdeal_height_eq_ringKrullDim` instead."
+  (since := "2026-04-04")]
+private theorem IsLocalRing.maximalIdeal_primeHeight_eq_ringKrullDim [IsLocalRing R] :
+    (IsLocalRing.maximalIdeal R).primeHeight = ringKrullDim R := by
+  simp [← Ideal.height_eq_primeHeight]
 
 /-- For a local ring with finite Krull dimension, a prime ideal has height equal to the Krull
 dimension if and only if it is the maximal ideal. -/
-theorem Ideal.primeHeight_eq_ringKrullDim_iff [FiniteRingKrullDim R] [IsLocalRing R] {I : Ideal R}
-    [I.IsPrime] : Ideal.primeHeight I = ringKrullDim R ↔ I = IsLocalRing.maximalIdeal R := by
+theorem Ideal.height_eq_ringKrullDim_iff [FiniteRingKrullDim R] [IsLocalRing R] {I : Ideal R}
+    [I.IsPrime] : I.height = ringKrullDim R ↔ I = IsLocalRing.maximalIdeal R := by
   constructor
   · intro h
-    exact IsLocalRing.eq_maximalIdeal (Ideal.isMaximal_of_primeHeight_eq_ringKrullDim h)
+    exact IsLocalRing.eq_maximalIdeal (Ideal.isMaximal_of_height_eq_ringKrullDim h)
   · rintro rfl
-    exact IsLocalRing.maximalIdeal_primeHeight_eq_ringKrullDim
+    exact IsLocalRing.maximalIdeal_height_eq_ringKrullDim
+
+@[deprecated "Use `Ideal.height_eq_ringKrullDim_iff` instead." (since := "2026-04-02")]
+private theorem Ideal.primeHeight_eq_ringKrullDim_iff [FiniteRingKrullDim R] [IsLocalRing R]
+    {I : Ideal R} [I.IsPrime] :
+    Ideal.primeHeight I = ringKrullDim R ↔ I = IsLocalRing.maximalIdeal R := by
+  rw [← Ideal.height_eq_primeHeight, Ideal.height_eq_ringKrullDim_iff]
 
 lemma Ideal.height_le_iff {p : Ideal R} {n : ℕ} [p.IsPrime] :
     p.height ≤ n ↔ ∀ q : Ideal R, q.IsPrime → q < p → q.height < n := by
@@ -323,11 +362,12 @@ lemma ringKrullDim_le_iff_isMaximal_height_le {R : Type*} [CommRing R] (n : With
   norm_cast
   exact Ideal.height_mono hle
 
-theorem IsLocalization.primeHeight_under (S : Submonoid R) {A : Type*} [CommRing A] [Algebra R A]
-    [IsLocalization S A] (J : Ideal A) [J.IsPrime] :
-    (J.under R).primeHeight = J.primeHeight := by
-  rw [eq_comm, Ideal.primeHeight, Ideal.primeHeight, ← WithBot.coe_inj,
-    Order.height_eq_krullDim_Iic, Order.height_eq_krullDim_Iic]
+private theorem IsLocalization.height_under_eq_of_isPrime (S : Submonoid R) {A : Type*} [CommRing A]
+    [Algebra R A] [IsLocalization S A] (J : Ideal A) [J.IsPrime] :
+    (J.comap (algebraMap R A)).height = J.height := by
+  rw [eq_comm, Ideal.height_eq_primeHeight, Ideal.height_eq_primeHeight, Ideal.primeHeight,
+    Ideal.primeHeight, ← WithBot.coe_inj, Order.height_eq_krullDim_Iic,
+    Order.height_eq_krullDim_Iic]
   let e := IsLocalization.orderIsoOfPrime S A
   have H (p : Ideal R) (hp : p ≤ J.comap (algebraMap R A)) : Disjoint (S : Set R) p :=
     Set.disjoint_of_subset_right hp (e ⟨_, ‹J.IsPrime›⟩).2.2
@@ -340,14 +380,19 @@ theorem IsLocalization.primeHeight_under (S : Submonoid R) {A : Type*} [CommRing
         congrArg (fun I ↦ I.1) (e.right_inv ⟨_, I.1.2, H _ I.2⟩)
       map_rel_iff' {I₁ I₂} := @RelIso.map_rel_iff _ _ _ _ e ⟨_, I₁.1.2⟩ ⟨_, I₂.1.2⟩ }
 
-@[deprecated (since := "2026-04-09")] alias IsLocalization.primeHeight_comap :=
-  IsLocalization.primeHeight_under
+@[deprecated "Use `Ideal.height_ne_top_of_isPrime` instead." (since := "2026-04-04")]
+private theorem IsLocalization.primeHeight_comap (S : Submonoid R) {A : Type*} [CommRing A]
+    [Algebra R A] [IsLocalization S A] (J : Ideal A) [J.IsPrime] :
+    (J.comap (algebraMap R A)).primeHeight = J.primeHeight := by
+  simpa [Ideal.height_eq_primeHeight] using IsLocalization.height_under_eq_of_isPrime S J
 
 theorem IsLocalization.height_under (S : Submonoid R) {A : Type*} [CommRing A] [Algebra R A]
     [IsLocalization S A] (J : Ideal A) : (J.under R).height = J.height := by
-  rw [Ideal.height, Ideal.height]
-  simp_rw [← IsLocalization.primeHeight_under S, IsLocalization.minimalPrimes_comap S A,
-    ← Ideal.height_eq_primeHeight, iInf_image]
+  rw [(J.comap _).height_eq_inf_minimalPrimes, J.height_eq_inf_minimalPrimes]
+  simp only [IsLocalization.minimalPrimes_comap S A, iInf_image]
+  apply iInf_congr (fun p ↦ iInf_congr fun hp ↦ ?_)
+  have := hp.isPrime
+  exact IsLocalization.height_under_eq_of_isPrime S _
 
 @[deprecated (since := "2026-04-09")] alias IsLocalization.height_comap :=
   IsLocalization.height_under
@@ -356,10 +401,9 @@ theorem IsLocalization.AtPrime.ringKrullDim_eq_height (I : Ideal R) [I.IsPrime]
     [CommRing A] [Algebra R A] [IsLocalization.AtPrime A I] :
     ringKrullDim A = I.height := by
   have := IsLocalization.AtPrime.isLocalRing A I
-  rw [← IsLocalRing.maximalIdeal_primeHeight_eq_ringKrullDim,
-      ← IsLocalization.primeHeight_under I.primeCompl,
-      ← IsLocalization.AtPrime.under_maximalIdeal A I,
-      Ideal.height_eq_primeHeight]
+  rw [← IsLocalRing.maximalIdeal_height_eq_ringKrullDim,
+      ← IsLocalization.height_under I.primeCompl,
+      ← IsLocalization.AtPrime.under_maximalIdeal A I]
 
 lemma IsLocalization.height_map_of_disjoint {S : Type*} [CommRing S] [Algebra R S] (M : Submonoid R)
     [IsLocalization M S] (p : Ideal R) [p.IsPrime] (h : Disjoint (M : Set R) (p : Set R)) :
@@ -373,7 +417,8 @@ lemma IsLocalization.height_map_of_disjoint {S : Type*} [CommRing S] [Algebra R
   rw [AtPrime.ringKrullDim_eq_height P, AtPrime.ringKrullDim_eq_height p] at this
   exact WithBot.coe_eq_coe.mp this
 
-lemma mem_minimalPrimes_of_primeHeight_eq_height {I J : Ideal R} [J.IsPrime] (e : I ≤ J)
+@[deprecated "Use `mem_minimalPrimes_of_height_eq` instead." (since := "2026-04-02")]
+private lemma mem_minimalPrimes_of_primeHeight_eq_height {I J : Ideal R} [J.IsPrime] (e : I ≤ J)
     (e' : J.primeHeight = I.height) [J.FiniteHeight] : J ∈ I.minimalPrimes := by
   rw [← J.height_eq_primeHeight] at e'
   exact mem_minimalPrimes_of_height_eq e (e' ▸ le_refl _)
@@ -408,25 +453,18 @@ lemma exists_spanRank_le_and_le_height_of_le_height [IsNoetherianRing R] (I : Id
       exact add_le_add h₂ ((Submodule.spanRank_span_le_card _).trans (by simp))
     · refine le_iInf₂ (fun p hp ↦ ?_)
       have := hp.isPrime
+      rw [← p.height_eq_primeHeight]
       by_cases h : p.height = ⊤
-      · rw [← p.height_eq_primeHeight, h]
-        exact le_top
+      · exact le_of_le_of_eq le_top h.symm
       have : p.FiniteHeight := ⟨Or.inr h⟩
-      have := Ideal.height_mono (le_sup_left.trans hp.1.2)
-      suffices h : (r : ℕ∞) ≠ p.primeHeight by
-        push_cast
-        have := h₃.trans this
-        rw [Ideal.height_eq_primeHeight] at this
-        exact Order.add_one_le_of_lt (lt_of_le_of_ne this h)
+      have := Ideal.height_mono (le_sup_left.trans hp.le)
+      suffices h : (r : ℕ∞) ≠ p.height by
+        exact Order.add_one_le_of_lt (lt_of_le_of_ne (h₃.trans this) h)
       intro e
       apply hx₂ p
-      · have : J.height = p.primeHeight := by
-          apply le_antisymm
-          · rwa [← p.height_eq_primeHeight]
-          · rwa [← e]
-        refine ⟨mem_minimalPrimes_of_primeHeight_eq_height (le_sup_left.trans hp.le) this.symm, ?_⟩
-        rwa [p.height_eq_primeHeight, eq_comm]
-      · exact hp.le <| Ideal.mem_sup_right <| mem_span_singleton_self x
+      · refine ⟨mem_minimalPrimes_of_height_eq (le_sup_left.trans hp.le) (e.symm.trans_le h₃),
+          e.symm⟩
+      · apply hp.le <| Ideal.mem_sup_right <| mem_span_singleton_self x
 
 /-- In a nontrivial commutative ring `R`, the supremum of heights of all ideals is equal to the
 Krull dimension of `R`. -/
@@ -447,33 +485,43 @@ lemma Ideal.sup_height_eq_ringKrullDim [Nontrivial R] :
       · exact le_iSup_of_le p.last.isPrime.ne_top' le_rfl
       · exact le_iSup (fun I => ⨆ _, I.height) p.last.asIdeal
 
-/-- In a nontrivial commutative ring `R`, the supremum of prime heights of all prime ideals is
+/-- In a nontrivial commutative ring `R`, the supremum of heights of all prime ideals is
 equal to the Krull dimension of `R`. -/
-lemma Ideal.sup_primeHeight_eq_ringKrullDim [Nontrivial R] :
-    ↑(⨆ (I : Ideal R) (_ : I.IsPrime), I.primeHeight) = ringKrullDim R := by
+lemma Ideal.sup_isPrime_height_eq_ringKrullDim [Nontrivial R] :
+    ↑(⨆ (I : Ideal R) (_ : I.IsPrime), I.height) = ringKrullDim R := by
   rw [← sup_height_eq_ringKrullDim, WithBot.coe_inj]
   apply le_antisymm
-  · exact iSup_mono fun I => iSup_mono' fun hI => ⟨hI.ne_top, by rw [← height_eq_primeHeight]⟩
+  · exact iSup_mono fun I => iSup_mono' fun hI => ⟨hI.ne_top, le_refl _⟩
   · refine iSup_mono' fun I => ?_
     by_cases I_top : I = ⊤
     · exact ⟨⊥, by simp [I_top]⟩
-    · obtain ⟨P, hP⟩ : I.minimalPrimes.Nonempty :=
-        Set.nonempty_coe_sort.mp (nonempty_minimalPrimes I_top)
+    · obtain ⟨P, hP⟩ := Set.nonempty_coe_sort.mp (nonempty_minimalPrimes I_top)
       refine ⟨P, iSup_pos (α := ℕ∞) I_top ▸ le_iSup_of_le (hP.left.left) ?_⟩
-      exact iInf_le_of_le P (iInf_le_of_le hP le_rfl)
+      have := hP.isPrime
+      exact iInf_le_of_le P (iInf_le_of_le hP (ge_of_eq (Ideal.height_eq_primeHeight P)))
+
+@[deprecated "Use `Ideal.sup_height_isPrime_eq_ringKrullDim` instead." (since := "2026-04-02")]
+private lemma Ideal.sup_primeHeight_eq_ringKrullDim [Nontrivial R] :
+    ↑(⨆ (I : Ideal R) (_ : I.IsPrime), I.primeHeight) = ringKrullDim R := by
+  simp [← Ideal.height_eq_primeHeight, Ideal.sup_isPrime_height_eq_ringKrullDim]
 
-/-- In a nontrivial commutative ring `R`, the supremum of prime heights of all maximal ideals is
+/-- In a nontrivial commutative ring `R`, the supremum of heights of all maximal ideals is
 equal to the Krull dimension of `R`. -/
-lemma Ideal.sup_primeHeight_of_maximal_eq_ringKrullDim [Nontrivial R] :
-    ↑(⨆ (I : Ideal R) (_ : I.IsMaximal), I.primeHeight) = ringKrullDim R := by
-  rw [← Ideal.sup_primeHeight_eq_ringKrullDim, WithBot.coe_inj]
+lemma Ideal.sup_isMaximal_height_eq_ringKrullDim [Nontrivial R] :
+    ↑(⨆ (I : Ideal R) (_ : I.IsMaximal), I.height) = ringKrullDim R := by
+  rw [← Ideal.sup_height_eq_ringKrullDim, WithBot.coe_inj]
   apply le_antisymm
-  · exact iSup_mono fun I => iSup_mono' fun hI => ⟨IsMaximal.isPrime hI, le_rfl⟩
+  · exact iSup_mono fun I => iSup_mono' fun hI => ⟨hI.isPrime.ne_top , le_rfl⟩
   · refine iSup_mono' fun I => ?_
     obtain rfl | I_top := eq_or_ne I ⊤
     · exact ⟨⊥, by grind [iSup_le_iff, Ideal.IsPrime.ne_top]⟩
     · obtain ⟨M, hM, hIM⟩ := exists_le_maximal I I_top
-      exact ⟨M, iSup_mono' (fun hI ↦ ⟨hM, primeHeight_mono hIM⟩)⟩
+      exact ⟨M, iSup_mono' (fun hI ↦ ⟨hM, height_mono hIM⟩)⟩
+
+@[deprecated "Use `Ideal.sup_height_of_maximal_eq_ringKrullDim` instead." (since := "2026-04-02")]
+private lemma Ideal.sup_primeHeight_of_maximal_eq_ringKrullDim [Nontrivial R] :
+    ↑(⨆ (I : Ideal R) (_ : I.IsMaximal), I.primeHeight) = ringKrullDim R := by
+  simp_rw [← Ideal.height_eq_primeHeight, Ideal.sup_isMaximal_height_eq_ringKrullDim]
 
 section isLocalization
 
@@ -488,10 +536,9 @@ lemma Ring.krullDimLE_of_isLocalization_maximal {n : ℕ}
     Ring.KrullDimLE n R := by
   simp_rw [Ring.krullDimLE_iff] at h ⊢
   nontriviality R
-  rw [← Ideal.sup_primeHeight_of_maximal_eq_ringKrullDim]
+  rw [← Ideal.sup_isMaximal_height_eq_ringKrullDim]
   refine (WithBot.coe_le_coe).mpr (iSup₂_le_iff.mpr fun P hP ↦ ?_)
-  rw [← Ideal.height_eq_primeHeight, ← WithBot.coe_le_coe]
-  rw [← IsLocalization.AtPrime.ringKrullDim_eq_height P (Rₚ P)]
+  rw [← WithBot.coe_le_coe, ← IsLocalization.AtPrime.ringKrullDim_eq_height P (Rₚ P)]
   exact h P
 
 end isLocalization
diff --git a/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean b/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean
index 86c33519dd60d2..5aa2e8787d83d3 100644
--- a/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean
+++ b/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean
@@ -160,9 +160,8 @@ theorem Ideal.mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert {q p : Ide
         sup_eq_left.mpr hI'q, sup_eq_left.mpr hI'p] using comap_mono (f := f) e
     have : (q.map f).IsPrime := map_isPrime_of_surjective hf (by rwa [mk_ker])
     have : (p.map f).FiniteHeight := ⟨Or.inr (h.trans_lt (WithTop.coe_lt_top 1)).ne⟩
-    rw [height_eq_primeHeight] at h
-    have := (primeHeight_strict_mono h_lt).trans_le h
-    rw [ENat.lt_one_iff_eq_zero, primeHeight_eq_zero_iff] at this
+    have := (height_strict_mono_of_isPrime_of_isPrime h_lt).trans_le h
+    rw [ENat.lt_one_iff_eq_zero, height_eq_zero_iff] at this
     have := minimalPrimes_comap_of_surjective hf this
     rwa [comap_map_of_surjective f hf, ← RingHom.ker_eq_comap_bot,
       mk_ker, sup_eq_left.mpr hI'q] at this
@@ -194,8 +193,7 @@ nonrec lemma Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes
     have := hp.isPrime
     cases n with
     | zero =>
-      rw [ENat.coe_zero, nonpos_iff_eq_zero, height_eq_primeHeight p,
-        primeHeight_eq_zero_iff, minimalPrimes]
+      rw [ENat.coe_zero, nonpos_iff_eq_zero, height_eq_zero_iff, minimalPrimes]
       simp_all
     | succ n =>
       wlog hR : ∃ (_ : IsLocalRing R), p = maximalIdeal R
@@ -255,9 +253,8 @@ than or equal to the minimum number of generators for this ideal. -/
 lemma Ideal.height_le_spanRank_toENat (I : Ideal R) (hI : I ≠ ⊤) :
     I.height ≤ I.spanRank.toENat := by
   obtain ⟨J, hJ⟩ := nonempty_minimalPrimes hI
-  refine (iInf₂_le J hJ).trans ?_
-  convert (I.height_le_spanRank_toENat_of_mem_minimalPrimes J hJ)
-  exact (@height_eq_primeHeight _ _ J hJ.1.1).symm
+  rw [I.height_eq_inf_minimalPrimes]
+  exact (iInf₂_le J hJ).trans (I.height_le_spanRank_toENat_of_mem_minimalPrimes J hJ)
 
 lemma Ideal.height_le_spanFinrank (I : Ideal R) (hI : I ≠ ⊤) :
     I.height ≤ I.spanFinrank := by
@@ -483,7 +480,7 @@ lemma Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown [IsNoetherianRing S
       simp [hlq, map_le_iff_le_comap, LiesOver.over (p := p) (P := P)]
   obtain ⟨lp', hlp'len, hlp', _⟩ := exists_ltSeries_of_hasGoingDown lp l'.head.asIdeal
   have : (lp'.smash l' hlp').length = lp.length + lq.length := by simp [hlp'len, l']
-  rw [← hlenp, ← hlenq, ← Nat.cast_add, ← this, height_eq_primeHeight]
+  rw [← hlenp, ← hlenq, ← Nat.cast_add, ← this, (⟨P, ‹_›⟩ : PrimeSpectrum S).height_eq_orderHeight]
   apply Order.length_le_height
   simp [hlq, l', ← PrimeSpectrum.asIdeal_le_asIdeal, map_le_iff_le_comap,
     LiesOver.over (p := p) (P := P)]
diff --git a/Mathlib/RingTheory/KrullDimension/PID.lean b/Mathlib/RingTheory/KrullDimension/PID.lean
index 74c56d4b0bde82..370302852f63ef 100644
--- a/Mathlib/RingTheory/KrullDimension/PID.lean
+++ b/Mathlib/RingTheory/KrullDimension/PID.lean
@@ -51,5 +51,5 @@ lemma IsPrincipalIdealRing.height_eq_one_of_isMaximal {R : Type*} [CommRing R] [
   · suffices h : (m.height : WithBot ℕ∞) ≤ 1 by norm_cast at h
     rw [← IsPrincipalIdealRing.ringKrullDim_eq_one _ h]
     exact Ideal.height_le_ringKrullDim_of_ne_top Ideal.IsPrime.ne_top'
-  · rw [Order.one_le_iff_pos, Ideal.height_eq_primeHeight, Ideal.primeHeight, Order.height_pos]
-    exact not_isMin_of_lt (b := ⊥) (Ideal.bot_lt_of_maximal m h)
+  · apply le_of_eq_of_le _ (Ideal.height_add_one_le_of_lt_of_isPrime (Ideal.bot_lt_of_maximal m h))
+    simp