-- 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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst_8 : ∀ (K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ) (K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂_1 : CochainComplex.{v_2, u_2, 0} C₂ ℤ
K₂ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
n : ℤ
⊢ Eq (α :=
    X (mapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂) K₂_1 F (ComplexShape.up ℤ))
        n ⟶
      X (mapBifunctor K₂ K₂_1 F (ComplexShape.up ℤ)) (n + 0))
    (Hom.f (Iso.hom (K₂.mapBifunctorShift₁Iso K₂_1 F 0)) n :
      X (mapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂) K₂_1 F (ComplexShape.up ℤ))
          n ⟶
        X
          (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) (A := ℤ) 0)
            (mapBifunctor K₂ K₂_1 F (ComplexShape.up ℤ)))
          n)
    (Hom.f (NatTrans.app (Iso.hom (CommShift.isoZero (obj (Functor.flip F.map₂CochainComplex) K₂_1) ℤ)) K₂) n :
      X (mapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂) K₂_1 F (ComplexShape.up ℤ))
          n ⟶
        X
          (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) (A := ℤ) 0)
            (mapBifunctor K₂ K₂_1 F (ComplexShape.up ℤ)))
          n)
have w : ∀ (p q : ℤ) (h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = n),
  Eq (α :=
    (F.obj ((obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂).X p)).obj (K₂_1.X q) ⟶
      X (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) (A := ℤ) 0) (mapBifunctor K₂ K₂_1 F (ComplexShape.up ℤ)))
        n)
    (CategoryStruct.comp (Y :=
        X
          (mapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂) K₂_1 F
            (ComplexShape.up ℤ))
          n)
        (ιMapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂) K₂_1 F (ComplexShape.up ℤ)
            p q n h :
          (F.obj ((obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂).X p)).obj (K₂_1.X q) ⟶
            X
              (mapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂) K₂_1 F
                (ComplexShape.up ℤ))
              n)
        (Hom.f (Iso.hom (K₂.mapBifunctorShift₁Iso K₂_1 F 0)) n :
          X
              (mapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂) K₂_1 F
                (ComplexShape.up ℤ))
              n ⟶
            X
              (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) (A := ℤ) 0)
                (mapBifunctor K₂ K₂_1 F (ComplexShape.up ℤ)))
              n) :
      (F.obj ((obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂).X p)).obj (K₂_1.X q) ⟶
        X
          (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) (A := ℤ) 0)
            (mapBifunctor K₂ K₂_1 F (ComplexShape.up ℤ)))
          n)
    (CategoryStruct.comp (Y :=
        X
          (mapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂) K₂_1 F
            (ComplexShape.up ℤ))
          n)
        (ιMapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂) K₂_1 F (ComplexShape.up ℤ)
          p q n h)
        (Hom.f (NatTrans.app (Iso.hom (CommShift.isoZero (obj (Functor.flip F.map₂CochainComplex) K₂_1) ℤ)) K₂) n) :
      (F.obj ((obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂).X p)).obj (K₂_1.X q) ⟶
        X
          (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) (A := ℤ) 0)
            (mapBifunctor K₂ K₂_1 F (ComplexShape.up ℤ)))
          n)
Tactic: ext p q h