-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
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 : ℕ
zero :
  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'))
      0 =
    HAdd.hAdd (α :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) 0 ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) 0)
        (β :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) 0 ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) 0)
        ((dNext 0 :
              (a :
                  (i j : ℕ) →
                    (AlternatingFaceMapComplex.obj (drop.obj X)).X i ⟶
                      (AlternatingFaceMapComplex.obj (drop.obj X)).X j) →
                (AlternatingFaceMapComplex.obj (drop.obj X)).X 0 ⟶ (AlternatingFaceMapComplex.obj (drop.obj X)).X 0)
            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)) 0 ⟶
            HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) 0)
        ((prevD 0 :
              (a :
                  (i j : ℕ) →
                    (AlternatingFaceMapComplex.obj (drop.obj X)).X i ⟶
                      (AlternatingFaceMapComplex.obj (drop.obj X)).X j) →
                (AlternatingFaceMapComplex.obj (drop.obj X)).X 0 ⟶ (AlternatingFaceMapComplex.obj (drop.obj X)).X 0)
            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)) 0 ⟶
            HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) 0) +
      HomologicalComplex.Hom.f (𝟙 (AlternatingFaceMapComplex.obj (Functor.obj drop X))) 0
succ :
  ∀ (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)
⊢ 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 =
    HAdd.hAdd (α :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) i ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) i)
        (β :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) i ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) i)
        ((dNext i :
              (a :
                  (i j : ℕ) →
                    (AlternatingFaceMapComplex.obj (drop.obj X)).X i ⟶
                      (AlternatingFaceMapComplex.obj (drop.obj X)).X j) →
                (AlternatingFaceMapComplex.obj (drop.obj X)).X i ⟶ (AlternatingFaceMapComplex.obj (drop.obj X)).X i)
            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 ⟶
            HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) i)
        ((prevD i :
              (a :
                  (i j : ℕ) →
                    (AlternatingFaceMapComplex.obj (drop.obj X)).X i ⟶
                      (AlternatingFaceMapComplex.obj (drop.obj X)).X j) →
                (AlternatingFaceMapComplex.obj (drop.obj X)).X i ⟶ (AlternatingFaceMapComplex.obj (drop.obj X)).X i)
            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 ⟶
            HomologicalComplex.X (AlternatingFaceMapComplex.obj (Functor.obj drop X)) i) +
      HomologicalComplex.Hom.f (𝟙 (AlternatingFaceMapComplex.obj (Functor.obj drop X))) i

Tactic:
cases i with
        | zero =>
          rw [Homotopy.prevD_chainComplex, Homotopy.dNext_zero_chainComplex]
          simp [dsimp% ChainComplex.fromSingle₀Equiv_symm_apply_f_zero
            (C := AlternatingFaceMapComplex.obj X.left), s_comp_δ₀, s₀_comp_δ₁]
        | succ i =>
          rw [Homotopy.prevD_chainComplex, Homotopy.dNext_succ_chainComplex]
          simp [Fin.sum_univ_succ (n := i + 2), s_comp_δ₀, Preadditive.sum_comp,
            Preadditive.comp_sum,
            s_comp_δ, pow_succ]

Premises used: pow_succ, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ, Homotopy.dNext_zero_chainComplex, Homotopy.prevD_chainComplex, CategoryTheory.Preadditive.sum_comp, CategoryTheory.Preadditive.comp_sum, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s₀_comp_δ₁, Homotopy.dNext_succ_chainComplex, ChainComplex.fromSingle₀Equiv_symm_apply_f_zero, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ₀, Fin.sum_univ_succ