-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (hypothesis)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex.{v, u} V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
n : ℕ
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 3) (n + 2) =
    (mkXIso X₀ X₁ X₂ d₀ d₁ s succ n).hom ≫
      PSigma.fst (β :=
        fun
          (d₂ :
            PSigma.fst (β := fun (X₃ : V) ↦
                (d₂ :
                  X₃ ⟶
                    (ShortComplex.mk (X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2)) (X₂ :=
                        (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1)) ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1))
                        ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n) ⋯).X₁) ×'
                  d₂ ≫
                      (ShortComplex.mk (X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2)) (X₂ :=
                          (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1)) ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1))
                          ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n) ⋯).f =
                    0)
                (succ
                  (ShortComplex.mk (X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2)) (X₂ :=
                    (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1)) ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1))
                    ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n) ⋯)) ⟶
              (ShortComplex.mk (X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2)) (X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1))
                  ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1)) ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n) ⋯).X₁) ↦
        d₂ ≫
            (ShortComplex.mk (X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2)) (X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1))
                ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1)) ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n) ⋯).f =
          0)
        (PSigma.snd (β := fun (X₃ : V) ↦
          (d₂ :
            X₃ ⟶
              (ShortComplex.mk (X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2)) (X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1))
                  ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1)) ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n) ⋯).X₁) ×'
            d₂ ≫
                (ShortComplex.mk (X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2)) (X₂ :=
                    (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1)) ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1))
                    ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n) ⋯).f =
              0)
          (succ
            (ShortComplex.mk (X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2)) (X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1))
              ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1)) ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n) ⋯)))
have eq : PSigma.fst (β :=
    fun
      (d₂ :
        PSigma.fst (β := fun (X₃ : V) ↦
            (d₂ : X₃ ⟶ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n).X₁) ×' d₂ ≫ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n).f = 0)
            (succ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n)) ⟶
          (mkAux X₀ X₁ X₂ d₀ d₁ s succ n).X₁) ↦
    d₂ ≫ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n).f = 0)
    (PSigma.snd (β := fun (X₃ : V) ↦
      (d₂ : X₃ ⟶ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n).X₁) ×' d₂ ≫ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n).f = 0)
      (succ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n))) =
  eqToHom sorry ≫
    PSigma.fst (β :=
        fun
          (d₂ :
            PSigma.fst (β := fun (X₃ : V) ↦
                (d₂ :
                  X₃ ⟶
                    (ShortComplex.mk (X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2)) (X₂ :=
                        (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1)) ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1))
                        ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n) sorry).X₁) ×'
                  d₂ ≫
                      (ShortComplex.mk (X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2)) (X₂ :=
                          (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1)) ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1))
                          ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n) sorry).f =
                    0)
                (succ
                  (ShortComplex.mk (X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2)) (X₂ :=
                    (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1)) ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1))
                    ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n) sorry)) ⟶
              (ShortComplex.mk (X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2)) (X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1))
                  ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1)) ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n) sorry).X₁) ↦
        d₂ ≫
            (ShortComplex.mk (X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2)) (X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1))
                ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1)) ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n) sorry).f =
          0)
        (PSigma.snd (β := fun (X₃ : V) ↦
          (d₂ :
            X₃ ⟶
              (ShortComplex.mk (X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2)) (X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1))
                  ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1)) ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n) sorry).X₁) ×'
            d₂ ≫
                (ShortComplex.mk (X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2)) (X₂ :=
                    (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1)) ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1))
                    ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n) sorry).f =
              0)
          (succ
            (ShortComplex.mk (X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2)) (X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1))
              ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1)) ((mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n) sorry))) ≫
      eqToHom sorry
Tactic: have eq := mk_congr_succ_d₂ succ
    (mkAux_eq_shortComplex_mk_d_comp_d X₀ X₁ X₂ d₀ d₁ s succ n)