α : Type u_1
β : Type ?u.45169
γ : Type ?u.45172
f : α ↪ β
s✝ s : Finset α
⊢ Multiset.map (↑(Embedding.subtype fun x => x ∈ s)) (Multiset.attach s.val) = s.val
α : Type u_1
β : Type ?u.45169
γ : Type ?u.45172
f : α ↪ β
s✝ s : Finset α
⊢ (map (Embedding.subtype fun x => x ∈ s) (attach s)).val = s.val
rw [map_val, attach_val]
no goals
α : Type u_1
β : Type ?u.45169
γ : Type ?u.45172
f : α ↪ β
s✝ s : Finset α
⊢ Multiset.map (↑(Embedding.subtype fun x => x ∈ s)) (Multiset.attach s.val) = s.val
exact Multiset.attach_map_val _