Theorem: CategoryTheory.List.assoc (Moncalc/CategoryTheory/List/Basic.lean)

State before:
α : Type u
inst✝ : Category α
head✝³ : α
tail✝³ : List α
head✝² : α
tail✝² : List α
head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
f : head✝³ ⟶ head✝²
fs : DVect2 Quiver.Hom tail✝³ tail✝²
g : head✝² ⟶ head✝¹
gs : DVect2 Quiver.Hom tail✝² tail✝¹
h : head✝¹ ⟶ head✝
hs : DVect2 Quiver.Hom tail✝¹ tail✝
⊢ List.comp (List.comp (DVect2.cons f fs) (DVect2.cons g gs)) (DVect2.cons h hs) =
    List.comp (DVect2.cons f fs) (List.comp (DVect2.cons g gs) (DVect2.cons h hs))
Tactic:
dsimp
State after:
α : Type u
inst✝ : Category α
head✝³ : α
tail✝³ : List α
head✝² : α
tail✝² : List α
head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
f : head✝³ ⟶ head✝²
fs : DVect2 Quiver.Hom tail✝³ tail✝²
g : head✝² ⟶ head✝¹
gs : DVect2 Quiver.Hom tail✝² tail✝¹
h : head✝¹ ⟶ head✝
hs : DVect2 Quiver.Hom tail✝¹ tail✝
⊢ DVect2.cons ((f ≫ g) ≫ h) (List.comp (List.comp fs gs) hs) = DVect2.cons (f ≫ g ≫ h) (List.comp fs (List.comp gs hs))

State before:
α : Type u
inst✝ : Category α
head✝³ : α
tail✝³ : List α
head✝² : α
tail✝² : List α
head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
f : head✝³ ⟶ head✝²
fs : DVect2 Quiver.Hom tail✝³ tail✝²
g : head✝² ⟶ head✝¹
gs : DVect2 Quiver.Hom tail✝² tail✝¹
h : head✝¹ ⟶ head✝
hs : DVect2 Quiver.Hom tail✝¹ tail✝
⊢ DVect2.cons ((f ≫ g) ≫ h) (List.comp (List.comp fs gs) hs) = DVect2.cons (f ≫ g ≫ h) (List.comp fs (List.comp gs hs))
Tactic:
rw [Category.assoc, List.assoc fs gs hs]
State after:
no goals