Theorem: CategoryTheory.List.appendF.map_comp (Moncalc/CategoryTheory/List/Basic.lean)

State before:
α : Type u
inst✝ : Category α
head✝² : α
tail✝² x✝² : List α
head✝¹ : α
tail✝¹ x✝¹ : List α
head✝ : α
tail✝ x✝ : List α
f : head✝² ⟶ head✝¹
fs₁ : DVect2 Quiver.Hom tail✝² tail✝¹
fs₂ : Hom x✝² x✝¹
g : head✝¹ ⟶ head✝
gs₁ : DVect2 Quiver.Hom tail✝¹ tail✝
gs₂ : Hom x✝¹ x✝
⊢ (DVect2.cons f fs₁ ++ fs₂) ≫ (DVect2.cons g gs₁ ++ gs₂) = DVect2.cons f fs₁ ≫ DVect2.cons g gs₁ ++ fs₂ ≫ gs₂
Tactic:
rw [DVect2.cons_append, DVect2.cons_append]
State after:
α : Type u
inst✝ : Category α
head✝² : α
tail✝² x✝² : List α
head✝¹ : α
tail✝¹ x✝¹ : List α
head✝ : α
tail✝ x✝ : List α
f : head✝² ⟶ head✝¹
fs₁ : DVect2 Quiver.Hom tail✝² tail✝¹
fs₂ : Hom x✝² x✝¹
g : head✝¹ ⟶ head✝
gs₁ : DVect2 Quiver.Hom tail✝¹ tail✝
gs₂ : Hom x✝¹ x✝
⊢ DVect2.cons f (fs₁ ++ fs₂) ≫ DVect2.cons g (gs₁ ++ gs₂) = DVect2.cons f fs₁ ≫ DVect2.cons g gs₁ ++ fs₂ ≫ gs₂

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

State before:
α : Type u
inst✝ : Category α
head✝² : α
tail✝² x✝² : List α
head✝¹ : α
tail✝¹ x✝¹ : List α
head✝ : α
tail✝ x✝ : List α
f : head✝² ⟶ head✝¹
fs₁ : DVect2 Quiver.Hom tail✝² tail✝¹
fs₂ : Hom x✝² x✝¹
g : head✝¹ ⟶ head✝
gs₁ : DVect2 Quiver.Hom tail✝¹ tail✝
gs₂ : Hom x✝¹ x✝
⊢ DVect2.cons (f ≫ g) ((fs₁ ++ fs₂) ≫ (gs₁ ++ gs₂)) = DVect2.cons (f ≫ g) (fs₁ ≫ gs₁) ++ fs₂ ≫ gs₂
Tactic:
rw [appendF.map_comp fs₁ _ gs₁ _, DVect2.cons_append]
State after:
no goals