diff --git a/comm_alg/grant.lean b/comm_alg/grant.lean
index 86c05fc..2814919 100644
--- a/comm_alg/grant.lean
+++ b/comm_alg/grant.lean
@@ -1,12 +1,31 @@
 import Mathlib.Order.KrullDimension
+import Mathlib.Order.JordanHolder
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
+import Mathlib.Order.Height
 
-def hello : IO Unit := do
-  IO.println "Hello, World!"
-
-#eval hello
 
 #check (p q : PrimeSpectrum _) → (p ≤ q)
 #check Preorder (PrimeSpectrum _)
 
-#check krullDim (PrimeSpectrum _)
\ No newline at end of file
+-- Dimension of a ring
+#check krullDim (PrimeSpectrum _)
+
+-- Length of a module
+#check krullDim (Submodule _ _)
+
+#check JordanHolderLattice
+
+
+variable {α : Type _} [Preorder α] (s : Set α)
+
+-- there should be a coercion from WithTop ℕ to WithBot (WithTop ℕ) but it doesn't seem to work
+-- it looks like this might be because someone changed the instance from CoeCT to Coe during the port
+lemma twoHeights : s ≠ ∅ → (some (Set.chainHeight s) : WithBot (WithTop ℕ)) = krullDim s := by
+  intro hs
+  unfold Set.chainHeight
+  unfold krullDim
+  have hKrullSome : ∃n, krullDim s = some n := by
+    
+    sorry
+  -- norm_cast
+  sorry
\ No newline at end of file