[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.42, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ Homotopy (P (q + 1)) (𝟙 K[X])
[PROOFSTEP]
refine'
  Homotopy.trans (Homotopy.ofEq _)
    (Homotopy.trans (Homotopy.add (homotopyPToId q) (Homotopy.compLeft (homotopyHσToZero q) (P q))) (Homotopy.ofEq _))
[GOAL]
case refine'_1
C : Type u_1
inst✝¹ : Category.{?u.42, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ P (q + 1) = P q + P q ≫ Hσ q
[PROOFSTEP]
simp only [P_succ, comp_add, comp_id]
[GOAL]
case refine'_2
C : Type u_1
inst✝¹ : Category.{?u.42, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ 𝟙 K[X] + P q ≫ 0 = 𝟙 K[X]
[PROOFSTEP]
simp only [add_zero, comp_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} 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)
[PROOFSTEP]
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]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} 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)
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.44641, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f PInfty n =
    ((↑(dNext n) fun i j => Homotopy.hom (homotopyPToId X (j + 1)) i j) +
        ↑(prevD n) fun i j => Homotopy.hom (homotopyPToId X (j + 1)) i j) +
      HomologicalComplex.Hom.f (𝟙 K[X]) n
[PROOFSTEP]
rcases n with _ | n
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{?u.44641, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ HomologicalComplex.Hom.f PInfty Nat.zero =
    ((↑(dNext Nat.zero) fun i j => Homotopy.hom (homotopyPToId X (j + 1)) i j) +
        ↑(prevD Nat.zero) fun i j => Homotopy.hom (homotopyPToId X (j + 1)) i j) +
      HomologicalComplex.Hom.f (𝟙 K[X]) Nat.zero
[PROOFSTEP]
simpa only [Homotopy.dNext_zero_chainComplex, Homotopy.prevD_chainComplex, PInfty_f, Nat.zero_eq, P_f_0_eq,
  zero_add] using (homotopyPToId X 2).comm 0
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.44641, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f PInfty (Nat.succ n) =
    ((↑(dNext (Nat.succ n)) fun i j => Homotopy.hom (homotopyPToId X (j + 1)) i j) +
        ↑(prevD (Nat.succ n)) fun i j => Homotopy.hom (homotopyPToId X (j + 1)) i j) +
      HomologicalComplex.Hom.f (𝟙 K[X]) (Nat.succ n)
[PROOFSTEP]
rw [Homotopy.dNext_succ_chainComplex, Homotopy.prevD_chainComplex, PInfty_f, ←
  P_is_eventually_constant (rfl.le : n + 1 ≤ n + 1)]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.44641, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f (P (n + 1 + 1)) (n + 1) =
    HomologicalComplex.d K[X] (n + 1) n ≫ Homotopy.hom (homotopyPToId X (n + 1 + 1)) n (n + 1) +
        Homotopy.hom (homotopyPToId X (Nat.succ n + 1 + 1)) (Nat.succ n) (Nat.succ n + 1) ≫
          HomologicalComplex.d K[X] (Nat.succ n + 1) (Nat.succ n) +
      HomologicalComplex.Hom.f (𝟙 K[X]) (Nat.succ n)
[PROOFSTEP]
erw [homotopyPToId_eventually_constant X (lt_add_one (Nat.succ n))]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.44641, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f (P (n + 1 + 1)) (n + 1) =
    HomologicalComplex.d K[X] (n + 1) n ≫ Homotopy.hom (homotopyPToId X (n + 1 + 1)) n (n + 1) +
        Homotopy.hom (homotopyPToId X (Nat.succ n + 1)) (Nat.succ n) (Nat.succ n + 1) ≫
          HomologicalComplex.d K[X] (Nat.succ n + 1) (Nat.succ n) +
      HomologicalComplex.Hom.f (𝟙 K[X]) (Nat.succ n)
[PROOFSTEP]
have := (homotopyPToId X (n + 2)).comm (n + 1)
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.44641, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
this :
  HomologicalComplex.Hom.f (P (n + 2)) (n + 1) =
    ↑(dNext (n + 1)) (homotopyPToId X (n + 2)).hom + ↑(prevD (n + 1)) (homotopyPToId X (n + 2)).hom +
      HomologicalComplex.Hom.f (𝟙 K[X]) (n + 1)
⊢ HomologicalComplex.Hom.f (P (n + 1 + 1)) (n + 1) =
    HomologicalComplex.d K[X] (n + 1) n ≫ Homotopy.hom (homotopyPToId X (n + 1 + 1)) n (n + 1) +
        Homotopy.hom (homotopyPToId X (Nat.succ n + 1)) (Nat.succ n) (Nat.succ n + 1) ≫
          HomologicalComplex.d K[X] (Nat.succ n + 1) (Nat.succ n) +
      HomologicalComplex.Hom.f (𝟙 K[X]) (Nat.succ n)
[PROOFSTEP]
rw [Homotopy.dNext_succ_chainComplex, Homotopy.prevD_chainComplex] at this 
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.44641, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
this :
  HomologicalComplex.Hom.f (P (n + 2)) (n + 1) =
    HomologicalComplex.d K[X] (n + 1) n ≫ Homotopy.hom (homotopyPToId X (n + 2)) n (n + 1) +
        Homotopy.hom (homotopyPToId X (n + 2)) (n + 1) (n + 1 + 1) ≫ HomologicalComplex.d K[X] (n + 1 + 1) (n + 1) +
      HomologicalComplex.Hom.f (𝟙 K[X]) (n + 1)
⊢ HomologicalComplex.Hom.f (P (n + 1 + 1)) (n + 1) =
    HomologicalComplex.d K[X] (n + 1) n ≫ Homotopy.hom (homotopyPToId X (n + 1 + 1)) n (n + 1) +
        Homotopy.hom (homotopyPToId X (Nat.succ n + 1)) (Nat.succ n) (Nat.succ n + 1) ≫
          HomologicalComplex.d K[X] (Nat.succ n + 1) (Nat.succ n) +
      HomologicalComplex.Hom.f (𝟙 K[X]) (Nat.succ n)
[PROOFSTEP]
exact this
