English
If J is a prime ideal containing I, and its height is at most the height of I, then J is a minimal prime over I.
Русский
Если J - простый идеал, содержащий I, и высота J не превышает высоту I, то J является минимальным над I.
LaTeX
$$$I \le J, \ J \text{ prime}, \ FiniteHeight(J), \ J.height \le I.height \Rightarrow J \in I.minimalPrimes.$$$
Lean4
/-- If J is a prime ideal containing I, and its height is less than or equal to the height of I,
then J is a minimal prime over I -/
theorem mem_minimalPrimes_of_height_eq {I J : Ideal R} (e : I ≤ J) [J.IsPrime] [FiniteHeight J]
(e' : J.height ≤ I.height) : J ∈ I.minimalPrimes :=
by
obtain ⟨p, h₁, h₂⟩ := Ideal.exists_minimalPrimes_le e
convert h₁
refine (eq_of_le_of_not_lt h₂ fun h₃ ↦ ?_).symm
have := h₁.1.1
have := finiteHeight_of_le h₂ IsPrime.ne_top'
exact lt_irrefl _ ((height_strict_mono_of_is_prime h₃).trans_le (e'.trans <| height_mono h₁.1.2))
