From 2402dd93b2ea145996de37ebc69d37591a3b96e9 Mon Sep 17 00:00:00 2001
From: leopoldmayer <leomayer@uw.edu>
Date: Fri, 16 Jun 2023 00:07:32 -0700
Subject: [PATCH] removed dependency on false sorried lemma

---
 CommAlg/krull.lean      | 28 ++++++++++++++++++++++++++--
 CommAlg/polynomial.lean | 18 ++++++++++++++++--
 2 files changed, 42 insertions(+), 4 deletions(-)

diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean
index e44fa91..e35a4c5 100644
--- a/CommAlg/krull.lean
+++ b/CommAlg/krull.lean
@@ -95,8 +95,32 @@ lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) :
     have : height I ≤ krullDim R := by apply height_le_krullDim
     exact le_trans h this
 
-lemma le_krullDim_iff' (R : Type _) [CommRing R] (n : ℕ∞) :
-  n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry
+#check ENat.recTopCoe
+
+/- terrible place for this lemma. Also this probably exists somewhere
+  Also this is a terrible proof
+-/
+lemma eq_top_iff (n : WithBot ℕ∞) : n = ⊤ ↔ ∀ m : ℕ, m ≤ n := by
+  aesop
+  induction' n using WithBot.recBotCoe with n
+  . exfalso
+    have := (a 0)
+    simp [not_lt_of_ge] at this
+  induction' n using ENat.recTopCoe with n
+  . rfl
+  . have := a (n + 1)
+    exfalso
+    change (((n + 1) : ℕ∞) : WithBot ℕ∞) ≤ _ at this
+    simp [WithBot.coe_le_coe] at this
+    change ((n + 1) : ℕ∞) ≤ (n : ℕ∞) at this
+    simp [ENat.add_one_le_iff] at this
+
+lemma krullDim_eq_top_iff (R : Type _) [CommRing R] :
+  krullDim R = ⊤ ↔ ∀ (n : ℕ), ∃ I : PrimeSpectrum R, n ≤ height I := by
+  simp [eq_top_iff, le_krullDim_iff]
+  change (∀ (m : ℕ), ∃ I, ((m : ℕ∞) : WithBot ℕ∞) ≤ height I) ↔ _
+  simp [WithBot.coe_le_coe]
+  
 
 /-- The Krull dimension of a local ring is the height of its maximal ideal. -/
 lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) := by
diff --git a/CommAlg/polynomial.lean b/CommAlg/polynomial.lean
index f130868..8dd886a 100644
--- a/CommAlg/polynomial.lean
+++ b/CommAlg/polynomial.lean
@@ -132,7 +132,7 @@ lemma ht_adjoin_x_eq_ht_add_one [Nontrivial R] (I : PrimeSpectrum R) : height I
       apply hl.2
       exact hb
 
-
+#check (⊤ : ℕ∞)
 /-
 dim R + 1 ≤ dim R[X]
 -/
@@ -142,12 +142,26 @@ lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
   rw [hn]
   change ↑(n + 1) ≤ krullDim R[X]
   have := le_of_eq hn.symm
-  rw [le_krullDim_iff'] at this ⊢
+  induction' n using ENat.recTopCoe with n
+  . change krullDim R = ⊤ at hn
+    change ⊤ ≤ krullDim R[X] 
+    rw [krullDim_eq_top_iff] at hn
+    rw [top_le_iff, krullDim_eq_top_iff]
+    intro n
+    obtain ⟨I, hI⟩ := hn n
+    use adjoin_x I
+    calc n ≤ height I := hI
+      _ ≤ height I + 1 := le_self_add
+      _ ≤ height (adjoin_x I) := ht_adjoin_x_eq_ht_add_one I
+  change n ≤ krullDim R at this
+  change (n + 1 : ℕ) ≤ krullDim R[X]
+  rw [le_krullDim_iff] at this ⊢
   obtain ⟨I, hI⟩ := this
   use adjoin_x I
   apply WithBot.coe_mono
   calc n + 1 ≤ height I + 1 := by
         apply add_le_add_right
+        change ((n : ℕ∞) : WithBot ℕ∞) ≤ (height I) at hI
         rw [WithBot.coe_le_coe] at hI
         exact hI
     _ ≤ height (adjoin_x I) := ht_adjoin_x_eq_ht_add_one I
\ No newline at end of file