From e3a7639399596c8dc532b35eec70f2e19df8cf11 Mon Sep 17 00:00:00 2001
From: SinTan1729 <sayantan.santra689@gmail.com>
Date: Mon, 12 Jun 2023 23:58:40 -0700
Subject: [PATCH] new: Made some progress on the isField.dim_zero lemma

---
 CommAlg/sayantan.lean | 16 +++++++++++++---
 1 file changed, 13 insertions(+), 3 deletions(-)

diff --git a/CommAlg/sayantan.lean b/CommAlg/sayantan.lean
index b2fc79a..6140db5 100644
--- a/CommAlg/sayantan.lean
+++ b/CommAlg/sayantan.lean
@@ -57,9 +57,19 @@ lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0)
   simp [height] at h
   by_contra x
   rw [Ring.not_isField_iff_exists_prime] at x
-  obtain ⟨P, ⟨h, primeP⟩⟩ := x
-  have PgtBot : P > ⊥ := Ne.bot_lt h
-  sorry
+  obtain ⟨P, ⟨h1, primeP⟩⟩ := x
+  have PgtBot : P > ⊥ := Ne.bot_lt h1
+  have pos_height : ↑(Set.chainHeight {J | J < P}) > 0 := by
+    have : ⊥ ∈ {J | J < P} := PgtBot
+    have : {J | J < P}.Nonempty := Set.nonempty_of_mem this
+    -- have : {J | J < P} ≠ ∅ := Set.Nonempty.ne_empty this
+    rw [←Set.one_le_chainHeight_iff] at this
+    exact Iff.mp ENat.one_le_iff_pos this
+  have zero_height : ↑(Set.chainHeight {J | J < P}) = 0 := by
+    -- Probably need to use Sup_le or something here
+    sorry
+  have : ↑(Set.chainHeight {J | J < P}) ≠ 0 := Iff.mp pos_iff_ne_zero pos_height
+  contradiction
 
 lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by
   constructor