no goals
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
I J K : Ideal P
S : Set (Ideal P)
⊢ x ∈ sInf S ↔ ∀ (s : Ideal P), s ∈ S → x ∈ s
simp_rw [← SetLike.mem_coe, coe_sInf, mem_iInter₂]