no goals
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : IsDirected P fun x x_1 => x ≥ x_1
x : P
I J K s t : Ideal P
hx : ¬x ∈ I
h : I = I ⊔ principal x
⊢ x ∈ I
simpa only [left_eq_sup, principal_le_iff] using h