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

State before:
α : Type u
inst✝ : Category α
⊢ joinF ⋙ joinF = Prefunctor.obj mapF.toPrefunctor joinF ⋙ joinF
Tactic:
dsimp [Functor.comp, joinF, mapF]
State after:
α : Type u
inst✝ : Category α
⊢ Functor.mk { obj := fun X ↦ List.join (List.join X), map := fun {X Y} f ↦ DVect2.join (DVect2.join f) } =
    Functor.mk
      { obj := fun X ↦ List.join (List.map List.join X),
        map := fun {X Y} f ↦ DVect2.join (DVect2.map List.join List.join (fun {a b} ↦ DVect2.join) f) }

State before:
α : Type u
inst✝ : Category α
⊢ Functor.mk { obj := fun X ↦ List.join (List.join X), map := fun {X Y} f ↦ DVect2.join (DVect2.join f) } =
    Functor.mk
      { obj := fun X ↦ List.join (List.map List.join X),
        map := fun {X Y} f ↦ DVect2.join (DVect2.map List.join List.join (fun {a b} ↦ DVect2.join) f) }
Tactic:
apply eqF_List <;> dsimp
State after:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a : List (List (List α))), List.join (List.join a) = List.join (List.map List.join a)

case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List (List (List α))) (f : a₁ ⟶ a₂),
    DVect2.Eq (DVect2.join (DVect2.join f)) (DVect2.join (DVect2.map List.join List.join (fun {a b} ↦ DVect2.join) f))

State before:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a : List (List (List α))), List.join (List.join a) = List.join (List.map List.join a)

case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List (List (List α))) (f : a₁ ⟶ a₂),
    DVect2.Eq (DVect2.join (DVect2.join f)) (DVect2.join (DVect2.map List.join List.join (fun {a b} ↦ DVect2.join) f))
Tactic:
. intros; exact List.join_join _
State after:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List (List (List α))) (f : a₁ ⟶ a₂),
    DVect2.Eq (DVect2.join (DVect2.join f)) (DVect2.join (DVect2.map List.join List.join (fun {a b} ↦ DVect2.join) f))

State before:
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List (List (List α))) (f : a₁ ⟶ a₂),
    DVect2.Eq (DVect2.join (DVect2.join f)) (DVect2.join (DVect2.map List.join List.join (fun {a b} ↦ DVect2.join) f))
Tactic:
. intros; exact DVect2.join_join _
State after:
no goals