-- 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
zero :
  (mk X₀ X₁ ((succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)) d₀
          ((succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
            fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦ d ≫ d₀ = 0))
          ⋯ fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
      2 1 =
    eqToHom ⋯ ≫
      PSigma.fst (β :=
        fun
          (d :
            PSigma.fst (β := fun (X₂ : V) ↦
                (d : X₂ ⟶ X₁) ×'
                  Eq (α := X₂ ⟶ X₀)
                    (d ≫
                      (mk X₀ X₁ ((succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)) d₀
                            ((succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
                              fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦
                              d ≫ d₀ = 0))
                            ⋯ fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
                        1 0)
                    0)
                (succ'
                    ((mk X₀ X₁ ((succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)) d₀
                          ((succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
                            fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦
                            d ≫ d₀ = 0))
                          ⋯ fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
                      1 0) :
                  (X₂ : V) ×'
                    (d : X₂ ⟶ X₁) ×'
                      Eq (α := X₂ ⟶ X₀)
                        (d ≫
                          (mk X₀ X₁ ((succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)) d₀
                                ((succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
                                  fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦
                                  d ≫ d₀ = 0))
                                ⋯ fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
                            1 0)
                        0) ⟶
              X₁) ↦
        Eq (α :=
          PSigma.fst (β := fun (X₂ : V) ↦
              (d : X₂ ⟶ X₁) ×'
                Eq (α := X₂ ⟶ X₀)
                  (d ≫
                    (mk X₀ X₁ ((succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)) d₀
                          ((succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
                            fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦
                            d ≫ d₀ = 0))
                          ⋯ fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
                      1 0)
                  0)
              (succ'
                  ((mk X₀ X₁ ((succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)) d₀
                        ((succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
                          fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦ d ≫ d₀ = 0))
                        ⋯ fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
                    1 0) :
                (X₂ : V) ×'
                  (d : X₂ ⟶ X₁) ×'
                    Eq (α := X₂ ⟶ X₀)
                      (d ≫
                        (mk X₀ X₁ ((succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)) d₀
                              ((succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
                                fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦
                                d ≫ d₀ = 0))
                              ⋯ fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
                          1 0)
                      0) ⟶
            X₀)
          (d ≫
            (mk X₀ X₁ ((succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)) d₀
                  ((succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
                    fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦ d ≫ d₀ = 0))
                  ⋯ fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
              1 0)
          0)
        (PSigma.snd (β := fun (X₂ : V) ↦
          (d : X₂ ⟶ X₁) ×'
            Eq (α := X₂ ⟶ X₀)
              (d ≫
                (mk X₀ X₁ ((succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)) d₀
                      ((succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
                        fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦ d ≫ d₀ = 0))
                      ⋯ fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
                  1 0)
              0)
          (succ'
              ((mk X₀ X₁ ((succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)) d₀
                    ((succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
                      fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦ d ≫ d₀ = 0))
                    ⋯ fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
                1 0) :
            (X₂ : V) ×'
              (d : X₂ ⟶ X₁) ×'
                Eq (α := X₂ ⟶ X₀)
                  (d ≫
                    (mk X₀ X₁ ((succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0)) d₀
                          ((succ' d₀).snd (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0).fst (β :=
                            fun (d : (succ' d₀).fst (β := fun (X₂ : V) ↦ (d : X₂ ⟶ X₁) ×' d ≫ d₀ = 0) ⟶ X₁) ↦
                            d ≫ d₀ = 0))
                          ⋯ fun (S : ShortComplex.{v, u} V) ↦ succ' S.f).d
                      1 0)
                  0))
⊢ 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:
dsimp [mk'XIso, mk']

Premises used: ChainComplex.mk'XIso, ChainComplex.mk'