ι : Type ?u.373772
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
i : ℕ
⊢ f (i + 1) (ComplexShape.prev (ComplexShape.up ℕ) (i + 1)) ≫
      d Q (ComplexShape.prev (ComplexShape.up ℕ) (i + 1)) (i + 1) =
    f (i + 1) i ≫ d Q i (i + 1)
ι : Type ?u.373772
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
i : ℕ
⊢ ↑(prevD (i + 1)) f = f (i + 1) i ≫ d Q i (i + 1)
dsimp [prevD]
ι : Type ?u.373772
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
i : ℕ
this : ComplexShape.prev (ComplexShape.up ℕ) (i + 1) = i
⊢ f (i + 1) (ComplexShape.prev (ComplexShape.up ℕ) (i + 1)) ≫
      d Q (ComplexShape.prev (ComplexShape.up ℕ) (i + 1)) (i + 1) =
    f (i + 1) i ≫ d Q i (i + 1)
ι : Type ?u.373772
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
i : ℕ
⊢ f (i + 1) (ComplexShape.prev (ComplexShape.up ℕ) (i + 1)) ≫
      d Q (ComplexShape.prev (ComplexShape.up ℕ) (i + 1)) (i + 1) =
    f (i + 1) i ≫ d Q i (i + 1)
have : (ComplexShape.up ℕ).prev (i + 1) = i := CochainComplex.prev_nat_succ i
no goals
ι : Type ?u.373772
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
i : ℕ
this : ComplexShape.prev (ComplexShape.up ℕ) (i + 1) = i
⊢ f (i + 1) (ComplexShape.prev (ComplexShape.up ℕ) (i + 1)) ≫
      d Q (ComplexShape.prev (ComplexShape.up ℕ) (i + 1)) (i + 1) =
    f (i + 1) i ≫ d Q i (i + 1)
congr 2