-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
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''
i : ℕ
zero₁ :
  (xNextIso P ⋯).inv ≫
      PSigma.fst (β := fun (f' : xNext P 0 ⟶ Q.X 0) ↦
        e.f 0 =
          PSigma.fst (β := fun (f : P.X 0 ⟶ xPrev Q 0) ↦
                (f' : xNext P 0 ⟶ Q.X 0) ×' e.f 0 = f ≫ dTo Q 0 + dFrom P 0 ≫ f')
                (mkCoinductiveAux₂ e zero comm_zero one comm_one succ 0) ≫
              dTo Q 0 +
            dFrom P 0 ≫ f')
        (PSigma.snd (β := fun (f : P.X 0 ⟶ xPrev Q 0) ↦
          (f' : xNext P 0 ⟶ Q.X 0) ×' e.f 0 = f ≫ dTo Q 0 + dFrom P 0 ≫ f')
          (mkCoinductiveAux₂ e zero comm_zero one comm_one succ 0)) =
    PSigma.fst (β := fun (f : P.X (HAdd.hAdd (α := ℕ) 0 1) ⟶ xPrev Q (HAdd.hAdd (α := ℕ) 0 1)) ↦
        (f' : xNext P (HAdd.hAdd (α := ℕ) 0 1) ⟶ Q.X (HAdd.hAdd (α := ℕ) 0 1)) ×'
          e.f (HAdd.hAdd (α := ℕ) 0 1) = f ≫ dTo Q (HAdd.hAdd (α := ℕ) 0 1) + dFrom P (HAdd.hAdd (α := ℕ) 0 1) ≫ f')
        (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (HAdd.hAdd (α := ℕ) 0 1)) ≫
      (xPrevIso Q ⋯).hom
succ₁ :
  (xNextIso P ⋯).inv ≫
      PSigma.fst (β := fun (f' : xNext P (HAdd.hAdd (α := ℕ) 0 1) ⟶ Q.X (HAdd.hAdd (α := ℕ) 0 1)) ↦
        e.f (HAdd.hAdd (α := ℕ) 0 1) =
          PSigma.fst (β := fun (f : P.X (HAdd.hAdd (α := ℕ) 0 1) ⟶ xPrev Q (HAdd.hAdd (α := ℕ) 0 1)) ↦
                (f' : xNext P (HAdd.hAdd (α := ℕ) 0 1) ⟶ Q.X (HAdd.hAdd (α := ℕ) 0 1)) ×'
                  e.f (HAdd.hAdd (α := ℕ) 0 1) =
                    f ≫ dTo Q (HAdd.hAdd (α := ℕ) 0 1) + dFrom P (HAdd.hAdd (α := ℕ) 0 1) ≫ f')
                (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (HAdd.hAdd (α := ℕ) 0 1)) ≫
              dTo Q (HAdd.hAdd (α := ℕ) 0 1) +
            dFrom P (HAdd.hAdd (α := ℕ) 0 1) ≫ f')
        (PSigma.snd (β := fun (f : P.X (HAdd.hAdd (α := ℕ) 0 1) ⟶ xPrev Q (HAdd.hAdd (α := ℕ) 0 1)) ↦
          (f' : xNext P (HAdd.hAdd (α := ℕ) 0 1) ⟶ Q.X (HAdd.hAdd (α := ℕ) 0 1)) ×'
            e.f (HAdd.hAdd (α := ℕ) 0 1) = f ≫ dTo Q (HAdd.hAdd (α := ℕ) 0 1) + dFrom P (HAdd.hAdd (α := ℕ) 0 1) ≫ f')
          (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (HAdd.hAdd (α := ℕ) 0 1))) =
    PSigma.fst (β := fun (f : P.X (HAdd.hAdd (α := ℕ) 0 1 + 1) ⟶ xPrev Q (HAdd.hAdd (α := ℕ) 0 1 + 1)) ↦
        (f' : xNext P (HAdd.hAdd (α := ℕ) 0 1 + 1) ⟶ Q.X (HAdd.hAdd (α := ℕ) 0 1 + 1)) ×'
          e.f (HAdd.hAdd (α := ℕ) 0 1 + 1) =
            f ≫ dTo Q (HAdd.hAdd (α := ℕ) 0 1 + 1) + dFrom P (HAdd.hAdd (α := ℕ) 0 1 + 1) ≫ f')
        (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (HAdd.hAdd (α := ℕ) 0 1 + 1)) ≫
      (xPrevIso Q ⋯).hom
⊢ (xNextIso P ⋯).inv ≫
      (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).snd (β := fun (f : P.X i ⟶ xPrev Q i) ↦
            (f' : xNext P i ⟶ Q.X i) ×' e.f i = f ≫ dTo Q i + dFrom P i ≫ f').fst
        (β := fun (f' : xNext P i ⟶ Q.X i) ↦
        e.f i =
          (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).fst (β := fun (f : P.X i ⟶ xPrev Q i) ↦
                (f' : xNext P i ⟶ Q.X i) ×' e.f i = f ≫ dTo Q i + dFrom P i ≫ f') ≫
              dTo Q i +
            dFrom P i ≫ f') =
    PSigma.fst (β := fun (f : P.X (i + 1) ⟶ xPrev Q (i + 1)) ↦
        (f' : xNext P (i + 1) ⟶ Q.X (i + 1)) ×' e.f (i + 1) = f ≫ dTo Q (i + 1) + dFrom P (i + 1) ≫ f')
        (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (i + 1)) ≫
      (xPrevIso Q ⋯).hom
have succ₂ : ∀ (i : ℕ),
  (xNextIso P sorry).inv ≫
      PSigma.fst (β := fun (f' : xNext P (i + 1 + 1) ⟶ Q.X (i + 1 + 1)) ↦
        e.f (i + 1 + 1) =
          PSigma.fst (β := fun (f : P.X (i + 1 + 1) ⟶ xPrev Q (i + 1 + 1)) ↦
                (f' : xNext P (i + 1 + 1) ⟶ Q.X (i + 1 + 1)) ×'
                  e.f (i + 1 + 1) = f ≫ dTo Q (i + 1 + 1) + dFrom P (i + 1 + 1) ≫ f')
                (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (i + 1 + 1)) ≫
              dTo Q (i + 1 + 1) +
            dFrom P (i + 1 + 1) ≫ f')
        (PSigma.snd (β := fun (f : P.X (i + 1 + 1) ⟶ xPrev Q (i + 1 + 1)) ↦
          (f' : xNext P (i + 1 + 1) ⟶ Q.X (i + 1 + 1)) ×'
            e.f (i + 1 + 1) = f ≫ dTo Q (i + 1 + 1) + dFrom P (i + 1 + 1) ≫ f')
          (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (i + 1 + 1))) =
    PSigma.fst (β := fun (f : P.X (i + 1 + 1 + 1) ⟶ xPrev Q (i + 1 + 1 + 1)) ↦
        (f' : xNext P (i + 1 + 1 + 1) ⟶ Q.X (i + 1 + 1 + 1)) ×'
          e.f (i + 1 + 1 + 1) = f ≫ dTo Q (i + 1 + 1 + 1) + dFrom P (i + 1 + 1 + 1) ≫ f')
        (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (i + 1 + 1 + 1)) ≫
      (xPrevIso Q sorry).hom
Tactic: rcases i with (_ | _ | i)
Cleared hypotheses: i