-- Module: Mathlib.Algebra.Homology.HomologicalComplex
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
n : ℕ
zero :
  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))))
succ :
  ∀ (n : ℕ),
    Eq (α :=
      HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 2) ⟶
        HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1))
      (HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 2) (n + 1 + 1))
      (Iso.hom (mk'XIso X₀ X₁ d₀ (fun {X₀ X₁ : V} ↦ succ') (n + 1)) ≫
        PSigma.fst (β :=
          fun
            (d :
              PSigma.fst (β := fun (X₂ : V) ↦
                  (d : X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1)) ×'
                    Eq (α := X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1))
                      (d ≫ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1) (n + 1)) 0)
                  (succ' (HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1) (n + 1))) ⟶
                HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1)) ↦
          Eq (α :=
            PSigma.fst (β := fun (X₂ : V) ↦
                (d : X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1)) ×'
                  Eq (α := X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1))
                    (d ≫ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1) (n + 1)) 0)
                (succ' (HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1) (n + 1))) ⟶
              HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1))
            (d ≫ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1) (n + 1)) 0)
          (PSigma.snd (β := fun (X₂ : V) ↦
            (d : X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1)) ×'
              Eq (α := X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1))
                (d ≫ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1) (n + 1)) 0)
            (succ' (HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1 + 1) (n + 1)))))
⊢ Eq (α :=
    HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 2) ⟶
      HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1))
    (HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 2) (n + 1))
    (Iso.hom (mk'XIso X₀ X₁ d₀ (fun {X₀ X₁ : V} ↦ succ') n) ≫
      PSigma.fst (β :=
        fun
          (d :
            PSigma.fst (β := fun (X₂ : V) ↦
                (d : X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1)) ×'
                  d ≫ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1) n = 0)
                (succ' (HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1) n)) ⟶
              HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1)) ↦
        d ≫ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1) n = 0)
        (PSigma.snd (β := fun (X₂ : V) ↦
          (d : X₂ ⟶ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1)) ×'
            d ≫ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1) n = 0)
          (succ' (HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') (n + 1) n))))

Tactic:
obtain _ | n := n