C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : n < q
⊢ Homotopy.hom (homotopyPToId X (q + 0)) n (n + 1) = Homotopy.hom (homotopyPToId X q) n (n + 1)
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : n < q
⊢ Homotopy.hom (homotopyPToId X (q + 1)) n (n + 1) = Homotopy.hom (homotopyPToId X q) n (n + 1)
simp only [homotopyHσToZero, AlternatingFaceMapComplex.obj_X, Nat.add_eq, Homotopy.trans_hom,
  Homotopy.ofEq_hom, Pi.zero_apply, Homotopy.add_hom, Homotopy.compLeft_hom, add_zero,
  Homotopy.nullHomotopy'_hom, ComplexShape.down_Rel, hσ'_eq_zero hqn (c_mk (n + 1) n rfl),
  dite_eq_ite, ite_self, comp_zero, zero_add, homotopyPToId]
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : n < q
⊢ Homotopy.hom (homotopyPToId X (q + 0)) n (n + 1) = Homotopy.hom (homotopyPToId X q) n (n + 1)
rfl