Theorem: CategoryTheory.List.joinF.associatorLeft_cons_cons_cons (Moncalc/CategoryTheory/List/Monad.lean)

State before:
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ joinF.associatorLeft (((a :: as) :: ass) :: asss) = DVect2.cons (𝟙 a) (joinF.associatorLeft ((as :: ass) :: asss))
Tactic:
unfold joinF.associatorLeft
State after:
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ associatorLeft.aux [] [] (((a :: as) :: ass) :: asss) =
    DVect2.cons (𝟙 a) (associatorLeft.aux [] [] ((as :: ass) :: asss))

State before:
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ associatorLeft.aux [] [] (((a :: as) :: ass) :: asss) =
    DVect2.cons (𝟙 a) (associatorLeft.aux [] [] ((as :: ass) :: asss))
Tactic:
unfold joinF.associatorLeft.aux
State after:
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ associatorLeft.aux [] ((a :: as) :: ass) asss = DVect2.cons (𝟙 a) (associatorLeft.aux [] (as :: ass) asss)

State before:
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ associatorLeft.aux [] ((a :: as) :: ass) asss = DVect2.cons (𝟙 a) (associatorLeft.aux [] (as :: ass) asss)
Tactic:
unfold joinF.associatorLeft.aux
State after:
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ associatorLeft.aux (a :: as) ass asss = DVect2.cons (𝟙 a) (associatorLeft.aux as ass asss)

State before:
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ associatorLeft.aux (a :: as) ass asss = DVect2.cons (𝟙 a) (associatorLeft.aux as ass asss)
Tactic:
conv => lhs; unfold joinF.associatorLeft.aux
State after:
no goals