F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
α : Type u_1
x : Multiset α
⊢ ∀ (a : List α), traverse pure (Quotient.mk (isSetoid α) a) = Quotient.mk (isSetoid α) a
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
α : Type u_1
x : Multiset α
⊢ traverse pure x = x
refine' Quotient.inductionOn x _
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
α : Type u_1
x : Multiset α
a✝ : List α
⊢ traverse pure (Quotient.mk (isSetoid α) a✝) = Quotient.mk (isSetoid α) a✝
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
α : Type u_1
x : Multiset α
⊢ ∀ (a : List α), traverse pure (Quotient.mk (isSetoid α) a) = Quotient.mk (isSetoid α) a
intro
no goals
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
α : Type u_1
x : Multiset α
a✝ : List α
⊢ traverse pure (Quotient.mk (isSetoid α) a✝) = Quotient.mk (isSetoid α) a✝
simp [traverse, Coe.coe]