apply mem_insert
case refine_1
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
s : Set α
x✝ : P s
h : ∀ ⦃y : Set α⦄, P y → s ⊆ y → s = y
x : α
hx : x ∉ s
hxs : P (insert x s)
⊢ x ∈ insert x s
no goals