[GOAL]
⊢ LawfulFunctor Multiset
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
⊢ ∀ {α β : Type ?u.250}, Functor.mapConst = Functor.map ∘ Function.const β
[PROOFSTEP]
intros
[GOAL]
case refine'_2
⊢ ∀ {α : Type ?u.250} (x : Multiset α), id <$> x = x
[PROOFSTEP]
intros
[GOAL]
case refine'_3
⊢ ∀ {α β γ : Type ?u.250} (g : α → β) (h : β → γ) (x : Multiset α), (h ∘ g) <$> x = h <$> g <$> x
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α✝ β✝ : Type ?u.250
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝
[PROOFSTEP]
try simp
[GOAL]
case refine'_1
α✝ β✝ : Type ?u.250
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝
[PROOFSTEP]
simp
[GOAL]
case refine'_2
α✝ : Type ?u.250
x✝ : Multiset α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
try simp
[GOAL]
case refine'_2
α✝ : Type ?u.250
x✝ : Multiset α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
simp
[GOAL]
case refine'_3
α✝ β✝ γ✝ : Type ?u.250
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : Multiset α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
[PROOFSTEP]
try simp
[GOAL]
case refine'_3
α✝ β✝ γ✝ : Type ?u.250
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : Multiset α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
[PROOFSTEP]
simp
[GOAL]
case refine'_1
α✝ β✝ : Type ?u.250
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
⊢ Multiset α' → F (Multiset β')
[PROOFSTEP]
refine' Quotient.lift (Functor.map Coe.coe ∘ Traversable.traverse f) _
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
⊢ ∀ (a b : List α'),
    a ≈ b → (Functor.map Coe.coe ∘ Traversable.traverse f) a = (Functor.map Coe.coe ∘ Traversable.traverse f) b
[PROOFSTEP]
introv p
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
p : a ≈ b
⊢ (Functor.map Coe.coe ∘ Traversable.traverse f) a = (Functor.map Coe.coe ∘ Traversable.traverse f) b
[PROOFSTEP]
unfold Function.comp
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
p : a ≈ b
⊢ Coe.coe <$> Traversable.traverse f a = Coe.coe <$> Traversable.traverse f b
[PROOFSTEP]
induction p
[GOAL]
case nil
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
⊢ Coe.coe <$> Traversable.traverse f [] = Coe.coe <$> Traversable.traverse f []
case cons
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x✝ : α'
l₁✝ l₂✝ : List α'
a✝ : l₁✝ ~ l₂✝
a_ih✝ : Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₂✝
⊢ Coe.coe <$> Traversable.traverse f (x✝ :: l₁✝) = Coe.coe <$> Traversable.traverse f (x✝ :: l₂✝)
case swap
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x✝ y✝ : α'
l✝ : List α'
⊢ Coe.coe <$> Traversable.traverse f (y✝ :: x✝ :: l✝) = Coe.coe <$> Traversable.traverse f (x✝ :: y✝ :: l✝)
case trans
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b l₁✝ l₂✝ l₃✝ : List α'
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
a_ih✝¹ : Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₂✝
a_ih✝ : Coe.coe <$> Traversable.traverse f l₂✝ = Coe.coe <$> Traversable.traverse f l₃✝
⊢ Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₃✝
[PROOFSTEP]
case nil => rfl
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
⊢ Coe.coe <$> Traversable.traverse f [] = Coe.coe <$> Traversable.traverse f []
[PROOFSTEP]
case nil => rfl
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
⊢ Coe.coe <$> Traversable.traverse f [] = Coe.coe <$> Traversable.traverse f []
[PROOFSTEP]
rfl
[GOAL]
case cons
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x✝ : α'
l₁✝ l₂✝ : List α'
a✝ : l₁✝ ~ l₂✝
a_ih✝ : Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₂✝
⊢ Coe.coe <$> Traversable.traverse f (x✝ :: l₁✝) = Coe.coe <$> Traversable.traverse f (x✝ :: l₂✝)
case swap
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x✝ y✝ : α'
l✝ : List α'
⊢ Coe.coe <$> Traversable.traverse f (y✝ :: x✝ :: l✝) = Coe.coe <$> Traversable.traverse f (x✝ :: y✝ :: l✝)
case trans
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b l₁✝ l₂✝ l₃✝ : List α'
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
a_ih✝¹ : Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₂✝
a_ih✝ : Coe.coe <$> Traversable.traverse f l₂✝ = Coe.coe <$> Traversable.traverse f l₃✝
⊢ Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₃✝
[PROOFSTEP]
case cons x l₁ l₂ _
  h =>
  have :
    Multiset.cons <$> f x <*> Coe.coe <$> Traversable.traverse f l₁ =
      Multiset.cons <$> f x <*> Coe.coe <$> Traversable.traverse f l₂ :=
    by rw [h]
  simpa [functor_norm] using this
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x : α'
l₁ l₂ : List α'
a✝ : l₁ ~ l₂
h : Coe.coe <$> Traversable.traverse f l₁ = Coe.coe <$> Traversable.traverse f l₂
⊢ Coe.coe <$> Traversable.traverse f (x :: l₁) = Coe.coe <$> Traversable.traverse f (x :: l₂)
[PROOFSTEP]
case cons x l₁ l₂ _
  h =>
  have :
    Multiset.cons <$> f x <*> Coe.coe <$> Traversable.traverse f l₁ =
      Multiset.cons <$> f x <*> Coe.coe <$> Traversable.traverse f l₂ :=
    by rw [h]
  simpa [functor_norm] using this
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x : α'
l₁ l₂ : List α'
a✝ : l₁ ~ l₂
h : Coe.coe <$> Traversable.traverse f l₁ = Coe.coe <$> Traversable.traverse f l₂
⊢ Coe.coe <$> Traversable.traverse f (x :: l₁) = Coe.coe <$> Traversable.traverse f (x :: l₂)
[PROOFSTEP]
have :
  Multiset.cons <$> f x <*> Coe.coe <$> Traversable.traverse f l₁ =
    Multiset.cons <$> f x <*> Coe.coe <$> Traversable.traverse f l₂ :=
  by rw [h]
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x : α'
l₁ l₂ : List α'
a✝ : l₁ ~ l₂
h : Coe.coe <$> Traversable.traverse f l₁ = Coe.coe <$> Traversable.traverse f l₂
⊢ (Seq.seq (cons <$> f x) fun x => Coe.coe <$> Traversable.traverse f l₁) =
    Seq.seq (cons <$> f x) fun x => Coe.coe <$> Traversable.traverse f l₂
[PROOFSTEP]
rw [h]
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x : α'
l₁ l₂ : List α'
a✝ : l₁ ~ l₂
h : Coe.coe <$> Traversable.traverse f l₁ = Coe.coe <$> Traversable.traverse f l₂
this :
  (Seq.seq (cons <$> f x) fun x => Coe.coe <$> Traversable.traverse f l₁) =
    Seq.seq (cons <$> f x) fun x => Coe.coe <$> Traversable.traverse f l₂
⊢ Coe.coe <$> Traversable.traverse f (x :: l₁) = Coe.coe <$> Traversable.traverse f (x :: l₂)
[PROOFSTEP]
simpa [functor_norm] using this
[GOAL]
case swap
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x✝ y✝ : α'
l✝ : List α'
⊢ Coe.coe <$> Traversable.traverse f (y✝ :: x✝ :: l✝) = Coe.coe <$> Traversable.traverse f (x✝ :: y✝ :: l✝)
case trans
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b l₁✝ l₂✝ l₃✝ : List α'
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
a_ih✝¹ : Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₂✝
a_ih✝ : Coe.coe <$> Traversable.traverse f l₂✝ = Coe.coe <$> Traversable.traverse f l₃✝
⊢ Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₃✝
[PROOFSTEP]
case 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
    funext a b l
    simpa [flip] using Perm.swap a b l
  simp [(· ∘ ·), this, functor_norm, Coe.coe]
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
⊢ Coe.coe <$> Traversable.traverse f (y :: x :: l) = Coe.coe <$> Traversable.traverse f (x :: y :: l)
[PROOFSTEP]
case 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
    funext a b l
    simpa [flip] using Perm.swap a b l
  simp [(· ∘ ·), this, functor_norm, Coe.coe]
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
⊢ Coe.coe <$> Traversable.traverse f (y :: x :: l) = Coe.coe <$> Traversable.traverse f (x :: y :: l)
[PROOFSTEP]
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
  funext a b l
  simpa [flip] using Perm.swap a b l
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
⊢ (Seq.seq ((fun a b l => ↑(a :: b :: l)) <$> f y) fun x_1 => f x) =
    Seq.seq ((fun a b l => ↑(a :: b :: l)) <$> f x) fun x => f y
[PROOFSTEP]
rw [CommApplicative.commutative_map]
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
⊢ (Seq.seq ((flip fun a b l => ↑(a :: b :: l)) <$> f x) fun x => f y) =
    Seq.seq ((fun a b l => ↑(a :: b :: l)) <$> f x) fun x => f y
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
⊢ (flip fun a b l => ↑(a :: b :: l)) = fun a b l => ↑(a :: b :: l)
[PROOFSTEP]
funext a b l
[GOAL]
case e_a.e_a.h.h.h
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a✝ b✝ : List α'
x y : α'
l✝ : List α'
a b : β'
l : List β'
⊢ flip (fun a b l => ↑(a :: b :: l)) a b l = ↑(a :: b :: l)
[PROOFSTEP]
simpa [flip] using Perm.swap a b l
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
this :
  (Seq.seq ((fun a b l => ↑(a :: b :: l)) <$> f y) fun x_1 => f x) =
    Seq.seq ((fun a b l => ↑(a :: b :: l)) <$> f x) fun x => f y
⊢ Coe.coe <$> Traversable.traverse f (y :: x :: l) = Coe.coe <$> Traversable.traverse f (x :: y :: l)
[PROOFSTEP]
simp [(· ∘ ·), this, functor_norm, Coe.coe]
[GOAL]
case trans
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b l₁✝ l₂✝ l₃✝ : List α'
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
a_ih✝¹ : Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₂✝
a_ih✝ : Coe.coe <$> Traversable.traverse f l₂✝ = Coe.coe <$> Traversable.traverse f l₃✝
⊢ Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₃✝
[PROOFSTEP]
case trans => simp [*]
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b l₁✝ l₂✝ l₃✝ : List α'
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
a_ih✝¹ : Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₂✝
a_ih✝ : Coe.coe <$> Traversable.traverse f l₂✝ = Coe.coe <$> Traversable.traverse f l₃✝
⊢ Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₃✝
[PROOFSTEP]
case trans => simp [*]
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b l₁✝ l₂✝ l₃✝ : List α'
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
a_ih✝¹ : Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₂✝
a_ih✝ : Coe.coe <$> Traversable.traverse f l₂✝ = Coe.coe <$> Traversable.traverse f l₃✝
⊢ Coe.coe <$> Traversable.traverse f l₁✝ = Coe.coe <$> Traversable.traverse f l₃✝
[PROOFSTEP]
simp [*]
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
α✝ : Type ?u.36389
x✝ : Multiset α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
simp only [fmap_def, id_eq, map_id']
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
α✝ β✝ : Type ?u.36389
x✝¹ : α✝
x✝ : α✝ → Multiset β✝
⊢ pure x✝¹ >>= x✝ = x✝ x✝¹
[PROOFSTEP]
simp only [pure_def, bind_def, singleton_bind]
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
α✝ β✝ : Type ?u.36389
x✝¹ : α✝ → β✝
x✝ : Multiset α✝
⊢ (do
      let y ← x✝
      pure (x✝¹ y)) =
    x✝¹ <$> x✝
[PROOFSTEP]
simp only [pure_def, bind_def, bind_singleton, fmap_def]
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
α β : Type u_1
h : α → β
⊢ Functor.map h ∘ Coe.coe = Coe.coe ∘ Functor.map h
[PROOFSTEP]
funext
[GOAL]
case h
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
α β : Type u_1
h : α → β
x✝ : List α
⊢ (Functor.map h ∘ Coe.coe) x✝ = (Coe.coe ∘ Functor.map h) x✝
[PROOFSTEP]
simp only [Function.comp_apply, Coe.coe, fmap_def, coe_map, List.map_eq_map]
[GOAL]
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
α : Type u_1
x : Multiset α
⊢ traverse pure x = x
[PROOFSTEP]
refine' Quotient.inductionOn x _
[GOAL]
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
[PROOFSTEP]
intro
[GOAL]
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✝
[PROOFSTEP]
simp [traverse, Coe.coe]
[GOAL]
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)
[PROOFSTEP]
refine' Quotient.inductionOn x _
[GOAL]
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))
[PROOFSTEP]
intro
[GOAL]
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✝))
[PROOFSTEP]
simp only [traverse, quot_mk_to_coe, lift_coe, Coe.coe, Function.comp_apply, Functor.map_map, functor_norm]
[GOAL]
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✝)
[PROOFSTEP]
simp only [Function.comp, lift_coe]
[GOAL]
F : Type u → Type u
inst✝³ : Applicative F
inst✝² : CommApplicative F
α' β' : Type u
f : α' → F β'
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
x : Multiset α
⊢ Functor.map h <$> traverse g x = traverse (Functor.map h ∘ g) x
[PROOFSTEP]
refine' Quotient.inductionOn x _
[GOAL]
F : Type u → Type u
inst✝³ : Applicative F
inst✝² : CommApplicative F
α' β' : Type u
f : α' → F β'
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
x : Multiset α
⊢ ∀ (a : List α),
    Functor.map h <$> traverse g (Quotient.mk (isSetoid α) a) =
      traverse (Functor.map h ∘ g) (Quotient.mk (isSetoid α) a)
[PROOFSTEP]
intro
[GOAL]
F : Type u → Type u
inst✝³ : Applicative F
inst✝² : CommApplicative F
α' β' : Type u
f : α' → F β'
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
x : Multiset α
a✝ : List α
⊢ Functor.map h <$> traverse g (Quotient.mk (isSetoid α) a✝) =
    traverse (Functor.map h ∘ g) (Quotient.mk (isSetoid α) a✝)
[PROOFSTEP]
simp only [traverse, quot_mk_to_coe, lift_coe, Function.comp_apply, Functor.map_map, map_comp_coe]
[GOAL]
F : Type u → Type u
inst✝³ : Applicative F
inst✝² : CommApplicative F
α' β' : Type u
f : α' → F β'
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
x : Multiset α
a✝ : List α
⊢ (Coe.coe ∘ Functor.map h) <$> Traversable.traverse g a✝ = Coe.coe <$> Traversable.traverse (Functor.map h ∘ g) a✝
[PROOFSTEP]
rw [LawfulFunctor.comp_map, Traversable.map_traverse']
[GOAL]
F : Type u → Type u
inst✝³ : Applicative F
inst✝² : CommApplicative F
α' β' : Type u
f : α' → F β'
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
x : Multiset α
a✝ : List α
⊢ Coe.coe <$> Functor.map h <$> Traversable.traverse g a✝ =
    Coe.coe <$> (Functor.map (Functor.map h) ∘ Traversable.traverse g) a✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u → Type u
inst✝³ : Applicative F
inst✝² : CommApplicative F
α' β' : Type u
f : α' → F β'
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
x : Multiset α
⊢ traverse h (map g x) = traverse (h ∘ g) x
[PROOFSTEP]
refine' Quotient.inductionOn x _
[GOAL]
F : Type u → Type u
inst✝³ : Applicative F
inst✝² : CommApplicative F
α' β' : Type u
f : α' → F β'
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
x : Multiset α
⊢ ∀ (a : List α), traverse h (map g (Quotient.mk (isSetoid α) a)) = traverse (h ∘ g) (Quotient.mk (isSetoid α) a)
[PROOFSTEP]
intro
[GOAL]
F : Type u → Type u
inst✝³ : Applicative F
inst✝² : CommApplicative F
α' β' : Type u
f : α' → F β'
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
x : Multiset α
a✝ : List α
⊢ traverse h (map g (Quotient.mk (isSetoid α) a✝)) = traverse (h ∘ g) (Quotient.mk (isSetoid α) a✝)
[PROOFSTEP]
simp only [traverse, quot_mk_to_coe, coe_map, lift_coe, Function.comp_apply]
[GOAL]
F : Type u → Type u
inst✝³ : Applicative F
inst✝² : CommApplicative F
α' β' : Type u
f : α' → F β'
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
x : Multiset α
a✝ : List α
⊢ Coe.coe <$> Traversable.traverse h (List.map g a✝) = Coe.coe <$> Traversable.traverse (h ∘ g) a✝
[PROOFSTEP]
rw [← Traversable.traverse_map h g, List.map_eq_map]
[GOAL]
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
[PROOFSTEP]
refine' Quotient.inductionOn x _
[GOAL]
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)
[PROOFSTEP]
intro
[GOAL]
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✝)
[PROOFSTEP]
simp only [quot_mk_to_coe, traverse, lift_coe, Function.comp_apply, ApplicativeTransformation.preserves_map,
  LawfulTraversable.naturality]
