-- Module: Mathlib.Algebra.Homology.HomologicalComplex
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) ⋯)))
rw :
  (mkAux X₀ X₁ X₂ d₀ d₁ s succ (n + 2)).g =
    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)))
⊢ Eq.{v + 1} (α := (mkAux X₀ X₁ X₂ d₀ d₁ s succ (n + 3)).X₃ ⟶ (mkAux X₀ X₁ X₂ d₀ d₁ s succ (n + 2)).X₃)
    (if h : n + 3 = n + 2 + 1 then eqToHom ⋯ ≫ (mkAux X₀ X₁ X₂ d₀ d₁ s succ (n + 2)).g else 0)
    (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))))

Tactic:
rw [dif_pos (by rfl), eqToHom_refl, id_comp]

Premises used: dif_pos, CategoryTheory.eqToHom_refl, CategoryTheory.Category.id_comp