formalize krull's height theorem

Stream: new members

[Kyle Trinh]

Hello, I am looking to try and formalize the height of ideals in Lean, but I am running into some trouble. Here is my height definiton and below is a lemma I am trying to prove to verify that it works:

noncomputable def height [h : I.IsPrime] : WithBot ℕ∞ :=
  Order.height {J : PrimeSpectrum R | J.asIdeal ≤ I}

lemma height_zero_of_minimal_prime' [h : I.IsPrime] :
    I ∈ minimalPrimes R → height I = 0 := by

  intros Imin
  rcases Imin with ⟨bot_le_I, y_minimal⟩
  simp_all
  by_contra height_neq_0
  simp [height] at *
  have nonempty_m : Nonempty {J : PrimeSpectrum R | J.asIdeal ≤ I} := by
    exact Set.nonempty_iff_ne_empty'.mpr height_neq_0
  let J := Classical.choice nonempty_m
  apply Nonempty.elim nonempty_m
  simp; intro a
  specialize y_minimal ?_
  . apply a.asIdeal
  . apply a.isPrime
  . contrapose! y_minimal; constructor
    . apply y_minimal
    . intro h
      sorry

Thank you!