diff --git a/CommAlg/sayantan(poly_over_field).lean b/CommAlg/sayantan(poly_over_field).lean
index 5379c52..987fe93 100644
--- a/CommAlg/sayantan(poly_over_field).lean
+++ b/CommAlg/sayantan(poly_over_field).lean
@@ -16,7 +16,8 @@ lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullD
   -- unfold krullDim
   rw [le_antisymm_iff]
   constructor
-  · sorry
+  · 
+    sorry
   · suffices : ∃I : PrimeSpectrum (Polynomial K), 1 ≤ (height I : WithBot ℕ∞)
     · obtain ⟨I, h⟩ := this
       have :  (height I : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum (Polynomial K)), ↑(height I) := by