-- Lean 4 proof step from Mathlib.AlgebraicTopology.ExtraDegeneracy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
i : ℕ
⊢ HomologicalComplex.Hom.f
      (CategoryStruct.comp (Y := Functor.obj (ChainComplex.single₀ C) (Functor.obj point X))
        (NatTrans.app AlternatingFaceMapComplex.ε X)
        ((Equiv.symm
              (ChainComplex.fromSingle₀Equiv (AlternatingFaceMapComplex.obj (Functor.obj drop X))
                (Functor.obj point X)) :
            (a : point.obj X ⟶ (AlternatingFaceMapComplex.obj (drop.obj X)).X 0) →
              (ChainComplex.single₀ C).obj (point.obj X) ⟶ AlternatingFaceMapComplex.obj (drop.obj X))
          ed.s'))
      (i + 1) =
    HAdd.hAdd (α :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1) ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1))
        (β :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1) ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1))
        ((dNext (i + 1) :
              (a :
                  (i j : ℕ) →
                    (AlternatingFaceMapComplex.obj (drop.obj X)).X i ⟶
                      (AlternatingFaceMapComplex.obj (drop.obj X)).X j) →
                (AlternatingFaceMapComplex.obj (drop.obj X)).X (i + 1) ⟶
                  (AlternatingFaceMapComplex.obj (drop.obj X)).X (i + 1))
            fun (i : ℕ) ↦
            Pi.single (M := fun (j : ℕ) ↦
              HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) i ⟶
                HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) j)
              (i + 1) (-ed.s i) :
          HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1) ⟶
            HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1))
        ((prevD (i + 1) :
              (a :
                  (i j : ℕ) →
                    (AlternatingFaceMapComplex.obj (drop.obj X)).X i ⟶
                      (AlternatingFaceMapComplex.obj (drop.obj X)).X j) →
                (AlternatingFaceMapComplex.obj (drop.obj X)).X (i + 1) ⟶
                  (AlternatingFaceMapComplex.obj (drop.obj X)).X (i + 1))
            fun (i : ℕ) ↦
            Pi.single (M := fun (j : ℕ) ↦
              HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) i ⟶
                HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) j)
              (i + 1) (-ed.s i) :
          HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1) ⟶
            HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1)) +
      HomologicalComplex.Hom.f (𝟙 (AlternatingFaceMapComplex.obj (Functor.obj drop X))) (i + 1)
have succ : HomologicalComplex.Hom.f
    (CategoryStruct.comp (Y := Functor.obj (ChainComplex.single₀ C) (Functor.obj point X))
      (NatTrans.app AlternatingFaceMapComplex.ε X)
      ((Equiv.symm
            (ChainComplex.fromSingle₀Equiv (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (Functor.obj point X)) :
          (a : point.obj X ⟶ (AlternatingFaceMapComplex.obj (drop.obj X)).X 0) →
            (ChainComplex.single₀ C).obj (point.obj X) ⟶ AlternatingFaceMapComplex.obj (drop.obj X))
        ed.s'))
    (i + 1) =
  HAdd.hAdd (α :=
      HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1) ⟶
        HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1))
      (β :=
      HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1) ⟶
        HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1))
      (HomologicalComplex.d (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1) i ≫
        Pi.single (M := fun (j : ℕ) ↦
          HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) i ⟶
            HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) j)
          (i + 1) (-ed.s i) (i + 1))
      (CategoryStruct.comp (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1 + 1))
          (Pi.single (M := fun (j : ℕ) ↦
            HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1) ⟶
              HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) j)
            (i + 1 + 1) (-ed.s (i + 1)) (i + 1 + 1))
          (HomologicalComplex.d (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1 + 1) (i + 1)) :
        HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1) ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) (i + 1)) +
    HomologicalComplex.Hom.f (𝟙 (AlternatingFaceMapComplex.obj (Functor.obj drop X))) (i + 1)
Tactic: rw [Homotopy.prevD_chainComplex, Homotopy.dNext_succ_chainComplex]