no goals
α : Type u_1
β : Type ?u.108664
γ : Type ?u.108667
inst✝¹ : DecidableEq β
f g : α → β
s✝ : Finset α
t : Finset β
a : α
b c : β
inst✝ : DecidableEq α
s : Finset α
⊢ (image Subtype.val (attach s)).val = s.val
rw [image_val, attach_val, Multiset.attach_map_val, dedup_eq_self]