F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : CommApplicative F
α' β' : Type u
f : α' → F β'
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
α β γ : Type u_1
g : α → G β
h : β → H γ
x : Multiset α
⊢ ∀ (a : List α),
    traverse (Comp.mk ∘ Functor.map h ∘ g) (Quotient.mk (isSetoid α) a) =
      Comp.mk (traverse h <$> traverse g (Quotient.mk (isSetoid α) a))
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : CommApplicative F
α' β' : Type u
f : α' → F β'
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
α β γ : Type u_1
g : α → G β
h : β → H γ
x : Multiset α
⊢ traverse (Comp.mk ∘ Functor.map h ∘ g) x = Comp.mk (traverse h <$> traverse g x)
refine' Quotient.inductionOn x _
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : CommApplicative F
α' β' : Type u
f : α' → F β'
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
α β γ : Type u_1
g : α → G β
h : β → H γ
x : Multiset α
a✝ : List α
⊢ traverse (Comp.mk ∘ Functor.map h ∘ g) (Quotient.mk (isSetoid α) a✝) =
    Comp.mk (traverse h <$> traverse g (Quotient.mk (isSetoid α) a✝))
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : CommApplicative F
α' β' : Type u
f : α' → F β'
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
α β γ : Type u_1
g : α → G β
h : β → H γ
x : Multiset α
⊢ ∀ (a : List α),
    traverse (Comp.mk ∘ Functor.map h ∘ g) (Quotient.mk (isSetoid α) a) =
      Comp.mk (traverse h <$> traverse g (Quotient.mk (isSetoid α) a))
intro
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : CommApplicative F
α' β' : Type u
f : α' → F β'
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
α β γ : Type u_1
g : α → G β
h : β → H γ
x : Multiset α
a✝ : List α
⊢ Comp.mk (((fun x => ofList <$> x) ∘ Traversable.traverse h) <$> Traversable.traverse g a✝) =
    Comp.mk
      ((Quotient.lift (Functor.map ofList ∘ Traversable.traverse h)
            (_ :
              ∀ (a b : List β),
                a ≈ b →
                  (Functor.map Coe.coe ∘ Traversable.traverse h) a = (Functor.map Coe.coe ∘ Traversable.traverse h) b) ∘
          ofList) <$>
        Traversable.traverse g a✝)
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : CommApplicative F
α' β' : Type u
f : α' → F β'
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
α β γ : Type u_1
g : α → G β
h : β → H γ
x : Multiset α
a✝ : List α
⊢ traverse (Comp.mk ∘ Functor.map h ∘ g) (Quotient.mk (isSetoid α) a✝) =
    Comp.mk (traverse h <$> traverse g (Quotient.mk (isSetoid α) a✝))
simp only [traverse, quot_mk_to_coe, lift_coe, Coe.coe, Function.comp_apply, Functor.map_map,
  functor_norm]
no goals
F : Type u → Type u
inst✝⁵ : Applicative F
inst✝⁴ : CommApplicative F
α' β' : Type u
f : α' → F β'
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
α β γ : Type u_1
g : α → G β
h : β → H γ
x : Multiset α
a✝ : List α
⊢ Comp.mk (((fun x => ofList <$> x) ∘ Traversable.traverse h) <$> Traversable.traverse g a✝) =
    Comp.mk
      ((Quotient.lift (Functor.map ofList ∘ Traversable.traverse h)
            (_ :
              ∀ (a b : List β),
                a ≈ b →
                  (Functor.map Coe.coe ∘ Traversable.traverse h) a = (Functor.map Coe.coe ∘ Traversable.traverse h) b) ∘
          ofList) <$>
        Traversable.traverse g a✝)
simp only [Function.comp, lift_coe]