rw [(h hxs diff_subset)] at hx
case refine_1
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t
s : Set α
x✝ : P s
h : ∀ ⦃y : Set α⦄, P y → y ⊆ s → s = y
x : α
hx : x ∈ s
hxs : P (s \ {x})
⊢ False
case refine_1
α : Type u_1
P : Set α → Prop
hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t
s : Set α
x✝ : P s
h : ∀ ⦃y : Set α⦄, P y → y ⊆ s → s = y
x : α
hx : x ∈ s \ {x}
hxs : P (s \ {x})
⊢ False