-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorShift (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
K₂ L₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
y : ℤ
inst_8 : K₁.HasMapBifunctor K₂ F
inst_9 : K₁.HasMapBifunctor L₂ F
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
      (HomologicalComplex.mapBifunctor K₁
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) K₂) F
        (ComplexShape.up ℤ))
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y) (K₁.mapBifunctor L₂ F)))
    (CategoryStruct.comp (Y :=
        HomologicalComplex.mapBifunctor K₁
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) L₂) F
          (ComplexShape.up ℤ))
        (mapBifunctorMap (𝟙 K₁)
            (CategoryTheory.Functor.map
              (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) f₂)
            F (ComplexShape.up ℤ) :
          Quiver.Hom (V := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
            (HomologicalComplex.mapBifunctor K₁
              (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) K₂)
              F (ComplexShape.up ℤ))
            (HomologicalComplex.mapBifunctor K₁
              (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) L₂)
              F (ComplexShape.up ℤ)))
        (Iso.hom (K₁.mapBifunctorShift₂Iso L₂ F y) :
          Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
            (K₁.mapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) L₂) F)
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y) (K₁.mapBifunctor L₂ F))) :
      Quiver.Hom (V := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
        (HomologicalComplex.mapBifunctor K₁
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) K₂) F
          (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y) (K₁.mapBifunctor L₂ F)))
    (CategoryStruct.comp (Y :=
        Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y) (K₁.mapBifunctor K₂ F))
        (Iso.hom (K₁.mapBifunctorShift₂Iso K₂ F y) :
          Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
            (K₁.mapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F)
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y) (K₁.mapBifunctor K₂ F)))
        (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y)
            (mapBifunctorMap (𝟙 K₁) f₂ F (ComplexShape.up ℤ)) :
          Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y) (K₁.mapBifunctor K₂ F))
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y)
              (HomologicalComplex.mapBifunctor K₁ L₂ F (ComplexShape.up ℤ)))) :
      Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
        (K₁.mapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂) F)
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y)
          (HomologicalComplex.mapBifunctor K₁ L₂ F (ComplexShape.up ℤ))))
have h : ∀ (n p q : ℤ) (h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = n),
  Eq (α :=
    (F.obj (K₁.X p)).obj
        ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) K₂).X
          q) ⟶
      X (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y) (K₁.mapBifunctor L₂ F)) n)
    (CategoryStruct.comp (Y :=
        X
          (HomologicalComplex.mapBifunctor K₁
            (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) K₂) F
            (ComplexShape.up ℤ))
          n)
        (HomologicalComplex.ιMapBifunctor K₁
            (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) K₂) F
            (ComplexShape.up ℤ) p q n h :
          (F.obj (K₁.X p)).obj
              ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y)
                    K₂).X
                q) ⟶
            X
              (HomologicalComplex.mapBifunctor K₁
                (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y)
                  K₂)
                F (ComplexShape.up ℤ))
              n)
        (Hom.f
            (CategoryStruct.comp (Y :=
              HomologicalComplex.mapBifunctor K₁
                (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y)
                  L₂)
                F (ComplexShape.up ℤ))
              (mapBifunctorMap (𝟙 K₁)
                  (CategoryTheory.Functor.map
                    (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) f₂)
                  F (ComplexShape.up ℤ) :
                Quiver.Hom (V := HomologicalComplex.{v_3, u_3, 0} D (ComplexShape.up ℤ))
                  (HomologicalComplex.mapBifunctor K₁
                    (Functor.obj
                      (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) K₂)
                    F (ComplexShape.up ℤ))
                  (HomologicalComplex.mapBifunctor K₁
                    (Functor.obj
                      (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) L₂)
                    F (ComplexShape.up ℤ)))
              (Iso.hom (K₁.mapBifunctorShift₂Iso L₂ F y) :
                Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
                  (K₁.mapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) L₂)
                    F)
                  (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y)
                    (K₁.mapBifunctor L₂ F))))
            n :
          X
              (HomologicalComplex.mapBifunctor K₁
                (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y)
                  K₂)
                F (ComplexShape.up ℤ))
              n ⟶
            X (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y) (K₁.mapBifunctor L₂ F))
              n) :
      (F.obj (K₁.X p)).obj
          ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) K₂).X
            q) ⟶
        X (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y) (K₁.mapBifunctor L₂ F)) n)
    (CategoryStruct.comp (Y :=
        X
          (HomologicalComplex.mapBifunctor K₁
            (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) K₂) F
            (ComplexShape.up ℤ))
          n)
        (HomologicalComplex.ιMapBifunctor K₁
            (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) K₂) F
            (ComplexShape.up ℤ) p q n h :
          (F.obj (K₁.X p)).obj
              ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y)
                    K₂).X
                q) ⟶
            X
              (HomologicalComplex.mapBifunctor K₁
                (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y)
                  K₂)
                F (ComplexShape.up ℤ))
              n)
        (Hom.f
            (CategoryStruct.comp (Y :=
              Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y) (K₁.mapBifunctor K₂ F))
              (Iso.hom (K₁.mapBifunctorShift₂Iso K₂ F y) :
                Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
                  (K₁.mapBifunctor (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) y) K₂)
                    F)
                  (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y)
                    (K₁.mapBifunctor K₂ F)))
              (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y)
                  (mapBifunctorMap (𝟙 K₁) f₂ F (ComplexShape.up ℤ)) :
                Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
                  (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y)
                    (K₁.mapBifunctor K₂ F))
                  (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y)
                    (HomologicalComplex.mapBifunctor K₁ L₂ F (ComplexShape.up ℤ)))))
            n :
          X
              (HomologicalComplex.mapBifunctor K₁
                (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y)
                  K₂)
                F (ComplexShape.up ℤ))
              n ⟶
            X (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y) (K₁.mapBifunctor L₂ F))
              n) :
      (F.obj (K₁.X p)).obj
          ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_2, u_2, 0} C₂ (ComplexShape.up ℤ)) y) K₂).X
            q) ⟶
        X (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) y) (K₁.mapBifunctor L₂ F)) n)
Tactic: ext n p q h