-- Lean 4 proof step from Mathlib.Algebra.Homology.Augment (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : X ⟶ C.X 0
w : Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0
i j : ℕ
hij : (ComplexShape.up ℕ).Rel i j
this : ∀ (k : ℕ), Eq (α := X ⟶ C.X (k + 1)) (f ≫ C.d 0 (k + 1)) 0
k : ℕ
hjk : (ComplexShape.up ℕ).Rel j (k + 1 + 1)
succ :
  ∀ (hij : (ComplexShape.up ℕ).Rel i 0) (hjk : (ComplexShape.up ℕ).Rel 0 (k + 1 + 1)),
    Eq.{v + 1} (α :=
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) i with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) k + 1 + 1 with
          | 0 => X
          | i.succ => C.X i :
          V))
      (CategoryStruct.comp (Y :=
          match (motive := ℕ → V) 0 with
          | 0 => X
          | i.succ => C.X i)
          (match (motive :=
            (x x_1 : ℕ) →
              Quiver.Hom.{v, u} (V := V)
                (match (motive := ℕ → V) x with
                  | 0 => X
                  | i.succ => C.X i :
                  V)
                (match (motive := ℕ → V) x_1 with
                  | 0 => X
                  | i.succ => C.X i :
                  V))
            i, 0 with
          | 0, 1 => f
          | i.succ, j.succ => C.d i j
          | x, x_1 => 0)
          (match (motive :=
            (x x_1 : ℕ) →
              Quiver.Hom.{v, u} (V := V)
                (match (motive := ℕ → V) x with
                  | 0 => X
                  | i.succ => C.X i :
                  V)
                (match (motive := ℕ → V) x_1 with
                  | 0 => X
                  | i.succ => C.X i :
                  V))
            0, k + 1 + 1 with
          | 0, 1 => f
          | i.succ, j.succ => C.d i j
          | x, x_1 => 0) :
        Quiver.Hom.{v, u} (V := V)
          (match (motive := ℕ → V) i with
            | 0 => X
            | i.succ => C.X i :
            V)
          (match (motive := ℕ → V) k + 1 + 1 with
            | 0 => X
            | i.succ => C.X i :
            V))
      (0 :
        Quiver.Hom.{v, u} (V := V)
          (match (motive := ℕ → V) i with
            | 0 => X
            | i.succ => C.X i :
            V)
          (match (motive := ℕ → V) k + 1 + 1 with
            | 0 => X
            | i.succ => C.X i :
            V))
succ₁ :
  ∀ (hij : (ComplexShape.up ℕ).Rel i (HAdd.hAdd (α := ℕ) 0 1))
    (hjk : (ComplexShape.up ℕ).Rel (HAdd.hAdd (α := ℕ) 0 1) (k + 1 + 1)),
    Eq.{v + 1} (α :=
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) i with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) k + 1 + 1 with
          | 0 => X
          | i.succ => C.X i :
          V))
      (CategoryStruct.comp (Y :=
          match (motive := ℕ → V) HAdd.hAdd (α := ℕ) 0 1 with
          | 0 => X
          | i.succ => C.X i)
          (match (motive :=
            (x x_1 : ℕ) →
              Quiver.Hom.{v, u} (V := V)
                (match (motive := ℕ → V) x with
                  | 0 => X
                  | i.succ => C.X i :
                  V)
                (match (motive := ℕ → V) x_1 with
                  | 0 => X
                  | i.succ => C.X i :
                  V))
            i, HAdd.hAdd (α := ℕ) 0 1 with
          | 0, 1 => f
          | i.succ, j.succ => C.d i j
          | x, x_1 => 0)
          (match (motive :=
            (x x_1 : ℕ) →
              Quiver.Hom.{v, u} (V := V)
                (match (motive := ℕ → V) x with
                  | 0 => X
                  | i.succ => C.X i :
                  V)
                (match (motive := ℕ → V) x_1 with
                  | 0 => X
                  | i.succ => C.X i :
                  V))
            HAdd.hAdd (α := ℕ) 0 1, k + 1 + 1 with
          | 0, 1 => f
          | i.succ, j.succ => C.d i j
          | x, x_1 => 0) :
        Quiver.Hom.{v, u} (V := V)
          (match (motive := ℕ → V) i with
            | 0 => X
            | i.succ => C.X i :
            V)
          (match (motive := ℕ → V) k + 1 + 1 with
            | 0 => X
            | i.succ => C.X i :
            V))
      (0 :
        Quiver.Hom.{v, u} (V := V)
          (match (motive := ℕ → V) i with
            | 0 => X
            | i.succ => C.X i :
            V)
          (match (motive := ℕ → V) k + 1 + 1 with
            | 0 => X
            | i.succ => C.X i :
            V))
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := V)
      (match (motive := ℕ → V) i with
        | 0 => X
        | i.succ => C.X i :
        V)
      (match (motive := ℕ → V) k + 1 + 1 with
        | 0 => X
        | i.succ => C.X i :
        V))
    (CategoryStruct.comp (Y :=
        match (motive := ℕ → V) j with
        | 0 => X
        | i.succ => C.X i)
        (match (motive :=
          (x x_1 : ℕ) →
            Quiver.Hom.{v, u} (V := V)
              (match (motive := ℕ → V) x with
                | 0 => X
                | i.succ => C.X i :
                V)
              (match (motive := ℕ → V) x_1 with
                | 0 => X
                | i.succ => C.X i :
                V))
          i, j with
        | 0, 1 => f
        | i.succ, j.succ => C.d i j
        | x, x_1 => 0)
        (match (motive :=
          (x x_1 : ℕ) →
            Quiver.Hom.{v, u} (V := V)
              (match (motive := ℕ → V) x with
                | 0 => X
                | i.succ => C.X i :
                V)
              (match (motive := ℕ → V) x_1 with
                | 0 => X
                | i.succ => C.X i :
                V))
          j, k + 1 + 1 with
        | 0, 1 => f
        | i.succ, j.succ => C.d i j
        | x, x_1 => 0) :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) i with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) k + 1 + 1 with
          | 0 => X
          | i.succ => C.X i :
          V))
    (0 :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) i with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) k + 1 + 1 with
          | 0 => X
          | i.succ => C.X i :
          V))
have succ₂ : ∀ (j : ℕ) (hij : (ComplexShape.up ℕ).Rel i (j + 1 + 1)) (hjk : (ComplexShape.up ℕ).Rel (j + 1 + 1) (k + 1 + 1)),
  Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := V)
      (match (motive := ℕ → V) i with
        | 0 => X
        | i.succ => C.X i :
        V)
      (match (motive := ℕ → V) k + 1 + 1 with
        | 0 => X
        | i.succ => C.X i :
        V))
    (CategoryStruct.comp (Y :=
        match (motive := ℕ → V) j + 1 + 1 with
        | 0 => X
        | i.succ => C.X i)
        (match (motive :=
          (x x_1 : ℕ) →
            Quiver.Hom.{v, u} (V := V)
              (match (motive := ℕ → V) x with
                | 0 => X
                | i.succ => C.X i :
                V)
              (match (motive := ℕ → V) x_1 with
                | 0 => X
                | i.succ => C.X i :
                V))
          i, j + 1 + 1 with
        | 0, 1 => f
        | i.succ, j.succ => C.d i j
        | x, x_1 => 0)
        (match (motive :=
          (x x_1 : ℕ) →
            Quiver.Hom.{v, u} (V := V)
              (match (motive := ℕ → V) x with
                | 0 => X
                | i.succ => C.X i :
                V)
              (match (motive := ℕ → V) x_1 with
                | 0 => X
                | i.succ => C.X i :
                V))
          j + 1 + 1, k + 1 + 1 with
        | 0, 1 => f
        | i.succ, j.succ => C.d i j
        | x, x_1 => 0) :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) i with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) k + 1 + 1 with
          | 0 => X
          | i.succ => C.X i :
          V))
    (0 :
      Quiver.Hom.{v, u} (V := V)
        (match (motive := ℕ → V) i with
          | 0 => X
          | i.succ => C.X i :
          V)
        (match (motive := ℕ → V) k + 1 + 1 with
          | 0 => X
          | i.succ => C.X i :
          V))
Tactic: rcases j with (_ | _ | j)
Cleared hypotheses: j, hij, hjk