-- 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_1 : ι
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 : ℕ
refine :
  (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 ≫
        (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') =
    HAdd.hAdd (α := P.X i ⟶ Q.X i) (β := P.X i ⟶ Q.X i)
      (((toPrev i : (a : (i j : ℕ) → P.X i ⟶ Q.X j) → P.X i ⟶ xPrev Q i) fun (i j : ℕ) ↦
            if h : j + 1 = i then
              (xNextIso P h).inv ≫
                (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd (β := fun (f : P.X j ⟶ xPrev Q j) ↦
                      (f' : xNext P j ⟶ Q.X j) ×' e.f j = f ≫ dTo Q j + dFrom P j ≫ f').fst
                  (β := fun (f' : xNext P j ⟶ Q.X j) ↦
                  e.f j =
                    (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).fst (β := fun (f : P.X j ⟶ xPrev Q j) ↦
                          (f' : xNext P j ⟶ Q.X j) ×' e.f j = f ≫ dTo Q j + dFrom P j ≫ f') ≫
                        dTo Q j +
                      dFrom P j ≫ f')
            else 0) ≫
          dTo Q i :
        P.X i ⟶ Q.X i)
      (dFrom P i ≫
        (fromNext i : (a : (i j : ℕ) → P.X i ⟶ Q.X j) → xNext P i ⟶ Q.X i) fun (i j : ℕ) ↦
          if h : j + 1 = i then
            (xNextIso P h).inv ≫
              (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd (β := fun (f : P.X j ⟶ xPrev Q j) ↦
                    (f' : xNext P j ⟶ Q.X j) ×' e.f j = f ≫ dTo Q j + dFrom P j ≫ f').fst
                (β := fun (f' : xNext P j ⟶ Q.X j) ↦
                e.f j =
                  (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).fst (β := fun (f : P.X j ⟶ xPrev Q j) ↦
                        (f' : xNext P j ⟶ Q.X j) ×' e.f j = f ≫ dTo Q j + dFrom P j ≫ f') ≫
                      dTo Q j +
                    dFrom P j ≫ f')
          else 0)
⊢ e.f i =
    HAdd.hAdd (α := P.X i ⟶ Q.X i) (β := P.X i ⟶ Q.X i)
      (((toPrev i : (a : (i j : ℕ) → P.X i ⟶ Q.X j) → P.X i ⟶ xPrev Q i) fun (i j : ℕ) ↦
            if h : j + 1 = i then
              (xNextIso P h).inv ≫
                (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd (β := fun (f : P.X j ⟶ xPrev Q j) ↦
                      (f' : xNext P j ⟶ Q.X j) ×' e.f j = f ≫ dTo Q j + dFrom P j ≫ f').fst
                  (β := fun (f' : xNext P j ⟶ Q.X j) ↦
                  e.f j =
                    (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).fst (β := fun (f : P.X j ⟶ xPrev Q j) ↦
                          (f' : xNext P j ⟶ Q.X j) ×' e.f j = f ≫ dTo Q j + dFrom P j ≫ f') ≫
                        dTo Q j +
                      dFrom P j ≫ f')
            else 0) ≫
          dTo Q i :
        P.X i ⟶ Q.X i)
      (dFrom P i ≫
        (fromNext i : (a : (i j : ℕ) → P.X i ⟶ Q.X j) → xNext P i ⟶ Q.X i) fun (i j : ℕ) ↦
          if h : j + 1 = i then
            (xNextIso P h).inv ≫
              (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd (β := fun (f : P.X j ⟶ xPrev Q j) ↦
                    (f' : xNext P j ⟶ Q.X j) ×' e.f j = f ≫ dTo Q j + dFrom P j ≫ f').fst
                (β := fun (f' : xNext P j ⟶ Q.X j) ↦
                e.f j =
                  (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).fst (β := fun (f : P.X j ⟶ xPrev Q j) ↦
                        (f' : xNext P j ⟶ Q.X j) ×' e.f j = f ≫ dTo Q j + dFrom P j ≫ f') ≫
                      dTo Q j +
                    dFrom P j ≫ f')
          else 0)

Tactic:
refine (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).2.2.trans ?_

Premises used: PSigma.snd, Homotopy.mkCoinductiveAux₂, Eq.trans