-- 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 : ChainComplex.{v, u, 0} V ℕ
i j : ℕ
zero :
  (ComplexShape.down ℕ).Rel 0 0 →
    Eq.{v + 1} (α := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0 ⟶ C.X 0)
      (CategoryStruct.comp (Y := C.X 0)
          (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x ⟶ C.X x) 0 with
          | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
          | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (n + 1)))
          (C.d 0 0) :
        ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0 ⟶ C.X 0)
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).d 0 0)
          (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x ⟶ C.X x) 0 with
          | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
          | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (n + 1))) :
        ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0 ⟶ C.X 0)
⊢ (ComplexShape.down ℕ).Rel 0 j →
    Eq.{v + 1} (α := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0 ⟶ C.X j)
      (CategoryStruct.comp (Y := C.X 0)
          (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x ⟶ C.X x) 0 with
          | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
          | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (n + 1)))
          (C.d 0 j) :
        ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0 ⟶ C.X j)
      (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).d 0 j ≫
          match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X x ⟶ C.X x) j with
          | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0)
          | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X (n + 1)) :
        ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) ⋯).X 0 ⟶ C.X j)
have succ : ∀ (j : ℕ),
  (ComplexShape.down ℕ).Rel 0 (j + 1) →
    Eq.{v + 1} (α := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) sorry).X 0 ⟶ C.X (j + 1))
      (CategoryStruct.comp (Y := C.X 0)
          (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) sorry).X x ⟶ C.X x) 0 with
          | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) sorry).X 0)
          | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) sorry).X (n + 1)))
          (C.d 0 (j + 1)) :
        ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) sorry).X 0 ⟶ C.X (j + 1))
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) sorry).X (j + 1))
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) sorry).d 0 (j + 1))
          (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) sorry).X x ⟶ C.X x)
            j + 1 with
          | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) sorry).X 0)
          | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) sorry).X (n + 1))) :
        ((Functor.obj truncate C).augment (X := C.X 0) (C.d 1 0) sorry).X 0 ⟶ C.X (j + 1))
Tactic: rcases j with - | j
Cleared hypotheses: j