English
There exists J ≤ I with J.spanRank = I.height and J.height = I.height, and J ≤ I, along with additional structure.
Русский
Существует J ≤ I такое, что J.spanRank = I.height и J.height = I.height, плюс дополнительная структура.
LaTeX
$$$\exists J \le I, J.spanRank = I.height \wedge J.height = I.height$$$
Lean4
theorem exists_spanRank_eq_and_height_eq (I : Ideal R) (hI : I ≠ ⊤) :
∃ J ≤ I, J.spanRank = I.height ∧ J.height = I.height :=
by
obtain ⟨J, hJ₁, hJ₂, hJ₃⟩ := exists_spanRank_le_and_le_height_of_le_height I _ (ENat.coe_toNat_le_self I.height)
rw [ENat.coe_toNat_eq_self.mpr (Ideal.height_ne_top hI)] at hJ₃
refine ⟨J, hJ₁, le_antisymm ?_ (le_trans ?_ (J.height_le_spanRank ?_)), le_antisymm (Ideal.height_mono hJ₁) hJ₃⟩
· convert hJ₂
exact Cardinal.ofENat_eq_nat.mpr (ENat.coe_toNat (I.height_ne_top hI)).symm
· exact Cardinal.ofENat_le_ofENat_of_le hJ₃
· rintro rfl
exact hI (top_le_iff.mp hJ₁)
