-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H_1 H : Homotopy f g
n : ℕ
zero :
  HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) f) 0 =
    HAdd.hAdd (α :=
        HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) 0 ⟶
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) 0)
        (β :=
        HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) 0 ⟶
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) 0)
        ((dNext 0 :
              (a : (i j : ℕ) → ((alternatingFaceMapComplex C).obj X).X i ⟶ ((alternatingFaceMapComplex C).obj Y).X j) →
                ((alternatingFaceMapComplex C).obj X).X 0 ⟶ ((alternatingFaceMapComplex C).obj Y).X 0)
            (ToChainHomotopy.hom H) :
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) 0 ⟶
            HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) 0)
        ((prevD 0 :
              (a : (i j : ℕ) → ((alternatingFaceMapComplex C).obj X).X i ⟶ ((alternatingFaceMapComplex C).obj Y).X j) →
                ((alternatingFaceMapComplex C).obj X).X 0 ⟶ ((alternatingFaceMapComplex C).obj Y).X 0)
            (ToChainHomotopy.hom H) :
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) 0 ⟶
            HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) 0) +
      HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) g) 0
succ :
  ∀ (n : ℕ),
    HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) f) (n + 1) =
      HAdd.hAdd (α :=
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) (n + 1) ⟶
            HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) (n + 1))
          (β :=
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) (n + 1) ⟶
            HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) (n + 1))
          ((dNext (n + 1) :
                (a :
                    (i j : ℕ) → ((alternatingFaceMapComplex C).obj X).X i ⟶ ((alternatingFaceMapComplex C).obj Y).X j) →
                  ((alternatingFaceMapComplex C).obj X).X (n + 1) ⟶ ((alternatingFaceMapComplex C).obj Y).X (n + 1))
              (ToChainHomotopy.hom H) :
            HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) (n + 1) ⟶
              HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) (n + 1))
          ((prevD (n + 1) :
                (a :
                    (i j : ℕ) → ((alternatingFaceMapComplex C).obj X).X i ⟶ ((alternatingFaceMapComplex C).obj Y).X j) →
                  ((alternatingFaceMapComplex C).obj X).X (n + 1) ⟶ ((alternatingFaceMapComplex C).obj Y).X (n + 1))
              (ToChainHomotopy.hom H) :
            HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) (n + 1) ⟶
              HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) (n + 1)) +
        HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) g) (n + 1)
⊢ HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) f) n =
    HAdd.hAdd (α :=
        HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) n ⟶
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) n)
        (β :=
        HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) n ⟶
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) n)
        ((dNext n :
              (a : (i j : ℕ) → ((alternatingFaceMapComplex C).obj X).X i ⟶ ((alternatingFaceMapComplex C).obj Y).X j) →
                ((alternatingFaceMapComplex C).obj X).X n ⟶ ((alternatingFaceMapComplex C).obj Y).X n)
            (ToChainHomotopy.hom H) :
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) n ⟶
            HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) n)
        ((prevD n :
              (a : (i j : ℕ) → ((alternatingFaceMapComplex C).obj X).X i ⟶ ((alternatingFaceMapComplex C).obj Y).X j) →
                ((alternatingFaceMapComplex C).obj X).X n ⟶ ((alternatingFaceMapComplex C).obj Y).X n)
            (ToChainHomotopy.hom H) :
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) n ⟶
            HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) n) +
      HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) g) n

Tactic:
cases n with
    | zero =>
      rw [prevD_eq (j' := 1) (w := by simp), dNext_eq_zero _ _ (by simp), zero_add]
      simp [ToChainHomotopy.comm_zero H]
    | succ n =>
      rw [dNext_eq (i' := n) (w := by simp), prevD_eq (j' := n + 2) (w := by simp)]
      simp [ToChainHomotopy.comm_succ H]

Premises used: prevD_eq, zero_add, _private.0.CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.comm_succ, _private.0.CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.comm_zero, dNext_eq, dNext_eq_zero