exact by_contra fun hxt ↦ h x hxs (hP ht (subset_diff_singleton hst hxt))
case refine_2
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t
s : Set α
x✝ : P s
h : ∀ x ∈ s, ¬P (s \ {x})
t : Set α
ht : P t
hst : t ⊆ s
x : α
hxs : x ∈ s
⊢ x ∈ t
no goals