From 19b26ca009c5eccb3d5ee33434686ce8687e1297 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 2 Aug 2024 09:49:48 -0300
Subject: [PATCH] height_top_eq_krullDim

---
 Carleson/ToMathlib/Height.lean | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/Carleson/ToMathlib/Height.lean b/Carleson/ToMathlib/Height.lean
index 588f3e1a..4fe94ab1 100644
--- a/Carleson/ToMathlib/Height.lean
+++ b/Carleson/ToMathlib/Height.lean
@@ -522,10 +522,15 @@ lemma krullDim_eq_iSup_height : krullDim α = ⨆ (a : α), (height a : WithBot
     · rw [krullDim_eq_of_nonempty]
       simp only [WithBot.coe_le_coe, iSup_le_iff]
       intro x
-      apply height_le
-      intro p _
-      apply le_iSup_of_le p
-      simp only [le_refl]
+      exact height_le _ _ (fun p _ ↦ le_iSup_of_le p (le_refl _))
+
+@[simp]
+lemma height_top_eq_krullDim [OrderTop α] : height (⊤ : α) = krullDim α := by
+  rw [krullDim_eq_of_nonempty]
+  simp only [WithBot.coe_inj]
+  apply le_antisymm
+  · exact height_le _ _ (fun p _ ↦ le_iSup_of_le p (le_refl _))
+  · exact iSup_le (fun p => le_height_of_last_le ⊤ p le_top)
 
 
 /-! TODO: coheight -/