diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean
index 06e6d0d..ec94d36 100644
--- a/CommAlg/krull.lean
+++ b/CommAlg/krull.lean
@@ -63,7 +63,7 @@ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) :=
     apply height_le_of_le
     apply le_maximalIdeal
     exact I.2.1
-  . simp
+  . simp only [height_le_krullDim]
 
 #check height_le_krullDim
 --some propositions that would be nice to be able to eventually
@@ -135,7 +135,7 @@ lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by
   unfold krullDim
   simp [field_prime_height_zero]
 
-lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by
+lemma domain_dim_zero.isField {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by
   by_contra x
   rw [Ring.not_isField_iff_exists_prime] at x
   obtain ⟨P, ⟨h1, primeP⟩⟩ := x
@@ -156,9 +156,9 @@ lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0)
     aesop
   contradiction
 
-lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by
+lemma domain_dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by
   constructor
-  · exact isField.dim_zero
+  · exact domain_dim_zero.isField
   · intro fieldD
     let h : Field D := IsField.toField fieldD
     exact dim_field_eq_zero
diff --git a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean
index ea6f7cd..089c4b5 100644
--- a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean
+++ b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean
@@ -22,11 +22,7 @@ noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.c
 lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
   krullDim R + 1 ≤ krullDim (Polynomial R) := sorry -- Others are working on it
 
--- private lemma sum_succ_of_succ_sum {ι : Type} (a : ℕ∞) [inst : Nonempty ι] :
---       (⨆ (x : ι), a + 1) = (⨆ (x : ι), a) + 1 := by
---   have : a + 1 = (⨆ (x : ι), a) + 1 := by rw [ciSup_const]
---   have : a + 1 = (⨆ (x : ι), a + 1) := Eq.symm ciSup_const
---   simp
+lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ height J := sorry -- Already done in main file
 
 lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
   krullDim R + 1 = krullDim (Polynomial R) := by
@@ -37,16 +33,30 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
     have htPBdd : ∀ (P : PrimeSpectrum (Polynomial R)), (height P : WithBot ℕ∞) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I + 1)) := by
       intro P
       have : ∃ (I : PrimeSpectrum R), (height P : WithBot ℕ∞) ≤ ↑(height I + 1) := by
-        sorry
+        have : ∃ M, Ideal.IsMaximal M ∧ P.asIdeal ≤ M := by
+          apply exists_le_maximal
+          apply IsPrime.ne_top
+          apply P.IsPrime
+        obtain ⟨M, maxM, PleM⟩ := this
+        let P' : PrimeSpectrum (Polynomial R) := PrimeSpectrum.mk M (IsMaximal.isPrime maxM)
+        have PleP' : P ≤ P' := PleM
+        have : height P ≤ height P' := height_le_of_le PleP'
+        simp only [WithBot.coe_le_coe]
+        have : ∃ (I : PrimeSpectrum R), height P' ≤ height I + 1 := by
+
+          sorry
+        obtain ⟨I, h⟩ := this
+        use I
+        exact ge_trans h this
       obtain ⟨I, IP⟩ := this
       have : (↑(height I + 1) : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum R), ↑(height I + 1) := by
         apply @le_iSup (WithBot ℕ∞) _ _ _ I
-      apply ge_trans this IP
+      exact ge_trans this IP
     have oneOut : (⨆ (I : PrimeSpectrum R), (height I : WithBot ℕ∞) + 1) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := by
       have : ∀ P : PrimeSpectrum R, (height P : WithBot ℕ∞) + 1 ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 :=
         fun P ↦ (by apply add_le_add_right (@le_iSup (WithBot ℕ∞) _ _ _ P) 1)
       apply iSup_le
       apply this
-    simp
+    simp only [iSup_le_iff]
     intro P
     exact ge_trans oneOut (htPBdd P)