-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
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
⊢ 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)
have 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 sorry else 0, comm' := sorry },
                  inv := { f := fun (i : ι) ↦ if h : i = j then eqToHom sorry else 0, comm' := sorry }, hom_inv_id := sorry,
                  inv_hom_id := sorry } :
                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 sorry else 0, comm' := sorry },
                  inv := { f := fun (i : ι) ↦ if h : i = j then eqToHom sorry else 0, comm' := sorry }, hom_inv_id := sorry,
                  inv_hom_id := sorry } :
                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)
Tactic: ext i