exact mem_insert _ _
case pos.refine_1
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
x : α
hxs : x ∈ s
heq : x = a
⊢ b ∈ insert b (f '' (s \ {a}))
no goals