-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ : V
d₀ : X₁ ⟶ X₀
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
⊢ (succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
      fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦ d ≫ d₀ = 0) =
    eqToHom ⋯ ≫
      PSigma.fst (β :=
        fun
          (d :
            PSigma.fst (β := fun (X₂ : V) ↦
                (d : X₂ ⟶ X₁) ×'
                  Eq (α := X₂ ⟶ X₀)
                    (d ≫
                      (mk X₀ X₁ ((succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)) d₀
                            ((succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
                              fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦
                              d ≫ d₀ = 0))
                            ⋯ fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
                        1 0)
                    0)
                (succ'
                    ((mk X₀ X₁ ((succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)) d₀
                          ((succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
                            fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦
                            d ≫ d₀ = 0))
                          ⋯ fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
                      1 0) :
                  (X₂ : V) ×'
                    (d : X₂ ⟶ X₁) ×'
                      Eq (α := X₂ ⟶ X₀)
                        (d ≫
                          (mk X₀ X₁ ((succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)) d₀
                                ((succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
                                  fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦
                                  d ≫ d₀ = 0))
                                ⋯ fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
                            1 0)
                        0) ⟶
              X₁) ↦
        Eq (α :=
          PSigma.fst (β := fun (X₂ : V) ↦
              (d : X₂ ⟶ X₁) ×'
                Eq (α := X₂ ⟶ X₀)
                  (d ≫
                    (mk X₀ X₁ ((succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)) d₀
                          ((succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
                            fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦
                            d ≫ d₀ = 0))
                          ⋯ fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
                      1 0)
                  0)
              (succ'
                  ((mk X₀ X₁ ((succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)) d₀
                        ((succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
                          fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦ d ≫ d₀ = 0))
                        ⋯ fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
                    1 0) :
                (X₂ : V) ×'
                  (d : X₂ ⟶ X₁) ×'
                    Eq (α := X₂ ⟶ X₀)
                      (d ≫
                        (mk X₀ X₁ ((succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)) d₀
                              ((succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
                                fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦
                                d ≫ d₀ = 0))
                              ⋯ fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
                          1 0)
                      0) ⟶
            X₀)
          (d ≫
            (mk X₀ X₁ ((succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)) d₀
                  ((succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
                    fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦ d ≫ d₀ = 0))
                  ⋯ fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
              1 0)
          0)
        (PSigma.snd (β := fun (X₂ : V) ↦
          (d : X₂ ⟶ X₁) ×'
            Eq (α := X₂ ⟶ X₀)
              (d ≫
                (mk X₀ X₁ ((succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)) d₀
                      ((succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
                        fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦ d ≫ d₀ = 0))
                      ⋯ fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
                  1 0)
              0)
          (succ'
              ((mk X₀ X₁ ((succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)) d₀
                    ((succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
                      fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦ d ≫ d₀ = 0))
                    ⋯ fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
                1 0) :
            (X₂ : V) ×'
              (d : X₂ ⟶ X₁) ×'
                Eq (α := X₂ ⟶ X₀)
                  (d ≫
                    (mk X₀ X₁ ((succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)) d₀
                          ((succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
                            fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦
                            d ≫ d₀ = 0))
                          ⋯ fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
                      1 0)
                  0))
have zero : d₀ =
  (mk X₀ X₁ ((succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)) d₀
        ((succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
          fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦ d ≫ d₀ = 0))
        sorry fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
    1 0
Tactic: apply mk'_congr_succ'_d