α β γ : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : CommApplicative F
inst✝¹ : CommApplicative G
inst✝ : DecidableEq α
s : Finset α
⊢ Multiset.toFinset <$> s.val = s
α β γ : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : CommApplicative F
inst✝¹ : CommApplicative G
inst✝ : DecidableEq α
s : Finset α
⊢ traverse pure s = s
rw [traverse, Multiset.id_traverse]
no goals
α β γ : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : CommApplicative F
inst✝¹ : CommApplicative G
inst✝ : DecidableEq α
s : Finset α
⊢ Multiset.toFinset <$> s.val = s
exact s.val_toFinset