ι : Type ?u.294299
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 : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
j : ℕ
⊢ f j (ComplexShape.prev (ComplexShape.down ℕ) j) ≫ d Q (ComplexShape.prev (ComplexShape.down ℕ) j) j =
    f j (j + 1) ≫ d Q (j + 1) j
ι : Type ?u.294299
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 : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
j : ℕ
⊢ ↑(prevD j) f = f j (j + 1) ≫ d Q (j + 1) j
dsimp [prevD]
ι : Type ?u.294299
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 : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
j : ℕ
this : ComplexShape.prev (ComplexShape.down ℕ) j = j + 1
⊢ f j (ComplexShape.prev (ComplexShape.down ℕ) j) ≫ d Q (ComplexShape.prev (ComplexShape.down ℕ) j) j =
    f j (j + 1) ≫ d Q (j + 1) j
ι : Type ?u.294299
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 : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
j : ℕ
⊢ f j (ComplexShape.prev (ComplexShape.down ℕ) j) ≫ d Q (ComplexShape.prev (ComplexShape.down ℕ) j) j =
    f j (j + 1) ≫ d Q (j + 1) j
have : (ComplexShape.down ℕ).prev j = j + 1 := ChainComplex.prev ℕ j
no goals
ι : Type ?u.294299
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 : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
j : ℕ
this : ComplexShape.prev (ComplexShape.down ℕ) j = j + 1
⊢ f j (ComplexShape.prev (ComplexShape.down ℕ) j) ≫ d Q (ComplexShape.prev (ComplexShape.down ℕ) j) j =
    f j (j + 1) ≫ d Q (j + 1) j
congr 2