no goals
P : Type u_1
inst✝² : LE P
inst✝¹ : IsDirected P fun x x_1 => x ≤ x_1
inst✝ : Nonempty P
I : Ideal P
hI : IsCoatom I
src✝ : IsProper I := IsCoatom.isProper hI
x✝ : Ideal P
hJ : I < x✝
⊢ ↑x✝ = univ
simp [hI.2 _ hJ]