ι : 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 k₀ : ι
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
hk₀' : ∀ (l : ι), ¬ComplexShape.Rel c l k₀
hom : (i j : ι) → X C i ⟶ X D j
⊢ d C k₀ (ComplexShape.next c k₀) ≫ hom (ComplexShape.next c k₀) k₀ +
      hom k₀ (ComplexShape.prev c k₀) ≫ d D (ComplexShape.prev c k₀) k₀ =
    0
ι : 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 k₀ : ι
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
hk₀' : ∀ (l : ι), ¬ComplexShape.Rel c l k₀
hom : (i j : ι) → X C i ⟶ X D j
⊢ Hom.f (nullHomotopicMap hom) k₀ = 0
dsimp [nullHomotopicMap, dNext, prevD]
no goals
ι : 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 k₀ : ι
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
hk₀' : ∀ (l : ι), ¬ComplexShape.Rel c l k₀
hom : (i j : ι) → X C i ⟶ X D j
⊢ d C k₀ (ComplexShape.next c k₀) ≫ hom (ComplexShape.next c k₀) k₀ +
      hom k₀ (ComplexShape.prev c k₀) ≫ d D (ComplexShape.prev c k₀) k₀ =
    0
rw [C.shape, D.shape, zero_comp, comp_zero, add_zero] <;> apply_assumption