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