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 : ι
f : C ⟶ D
hom : (i j : ι) → X D i ⟶ X E j
n : ι
⊢ Hom.f (f ≫ nullHomotopicMap hom) n = Hom.f (nullHomotopicMap fun i j => Hom.f f i ≫ hom i 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 : ι
f : C ⟶ D
hom : (i j : ι) → X D i ⟶ X E j
⊢ f ≫ nullHomotopicMap hom = nullHomotopicMap fun i j => Hom.f f i ≫ hom i 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 : ι
f : C ⟶ D
hom : (i j : ι) → X D i ⟶ X E j
n : ι
⊢ Hom.f f n ≫ (dFrom D n ≫ hom (ComplexShape.next c n) n + hom n (ComplexShape.prev c n) ≫ dTo E n) =
    dFrom C n ≫ Hom.f f (ComplexShape.next c n) ≫ hom (ComplexShape.next c n) n +
      (Hom.f f n ≫ hom n (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 : ι
f : C ⟶ D
hom : (i j : ι) → X D i ⟶ X E j
n : ι
⊢ Hom.f (f ≫ nullHomotopicMap hom) n = Hom.f (nullHomotopicMap fun i j => Hom.f f i ≫ hom i 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 : ι
f : C ⟶ D
hom : (i j : ι) → X D i ⟶ X E j
n : ι
⊢ Hom.f f n ≫ (dFrom D n ≫ hom (ComplexShape.next c n) n + hom n (ComplexShape.prev c n) ≫ dTo E n) =
    dFrom C n ≫ Hom.f f (ComplexShape.next c n) ≫ hom (ComplexShape.next c n) n +
      (Hom.f f n ≫ hom n (ComplexShape.prev c n)) ≫ dTo E n
simp only [Preadditive.comp_add, Category.assoc, f.comm_assoc]