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
eta : ApplicativeTransformation G H
α β : Type u_1
f : α → G β
x : Multiset α
⊢ ∀ (a : List α),
    (fun {α} => ApplicativeTransformation.app eta α) (traverse f (Quotient.mk (isSetoid α) a)) =
      traverse ((fun {α} => ApplicativeTransformation.app eta α) ∘ f) (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
eta : ApplicativeTransformation G H
α β : Type u_1
f : α → G β
x : Multiset α
⊢ (fun {α} => ApplicativeTransformation.app eta α) (traverse f x) =
    traverse ((fun {α} => ApplicativeTransformation.app eta α) ∘ f) 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
eta : ApplicativeTransformation G H
α β : Type u_1
f : α → G β
x : Multiset α
a✝ : List α
⊢ (fun {α} => ApplicativeTransformation.app eta α) (traverse f (Quotient.mk (isSetoid α) a✝)) =
    traverse ((fun {α} => ApplicativeTransformation.app eta α) ∘ f) (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
eta : ApplicativeTransformation G H
α β : Type u_1
f : α → G β
x : Multiset α
⊢ ∀ (a : List α),
    (fun {α} => ApplicativeTransformation.app eta α) (traverse f (Quotient.mk (isSetoid α) a)) =
      traverse ((fun {α} => ApplicativeTransformation.app eta α) ∘ f) (Quotient.mk (isSetoid α) a)
intro
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
eta : ApplicativeTransformation G H
α β : Type u_1
f : α → G β
x : Multiset α
a✝ : List α
⊢ (fun {α} => ApplicativeTransformation.app eta α) (traverse f (Quotient.mk (isSetoid α) a✝)) =
    traverse ((fun {α} => ApplicativeTransformation.app eta α) ∘ f) (Quotient.mk (isSetoid α) a✝)
simp only [quot_mk_to_coe, traverse, lift_coe, Function.comp_apply,
  ApplicativeTransformation.preserves_map, IsLawfulTraversable.naturality]