-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f_1 : C ⟶ D
i : ι
inst_8 : HasZeroObject.{v_2, u_3} W₁
inst_9 : HasZeroObject.{v_3, u_4} W₂
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_10 : F.PreservesZeroMorphisms
c : ComplexShape ι
inst_11 : DecidableEq ι
j : ι
X Y : W₁
f : X ⟶ Y
h :
  ∀ (i : ι),
    Eq (α :=
      HomologicalComplex.X
          (Functor.obj
            (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) X)
          i ⟶
        HomologicalComplex.X (Functor.obj (F ⋙ single W₂ c j) Y) i)
      (Hom.f
        (CategoryTheory.Functor.map
            (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c))
            f ≫
          Iso.hom
            ((fun (X : W₁) ↦
                ({ hom := { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ },
                    inv := { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ }, hom_inv_id := ⋯,
                    inv_hom_id := ⋯ } :
                  Iso (C := HomologicalComplex.{v_3, u_4, u_1} W₂ c)
                    (Functor.obj
                      (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j)
                        (F.mapHomologicalComplex c))
                      X)
                    (Functor.obj (F ⋙ single W₂ c j) X)))
              Y))
        i)
      (Hom.f
        (Iso.hom
            ((fun (X : W₁) ↦
                ({ hom := { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ },
                    inv := { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ }, hom_inv_id := ⋯,
                    inv_hom_id := ⋯ } :
                  Iso (C := HomologicalComplex.{v_3, u_4, u_1} W₂ c)
                    (Functor.obj
                      (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j)
                        (F.mapHomologicalComplex c))
                      X)
                    (Functor.obj (F ⋙ single W₂ c j) X)))
              X) ≫
          CategoryTheory.Functor.map (F ⋙ single W₂ c j) f)
        i)
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_3, u_4, u_1} W₂ c)
      (Functor.obj
        (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) X)
      (Functor.obj (F ⋙ single W₂ c j) Y))
    (CategoryTheory.Functor.map
        (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) f ≫
      Iso.hom
        ((fun (X : W₁) ↦
            ({ hom := { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ },
                inv := { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ }, hom_inv_id := ⋯,
                inv_hom_id := ⋯ } :
              Iso (C := HomologicalComplex.{v_3, u_4, u_1} W₂ c)
                (Functor.obj
                  (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j)
                    (F.mapHomologicalComplex c))
                  X)
                (Functor.obj (F ⋙ single W₂ c j) X)))
          Y))
    (Iso.hom
        ((fun (X : W₁) ↦
            ({ hom := { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ },
                inv := { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ }, hom_inv_id := ⋯,
                inv_hom_id := ⋯ } :
              Iso (C := HomologicalComplex.{v_3, u_4, u_1} W₂ c)
                (Functor.obj
                  (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j)
                    (F.mapHomologicalComplex c))
                  X)
                (Functor.obj (F ⋙ single W₂ c j) X)))
          X) ≫
      CategoryTheory.Functor.map (F ⋙ single W₂ c j) f)

Tactic:
ext i