ι : Type ?u.103173
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 : ChainComplex V ℕ
i : ℕ
f : (i j : ℕ) → X C i ⟶ X D j
⊢ d C i (ComplexShape.next (ComplexShape.down ℕ) i) ≫ f (ComplexShape.next (ComplexShape.down ℕ) i) i =
    d C i (i - 1) ≫ f (i - 1) i
ι : Type ?u.103173
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 : ChainComplex V ℕ
i : ℕ
f : (i j : ℕ) → X C i ⟶ X D j
⊢ ↑(dNext i) f = d C i (i - 1) ≫ f (i - 1) i
dsimp [dNext]
case zero
ι : Type ?u.103173
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 : ChainComplex V ℕ
f : (i j : ℕ) → X C i ⟶ X D j
⊢ d C Nat.zero (ComplexShape.next (ComplexShape.down ℕ) Nat.zero) ≫
      f (ComplexShape.next (ComplexShape.down ℕ) Nat.zero) Nat.zero =
    d C Nat.zero (Nat.zero - 1) ≫ f (Nat.zero - 1) Nat.zero

case succ
ι : Type ?u.103173
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 : ChainComplex V ℕ
f : (i j : ℕ) → X C i ⟶ X D j
n✝ : ℕ
⊢ d C (Nat.succ n✝) (ComplexShape.next (ComplexShape.down ℕ) (Nat.succ n✝)) ≫
      f (ComplexShape.next (ComplexShape.down ℕ) (Nat.succ n✝)) (Nat.succ n✝) =
    d C (Nat.succ n✝) (Nat.succ n✝ - 1) ≫ f (Nat.succ n✝ - 1) (Nat.succ n✝)
ι : Type ?u.103173
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 : ChainComplex V ℕ
i : ℕ
f : (i j : ℕ) → X C i ⟶ X D j
⊢ d C i (ComplexShape.next (ComplexShape.down ℕ) i) ≫ f (ComplexShape.next (ComplexShape.down ℕ) i) i =
    d C i (i - 1) ≫ f (i - 1) i
cases i
no goals
case zero
ι : Type ?u.103173
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 : ChainComplex V ℕ
f : (i j : ℕ) → X C i ⟶ X D j
⊢ d C Nat.zero (ComplexShape.next (ComplexShape.down ℕ) Nat.zero) ≫
      f (ComplexShape.next (ComplexShape.down ℕ) Nat.zero) Nat.zero =
    d C Nat.zero (Nat.zero - 1) ≫ f (Nat.zero - 1) Nat.zero
simp only [shape, ChainComplex.next_nat_zero, ComplexShape.down_Rel, Nat.one_ne_zero,
  not_false_iff, zero_comp]
no goals
case succ
ι : Type ?u.103173
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 : ChainComplex V ℕ
f : (i j : ℕ) → X C i ⟶ X D j
n✝ : ℕ
⊢ d C (Nat.succ n✝) (ComplexShape.next (ComplexShape.down ℕ) (Nat.succ n✝)) ≫
      f (ComplexShape.next (ComplexShape.down ℕ) (Nat.succ n✝)) (Nat.succ n✝) =
    d C (Nat.succ n✝) (Nat.succ n✝ - 1) ≫ f (Nat.succ n✝ - 1) (Nat.succ n✝)
congr <;> simp