-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex.{v, u, 0} V ℕ
e : P ⟶ Q
zero : P.X 0 ⟶ Q.X 1
comm_zero : e.f 0 = zero ≫ Q.d 1 0
one : P.X 1 ⟶ Q.X 2
comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1
succ :
  (n : ℕ) →
    (p :
        (f : P.X n ⟶ Q.X (n + 1)) ×'
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
        e.f (n + 2) =
          P.d (n + 2) (n + 1) ≫
              p.snd (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)).fst
                (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ↦
                e.f (n + 1) =
                  P.d (n + 1) n ≫
                      p.fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                        (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
                          e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) +
                    f' ≫ Q.d (n + 2) (n + 1)) +
            f'' ≫ Q.d (n + 3) (n + 2)
n : ℕ
e_a :
  Iso.hom (xNextIso P ⋯) ≫
      (mkInductiveAux₁ e zero one comm_one succ n).fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
        (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) =
    PSigma.fst (β :=
        fun (f' : P.X ((ComplexShape.down ℕ).next (n + 1)) ⟶ xPrev Q ((ComplexShape.down ℕ).next (n + 1))) ↦
        e.f ((ComplexShape.down ℕ).next (n + 1)) =
          dFrom P ((ComplexShape.down ℕ).next (n + 1)) ≫
              PSigma.fst (β :=
                fun (f : xNext P ((ComplexShape.down ℕ).next (n + 1)) ⟶ Q.X ((ComplexShape.down ℕ).next (n + 1))) ↦
                (f' : P.X ((ComplexShape.down ℕ).next (n + 1)) ⟶ xPrev Q ((ComplexShape.down ℕ).next (n + 1))) ×'
                  e.f ((ComplexShape.down ℕ).next (n + 1)) =
                    dFrom P ((ComplexShape.down ℕ).next (n + 1)) ≫ f + f' ≫ dTo Q ((ComplexShape.down ℕ).next (n + 1)))
                (mkInductiveAux₂ e zero comm_zero one comm_one succ ((ComplexShape.down ℕ).next (n + 1))) +
            f' ≫ dTo Q ((ComplexShape.down ℕ).next (n + 1)))
        (PSigma.snd (β :=
          fun (f : xNext P ((ComplexShape.down ℕ).next (n + 1)) ⟶ Q.X ((ComplexShape.down ℕ).next (n + 1))) ↦
          (f' : P.X ((ComplexShape.down ℕ).next (n + 1)) ⟶ xPrev Q ((ComplexShape.down ℕ).next (n + 1))) ×'
            e.f ((ComplexShape.down ℕ).next (n + 1)) =
              dFrom P ((ComplexShape.down ℕ).next (n + 1)) ≫ f + f' ≫ dTo Q ((ComplexShape.down ℕ).next (n + 1)))
          (mkInductiveAux₂ e zero comm_zero one comm_one succ ((ComplexShape.down ℕ).next (n + 1)))) ≫
      (xPrevIso Q ⋯).hom
⊢ Iso.hom (xNextIso P ⋯) ≫
      (mkInductiveAux₁ e zero one comm_one succ n).fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
        (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) =
    if h : (ComplexShape.down ℕ).next (n + 1) + 1 = n + 1 then
      PSigma.fst (β :=
          fun (f' : P.X ((ComplexShape.down ℕ).next (n + 1)) ⟶ xPrev Q ((ComplexShape.down ℕ).next (n + 1))) ↦
          e.f ((ComplexShape.down ℕ).next (n + 1)) =
            dFrom P ((ComplexShape.down ℕ).next (n + 1)) ≫
                PSigma.fst (β :=
                  fun (f : xNext P ((ComplexShape.down ℕ).next (n + 1)) ⟶ Q.X ((ComplexShape.down ℕ).next (n + 1))) ↦
                  (f' : P.X ((ComplexShape.down ℕ).next (n + 1)) ⟶ xPrev Q ((ComplexShape.down ℕ).next (n + 1))) ×'
                    e.f ((ComplexShape.down ℕ).next (n + 1)) =
                      dFrom P ((ComplexShape.down ℕ).next (n + 1)) ≫ f +
                        f' ≫ dTo Q ((ComplexShape.down ℕ).next (n + 1)))
                  (mkInductiveAux₂ e zero comm_zero one comm_one succ ((ComplexShape.down ℕ).next (n + 1))) +
              f' ≫ dTo Q ((ComplexShape.down ℕ).next (n + 1)))
          (PSigma.snd (β :=
            fun (f : xNext P ((ComplexShape.down ℕ).next (n + 1)) ⟶ Q.X ((ComplexShape.down ℕ).next (n + 1))) ↦
            (f' : P.X ((ComplexShape.down ℕ).next (n + 1)) ⟶ xPrev Q ((ComplexShape.down ℕ).next (n + 1))) ×'
              e.f ((ComplexShape.down ℕ).next (n + 1)) =
                dFrom P ((ComplexShape.down ℕ).next (n + 1)) ≫ f + f' ≫ dTo Q ((ComplexShape.down ℕ).next (n + 1)))
            (mkInductiveAux₂ e zero comm_zero one comm_one succ ((ComplexShape.down ℕ).next (n + 1)))) ≫
        (xPrevIso Q h).hom
    else 0

Tactic:
simp only [ChainComplex.next_nat_succ, dite_true]

Premises used: ChainComplex.next_nat_succ, dite_true