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

State before:
α : Type u
inst✝ : Category α
head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
f : head✝¹ ⟶ head✝
fs : DVect2 Quiver.Hom tail✝¹ tail✝
⊢ List.comp (List.id (head✝¹ :: tail✝¹)) (DVect2.cons f fs) = DVect2.cons f fs
Tactic:
dsimp
State after:
α : Type u
inst✝ : Category α
head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
f : head✝¹ ⟶ head✝
fs : DVect2 Quiver.Hom tail✝¹ tail✝
⊢ DVect2.cons (𝟙 head✝¹ ≫ f) (List.comp (List.id tail✝¹) fs) = DVect2.cons f fs

State before:
α : Type u
inst✝ : Category α
head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
f : head✝¹ ⟶ head✝
fs : DVect2 Quiver.Hom tail✝¹ tail✝
⊢ DVect2.cons (𝟙 head✝¹ ≫ f) (List.comp (List.id tail✝¹) fs) = DVect2.cons f fs
Tactic:
rw [Category.id_comp, List.id_comp fs]
State after:
no goals