ι : Type ?u.303893
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
i : ℕ
⊢ d P (i + 1) (ComplexShape.next (ComplexShape.down ℕ) (i + 1)) ≫
      f (ComplexShape.next (ComplexShape.down ℕ) (i + 1)) (i + 1) =
    d P (i + 1) i ≫ f i (i + 1)
ι : Type ?u.303893
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
i : ℕ
⊢ ↑(dNext (i + 1)) f = d P (i + 1) i ≫ f i (i + 1)
dsimp [dNext]
ι : Type ?u.303893
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
i : ℕ
this : ComplexShape.next (ComplexShape.down ℕ) (i + 1) = i
⊢ d P (i + 1) (ComplexShape.next (ComplexShape.down ℕ) (i + 1)) ≫
      f (ComplexShape.next (ComplexShape.down ℕ) (i + 1)) (i + 1) =
    d P (i + 1) i ≫ f i (i + 1)
ι : Type ?u.303893
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
i : ℕ
⊢ d P (i + 1) (ComplexShape.next (ComplexShape.down ℕ) (i + 1)) ≫
      f (ComplexShape.next (ComplexShape.down ℕ) (i + 1)) (i + 1) =
    d P (i + 1) i ≫ f i (i + 1)
have : (ComplexShape.down ℕ).next (i + 1) = i := ChainComplex.next_nat_succ _
no goals
ι : Type ?u.303893
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
i : ℕ
this : ComplexShape.next (ComplexShape.down ℕ) (i + 1) = i
⊢ d P (i + 1) (ComplexShape.next (ComplexShape.down ℕ) (i + 1)) ≫
      f (ComplexShape.next (ComplexShape.down ℕ) (i + 1)) (i + 1) =
    d P (i + 1) i ≫ f i (i + 1)
congr 2