-- 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
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))))
⊢ 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))))
have 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)))))
Tactic: obtain _ | n := n
Cleared hypotheses: n