Theorem: CategoryTheory.List.comp_cons' (Moncalc/CategoryTheory/List/Basic.lean)

State before:
α : Type u
inst✝ : Category α
⊢ ∀ {a b c : α} {as bs cs : List α} {f : a ⟶ b} {fs : Hom as bs} {g : b ⟶ c} {gs : Hom bs cs},
    List.comp (DVect2.cons f fs) (DVect2.cons g gs) = DVect2.cons (f ≫ g) (List.comp fs gs)
Tactic:
intros
State after:
α : Type u
inst✝ : Category α
a✝ b✝ c✝ : α
as✝ bs✝ cs✝ : List α
f✝ : a✝ ⟶ b✝
fs✝ : Hom as✝ bs✝
g✝ : b✝ ⟶ c✝
gs✝ : Hom bs✝ cs✝
⊢ List.comp (DVect2.cons f✝ fs✝) (DVect2.cons g✝ gs✝) = DVect2.cons (f✝ ≫ g✝) (List.comp fs✝ gs✝)

State before:
α : Type u
inst✝ : Category α
a✝ b✝ c✝ : α
as✝ bs✝ cs✝ : List α
f✝ : a✝ ⟶ b✝
fs✝ : Hom as✝ bs✝
g✝ : b✝ ⟶ c✝
gs✝ : Hom bs✝ cs✝
⊢ List.comp (DVect2.cons f✝ fs✝) (DVect2.cons g✝ gs✝) = DVect2.cons (f✝ ≫ g✝) (List.comp fs✝ gs✝)
Tactic:
rfl
State after:
no goals