-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy (goal)
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 : ℕ
⊢ 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
have 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
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]
Cleared hypotheses: n