-- 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₁ L₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
f : K₁ ⟶ L₁
n : ℤ
K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ
d : ℤ
⊢ Eq (α :=
    X (mapBifunctor K₁ (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂) F (ComplexShape.up ℤ)) d ⟶
      X (mapBifunctor L₁ K₂ F (ComplexShape.up ℤ)) (d + n))
    (CategoryStruct.comp (Y := X (mapBifunctor K₁ K₂ F (ComplexShape.up ℤ)) (d + n))
        (Hom.f (NatTrans.app (Iso.hom (commShiftIso (obj F.map₂CochainComplex K₁) n)) K₂) d)
        (Hom.f (mapBifunctorMap f (𝟙 K₂) F (ComplexShape.up ℤ)) (d + n)) :
      X (mapBifunctor K₁ (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂) F (ComplexShape.up ℤ)) d ⟶
        X (mapBifunctor L₁ K₂ F (ComplexShape.up ℤ)) (d + n))
    (CategoryStruct.comp (Y :=
        X (mapBifunctor L₁ (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂) F (ComplexShape.up ℤ)) d)
        (Hom.f
          (mapBifunctorMap f (𝟙 (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂)) F (ComplexShape.up ℤ)) d)
        (Hom.f (NatTrans.app (Iso.hom (commShiftIso (obj F.map₂CochainComplex L₁) n)) K₂) d) :
      X (mapBifunctor K₁ (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂) F (ComplexShape.up ℤ)) d ⟶
        X (mapBifunctor L₁ K₂ F (ComplexShape.up ℤ)) (d + n))
have w : ∀ (p q : ℤ) (h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = d),
  Eq (α :=
    (F.obj (K₁.X p)).obj ((obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂).X q) ⟶
      X (mapBifunctor L₁ K₂ F (ComplexShape.up ℤ)) (d + n))
    (CategoryStruct.comp (Y :=
      X (mapBifunctor K₁ (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂) F (ComplexShape.up ℤ)) d)
      (ιMapBifunctor K₁ (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂) F (ComplexShape.up ℤ) p q d h)
      (CategoryStruct.comp (Y := X (mapBifunctor K₁ K₂ F (ComplexShape.up ℤ)) (d + n))
        (Hom.f (NatTrans.app (Iso.hom (commShiftIso (obj F.map₂CochainComplex K₁) n)) K₂) d)
        (Hom.f (mapBifunctorMap f (𝟙 K₂) F (ComplexShape.up ℤ)) (d + n))))
    (CategoryStruct.comp (Y :=
      X (mapBifunctor K₁ (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂) F (ComplexShape.up ℤ)) d)
      (ιMapBifunctor K₁ (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂) F (ComplexShape.up ℤ) p q d h)
      (CategoryStruct.comp (Y :=
        X (mapBifunctor L₁ (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂) F (ComplexShape.up ℤ)) d)
        (Hom.f
          (mapBifunctorMap f (𝟙 (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂)) F (ComplexShape.up ℤ)) d)
        (Hom.f (NatTrans.app (Iso.hom (commShiftIso (obj F.map₂CochainComplex L₁) n)) K₂) d)))
Tactic: ext p q h