case h
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g✝ : C ⟶ D
h k : D ⟶ E
i : ι
hom : (i j : ι) → X C i ⟶ X D j
g : D ⟶ E
n : ι
⊢ Hom.f (nullHomotopicMap hom ≫ g) n = Hom.f (nullHomotopicMap fun i j => hom i j ≫ Hom.f g j) n
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g✝ : C ⟶ D
h k : D ⟶ E
i : ι
hom : (i j : ι) → X C i ⟶ X D j
g : D ⟶ E
⊢ nullHomotopicMap hom ≫ g = nullHomotopicMap fun i j => hom i j ≫ Hom.f g j
ext n
case h
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g✝ : C ⟶ D
h k : D ⟶ E
i : ι
hom : (i j : ι) → X C i ⟶ X D j
g : D ⟶ E
n : ι
⊢ (dFrom C n ≫ hom (ComplexShape.next c n) n + hom n (ComplexShape.prev c n) ≫ dTo D n) ≫ Hom.f g n =
    dFrom C n ≫ hom (ComplexShape.next c n) n ≫ Hom.f g n +
      (hom n (ComplexShape.prev c n) ≫ Hom.f g (ComplexShape.prev c n)) ≫ dTo E n
case h
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g✝ : C ⟶ D
h k : D ⟶ E
i : ι
hom : (i j : ι) → X C i ⟶ X D j
g : D ⟶ E
n : ι
⊢ Hom.f (nullHomotopicMap hom ≫ g) n = Hom.f (nullHomotopicMap fun i j => hom i j ≫ Hom.f g j) n
dsimp [nullHomotopicMap, fromNext, toPrev, AddMonoidHom.mk'_apply]
no goals
case h
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g✝ : C ⟶ D
h k : D ⟶ E
i : ι
hom : (i j : ι) → X C i ⟶ X D j
g : D ⟶ E
n : ι
⊢ (dFrom C n ≫ hom (ComplexShape.next c n) n + hom n (ComplexShape.prev c n) ≫ dTo D n) ≫ Hom.f g n =
    dFrom C n ≫ hom (ComplexShape.next c n) n ≫ Hom.f g n +
      (hom n (ComplexShape.prev c n) ≫ Hom.f g (ComplexShape.prev c n)) ≫ dTo E n
simp only [Preadditive.add_comp, Category.assoc, g.comm]