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

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

State before:
α : Type u
inst✝ : Category α
ass : List (List α)
asss : List (List (List α))
⊢ associatorRight.aux [] [] (([] :: ass) :: asss) = associatorRight.aux [] [] (ass :: asss)
Tactic:
conv => lhs; unfold associatorRight.aux; unfold associatorRight.aux
State after:
no goals