ι : Type ?u.115833
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✝ : ι
C D : CochainComplex V ℕ
i : ℕ
f : (i j : ℕ) → X C i ⟶ X D j
⊢ f i (ComplexShape.prev (ComplexShape.up ℕ) i) ≫ d D (ComplexShape.prev (ComplexShape.up ℕ) i) i =
    f i (i - 1) ≫ d D (i - 1) i
ι : Type ?u.115833
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✝ : ι
C D : CochainComplex V ℕ
i : ℕ
f : (i j : ℕ) → X C i ⟶ X D j
⊢ ↑(prevD i) f = f i (i - 1) ≫ d D (i - 1) i
dsimp [prevD]
case zero
ι : Type ?u.115833
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 : ι
C D : CochainComplex V ℕ
f : (i j : ℕ) → X C i ⟶ X D j
⊢ f Nat.zero (ComplexShape.prev (ComplexShape.up ℕ) Nat.zero) ≫
      d D (ComplexShape.prev (ComplexShape.up ℕ) Nat.zero) Nat.zero =
    f Nat.zero (Nat.zero - 1) ≫ d D (Nat.zero - 1) Nat.zero

case succ
ι : Type ?u.115833
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 : ι
C D : CochainComplex V ℕ
f : (i j : ℕ) → X C i ⟶ X D j
n✝ : ℕ
⊢ f (Nat.succ n✝) (ComplexShape.prev (ComplexShape.up ℕ) (Nat.succ n✝)) ≫
      d D (ComplexShape.prev (ComplexShape.up ℕ) (Nat.succ n✝)) (Nat.succ n✝) =
    f (Nat.succ n✝) (Nat.succ n✝ - 1) ≫ d D (Nat.succ n✝ - 1) (Nat.succ n✝)
ι : Type ?u.115833
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✝ : ι
C D : CochainComplex V ℕ
i : ℕ
f : (i j : ℕ) → X C i ⟶ X D j
⊢ f i (ComplexShape.prev (ComplexShape.up ℕ) i) ≫ d D (ComplexShape.prev (ComplexShape.up ℕ) i) i =
    f i (i - 1) ≫ d D (i - 1) i
cases i
no goals
case succ
ι : Type ?u.115833
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 : ι
C D : CochainComplex V ℕ
f : (i j : ℕ) → X C i ⟶ X D j
n✝ : ℕ
⊢ f (Nat.succ n✝) (ComplexShape.prev (ComplexShape.up ℕ) (Nat.succ n✝)) ≫
      d D (ComplexShape.prev (ComplexShape.up ℕ) (Nat.succ n✝)) (Nat.succ n✝) =
    f (Nat.succ n✝) (Nat.succ n✝ - 1) ≫ d D (Nat.succ n✝ - 1) (Nat.succ n✝)
. congr <;> simp
no goals
case zero
ι : Type ?u.115833
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 : ι
C D : CochainComplex V ℕ
f : (i j : ℕ) → X C i ⟶ X D j
⊢ f Nat.zero (ComplexShape.prev (ComplexShape.up ℕ) Nat.zero) ≫
      d D (ComplexShape.prev (ComplexShape.up ℕ) Nat.zero) Nat.zero =
    f Nat.zero (Nat.zero - 1) ≫ d D (Nat.zero - 1) Nat.zero
simp only [shape, CochainComplex.prev_nat_zero, ComplexShape.up_Rel, Nat.one_ne_zero,
  not_false_iff, comp_zero]
no goals
case succ
ι : Type ?u.115833
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 : ι
C D : CochainComplex V ℕ
f : (i j : ℕ) → X C i ⟶ X D j
n✝ : ℕ
⊢ f (Nat.succ n✝) (ComplexShape.prev (ComplexShape.up ℕ) (Nat.succ n✝)) ≫
      d D (ComplexShape.prev (ComplexShape.up ℕ) (Nat.succ n✝)) (Nat.succ n✝) =
    f (Nat.succ n✝) (Nat.succ n✝ - 1) ≫ d D (Nat.succ n✝ - 1) (Nat.succ n✝)
congr <;> simp