no goals
C : Type u
inst✝⁵ : Category C
D : Type u
inst✝⁴ : Category D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
P : InjectiveResolution X
inst✝ : PreservesFiniteLimits F
⊢ (Iso.refl (F.obj (HomologicalComplex.X ((CochainComplex.single₀ C).obj X) 0))).hom ≫
      F.map (HomologicalComplex.Hom.f P.ι 0) =
    F.map (HomologicalComplex.Hom.f P.ι 0) ≫ (Iso.refl (F.obj (HomologicalComplex.X P.cocomplex 0))).hom
simp
no goals
C : Type u
inst✝⁵ : Category C
D : Type u
inst✝⁴ : Category D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
P : InjectiveResolution X
inst✝ : PreservesFiniteLimits F
⊢ (Iso.refl (F.obj (HomologicalComplex.X P.cocomplex 0))).hom ≫
      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
    F.map (HomologicalComplex.d P.cocomplex 0 1) ≫
      (HomologicalComplex.xNextIso ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
            (_ : 0 + 1 = 0 + 1)).symm.hom
rw [Iso.refl_hom, Category.id_comp, Iso.symm_hom, HomologicalComplex.dFrom_eq] <;> congr