α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : List α
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) xs) = xs
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : List α
⊢ toList xs = xs
simp only [toList_spec, foldMap, traverse]
case nil
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) []) = []

case cons
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
head✝ : α
tail✝ : List α
tail_ih✝ : ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) = head✝ :: tail✝
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
xs : List α
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) xs) = xs
induction xs
case cons
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
head✝ : α
tail✝ : List α
tail_ih✝ : ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) = head✝ :: tail✝
case nil
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) []) = []

case cons
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
head✝ : α
tail✝ : List α
tail_ih✝ : ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) = head✝ :: tail✝
case nil => rfl
no goals
case cons
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
head✝ : α
tail✝ : List α
tail_ih✝ : ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) = head✝ :: tail✝
case cons _ _ ih => conv_rhs => rw [← ih]; rfl
no goals
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) []) = []
rfl
no goals
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : IsLawfulTraversable t
head✝ : α
tail✝ : List α
ih : ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ ↑FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) = head✝ :: tail✝
conv_rhs => rw [← ih]; rfl