From eb1e6118a05c375ee5d07150f9eedaede254e80c Mon Sep 17 00:00:00 2001
From: SinTan1729 <sayantan.santra689@gmail.com>
Date: Thu, 15 Jun 2023 19:36:02 -0700
Subject: [PATCH] Some changes to dim_eq_dim_poly_add_one

---
 CommAlg/sayantan(poly_over_field).lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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