Theorem: CategoryTheory.List.joinF.associatorRight_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.associatorRight (((a :: as) :: ass) :: asss) = DVect2.cons (𝟙 a) (joinF.associatorRight ((as :: ass) :: asss))
Tactic:
unfold joinF.associatorRight
State after:
α : Type u
inst✝ : Category α
a : α
as : List α
ass : List (List α)
asss : List (List (List α))
⊢ associatorRight.aux [] [] (((a :: as) :: ass) :: asss) =
    DVect2.cons (𝟙 a) (associatorRight.aux [] [] ((as :: ass) :: asss))

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

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

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