-- 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 : ℕ
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
⊢ 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 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)
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