Lean4
/-- Map each element of a `Multiset` to an action, evaluate these actions in order,
and collect the results.
-/
def traverse : Multiset α' → F (Multiset β') :=
by
refine Quotient.lift (Functor.map ofList ∘ Traversable.traverse f) ?_
introv p; unfold Function.comp
induction p with
| nil => rfl
| @cons x l₁ l₂ _
h =>
have :
Multiset.cons <$> f x <*> ofList <$> Traversable.traverse f l₁ =
Multiset.cons <$> f x <*> ofList <$> Traversable.traverse f l₂ :=
by rw [h]
simpa [functor_norm] using this
| swap x y
l =>
have :
(fun a b (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) <$> f y <*> f x =
(fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y :=
by
rw [CommApplicative.commutative_map]
congr 2
funext a b l
simpa [flip] using Perm.swap a b l
simp [Function.comp_def, this, functor_norm]
| trans => simp [*]
