C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
⊢ f.app [n].op ≫ 𝟙 (HomologicalComplex.X K[Y] n) = 𝟙 (HomologicalComplex.X K[X] n) ≫ f.app [n].op
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
⊢ f.app [n].op ≫ HomologicalComplex.Hom.f (Q q) n = HomologicalComplex.Hom.f (Q q) n ≫ f.app [n].op
simp only [Q, HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, comp_sub, P_f_naturality,
  sub_comp, sub_left_inj]
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
⊢ f.app [n].op ≫ 𝟙 (Y.obj [n].op) = 𝟙 (X.obj [n].op) ≫ f.app [n].op
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
⊢ f.app [n].op ≫ 𝟙 (HomologicalComplex.X K[Y] n) = 𝟙 (HomologicalComplex.X K[X] n) ≫ f.app [n].op
dsimp
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
⊢ f.app [n].op ≫ 𝟙 (Y.obj [n].op) = 𝟙 (X.obj [n].op) ≫ f.app [n].op
simp only [comp_id, id_comp]