-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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 : CochainComplex.{v, u, 0} V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×'
        e.f (n + 2) =
          p.snd (β := fun (f : P.X (n + 1) ⟶ Q.X n) ↦
                    (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f').fst
                (β := fun (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ↦
                e.f (n + 1) =
                  p.fst (β := fun (f : P.X (n + 1) ⟶ Q.X n) ↦
                        (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×'
                          e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') ≫
                      Q.d n (n + 1) +
                    P.d (n + 1) (n + 2) ≫ f') ≫
              Q.d (n + 1) (n + 2) +
            P.d (n + 2) (n + 3) ≫ f''
n : ℕ
⊢ (mkCoinductiveAux₁ e zero one comm_one succ n).fst (β := fun (f : P.X (n + 1) ⟶ Q.X n) ↦
        (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') ≫
      Iso.inv (xPrevIso Q ⋯) =
    if h : (ComplexShape.up ℕ).prev (n + 1) + 1 = n + 1 then
      (xNextIso P h).inv ≫
        PSigma.fst (β :=
          fun (f' : xNext P ((ComplexShape.up ℕ).prev (n + 1)) ⟶ Q.X ((ComplexShape.up ℕ).prev (n + 1))) ↦
          e.f ((ComplexShape.up ℕ).prev (n + 1)) =
            PSigma.fst (β :=
                  fun (f : P.X ((ComplexShape.up ℕ).prev (n + 1)) ⟶ xPrev Q ((ComplexShape.up ℕ).prev (n + 1))) ↦
                  (f' : xNext P ((ComplexShape.up ℕ).prev (n + 1)) ⟶ Q.X ((ComplexShape.up ℕ).prev (n + 1))) ×'
                    e.f ((ComplexShape.up ℕ).prev (n + 1)) =
                      f ≫ dTo Q ((ComplexShape.up ℕ).prev (n + 1)) + dFrom P ((ComplexShape.up ℕ).prev (n + 1)) ≫ f')
                  (mkCoinductiveAux₂ e zero comm_zero one comm_one succ ((ComplexShape.up ℕ).prev (n + 1))) ≫
                dTo Q ((ComplexShape.up ℕ).prev (n + 1)) +
              dFrom P ((ComplexShape.up ℕ).prev (n + 1)) ≫ f')
          (PSigma.snd (β :=
            fun (f : P.X ((ComplexShape.up ℕ).prev (n + 1)) ⟶ xPrev Q ((ComplexShape.up ℕ).prev (n + 1))) ↦
            (f' : xNext P ((ComplexShape.up ℕ).prev (n + 1)) ⟶ Q.X ((ComplexShape.up ℕ).prev (n + 1))) ×'
              e.f ((ComplexShape.up ℕ).prev (n + 1)) =
                f ≫ dTo Q ((ComplexShape.up ℕ).prev (n + 1)) + dFrom P ((ComplexShape.up ℕ).prev (n + 1)) ≫ f')
            (mkCoinductiveAux₂ e zero comm_zero one comm_one succ ((ComplexShape.up ℕ).prev (n + 1))))
    else 0
have e_a : (mkCoinductiveAux₁ e zero one comm_one succ n).fst (β := fun (f : P.X (n + 1) ⟶ Q.X n) ↦
      (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') ≫
    Iso.inv (xPrevIso Q sorry) =
  (xNextIso P sorry).inv ≫
    PSigma.fst (β := fun (f' : xNext P ((ComplexShape.up ℕ).prev (n + 1)) ⟶ Q.X ((ComplexShape.up ℕ).prev (n + 1))) ↦
      e.f ((ComplexShape.up ℕ).prev (n + 1)) =
        PSigma.fst (β := fun (f : P.X ((ComplexShape.up ℕ).prev (n + 1)) ⟶ xPrev Q ((ComplexShape.up ℕ).prev (n + 1))) ↦
              (f' : xNext P ((ComplexShape.up ℕ).prev (n + 1)) ⟶ Q.X ((ComplexShape.up ℕ).prev (n + 1))) ×'
                e.f ((ComplexShape.up ℕ).prev (n + 1)) =
                  f ≫ dTo Q ((ComplexShape.up ℕ).prev (n + 1)) + dFrom P ((ComplexShape.up ℕ).prev (n + 1)) ≫ f')
              (mkCoinductiveAux₂ e zero comm_zero one comm_one succ ((ComplexShape.up ℕ).prev (n + 1))) ≫
            dTo Q ((ComplexShape.up ℕ).prev (n + 1)) +
          dFrom P ((ComplexShape.up ℕ).prev (n + 1)) ≫ f')
      (PSigma.snd (β := fun (f : P.X ((ComplexShape.up ℕ).prev (n + 1)) ⟶ xPrev Q ((ComplexShape.up ℕ).prev (n + 1))) ↦
        (f' : xNext P ((ComplexShape.up ℕ).prev (n + 1)) ⟶ Q.X ((ComplexShape.up ℕ).prev (n + 1))) ×'
          e.f ((ComplexShape.up ℕ).prev (n + 1)) =
            f ≫ dTo Q ((ComplexShape.up ℕ).prev (n + 1)) + dFrom P ((ComplexShape.up ℕ).prev (n + 1)) ≫ f')
        (mkCoinductiveAux₂ e zero comm_zero one comm_one succ ((ComplexShape.up ℕ).prev (n + 1))))
Tactic: simp only [CochainComplex.prev_nat_succ, dite_true]