From 9c4f129a56e2fd7d935e988815ea793a95e25683 Mon Sep 17 00:00:00 2001
From: GTBarkley <barkleygrant@gmail.com>
Date: Fri, 16 Jun 2023 04:57:28 +0000
Subject: [PATCH] added WF_interval_le_prime

---
 CommAlg/grant2.lean | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

diff --git a/CommAlg/grant2.lean b/CommAlg/grant2.lean
index 0e3092e..24edcff 100644
--- a/CommAlg/grant2.lean
+++ b/CommAlg/grant2.lean
@@ -54,9 +54,20 @@ def symbolicIdeal(Q : Ideal R) {hin : Q.IsPrime} (I : Ideal R) : Ideal R where
     rw [←mul_assoc, mul_comm s, mul_assoc]
     exact Ideal.mul_mem_left _ _ hs2
 
+
+theorem WF_interval_le_prime (I : Ideal R) (P : Ideal R) [P.IsPrime] 
+  (h : ∀ J ∈ (Set.Icc I P), J.IsPrime → J = P ):
+  WellFounded ((· < ·) : (Set.Icc I P) → (Set.Icc I P) → Prop ) := sorry 
+
 protected lemma LocalRing.height_le_one_of_minimal_over_principle
-  [LocalRing R] (q : PrimeSpectrum R) {x : R} 
+  [LocalRing R] {x : R} 
   (h : (closedPoint R).asIdeal ∈ (Ideal.span {x}).minimalPrimes) :
-  q = closedPoint R ∨ Ideal.height q = 0 := by
-  
+  Ideal.height (closedPoint R) ≤ 1 := by
+  -- by_contra hcont
+  -- push_neg at hcont
+  -- rw [Ideal.lt_height_iff'] at hcont
+  -- rcases hcont with ⟨c, hc1, hc2, hc3⟩
+  apply height_le_of_gt_height_lt
+  intro p hp
+
   sorry
\ No newline at end of file