-- 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 : ℕ
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 ⋯ ≫
      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) ⋯))) ≫
        eqToHom ⋯
⊢ (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)))
Tactic: set_option backward.isDefEq.respectTransparency false in
    rw [eqToHom_refl, comp_id] at eq
Cleared hypotheses: eq