-- 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
⊢ Eq (α :=
    HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 2) ⟶
      HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1))
    (HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
    (Iso.hom (mk'XIso X₀ X₁ d₀ (fun {X₀ X₁ : V} ↦ succ') 0) ≫
      PSigma.fst (β :=
        fun
          (d :
            PSigma.fst (β := fun (X₂ : V) ↦
                (d : X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1)) ×'
                  Eq (α := X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') 0)
                    (d ≫ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1) 0) 0)
                (succ' (HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1) 0)) ⟶
              HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1)) ↦
        Eq (α :=
          PSigma.fst (β := fun (X₂ : V) ↦
              (d : X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1)) ×'
                Eq (α := X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') 0)
                  (d ≫ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1) 0) 0)
              (succ' (HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1) 0)) ⟶
            HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') 0)
          (d ≫ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1) 0) 0)
        (PSigma.snd (β := fun (X₂ : V) ↦
          (d : X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1)) ×'
            Eq (α := X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') 0)
              (d ≫ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1) 0) 0)
          (succ' (HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (HAdd.hAdd (α := ℕ) 0 1) 0))))
have zero : (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
    2 1 =
  eqToHom sorry ≫
    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))
                          sorry 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))
                        sorry 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))
                              sorry 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))
                        sorry 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))
                      sorry 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))
                            sorry 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))
                sorry 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))
                    sorry 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))
                  sorry 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))
                        sorry fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
                    1 0)
                0))
Tactic: dsimp [mk'XIso, mk']