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