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