-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext.{w, v, u} (biprod.{v, u} X₁ X₂) Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
h₁ :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X₁)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (Functor.map (singleFunctor C 0) biprod.inl ≫ α.hom) (Functor.map (singleFunctor C 0) biprod.inl ≫ β.hom)
h₂ :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X₂)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (Functor.map (singleFunctor C 0) biprod.inr ≫ α.hom) (Functor.map (singleFunctor C 0) biprod.inr ≫ β.hom)
h₃ :
  Eq (α :=
    Quiver.Hom (V := DerivedCategory C)
      (Functor.obj (pair (Functor.obj (singleFunctor C 0) X₁) (Functor.obj (singleFunctor C 0) X₂))
        { as := WalkingPair.left : Discrete WalkingPair })
      (Functor.obj (shiftFunctor (DerivedCategory C) (A := ℤ) (↑n : ℤ)) (Functor.obj (singleFunctor C 0) Y)))
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt (F := pair (Functor.obj (singleFunctor C 0) X₁) (Functor.obj (singleFunctor C 0) X₂))
            (BinaryBicone.toCocone (Functor.mapBinaryBicone (singleFunctor C 0) (BinaryBiproduct.bicone X₁ X₂)))))
        { as := WalkingPair.left : Discrete WalkingPair })
      (BinaryCofan.inl
        (BinaryBicone.toCocone (Functor.mapBinaryBicone (singleFunctor C 0) (BinaryBiproduct.bicone X₁ X₂))))
      α.hom)
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt (F := pair (Functor.obj (singleFunctor C 0) X₁) (Functor.obj (singleFunctor C 0) X₂))
            (BinaryBicone.toCocone (Functor.mapBinaryBicone (singleFunctor C 0) (BinaryBiproduct.bicone X₁ X₂)))))
        { as := WalkingPair.left : Discrete WalkingPair })
      (BinaryCofan.inl
        (BinaryBicone.toCocone (Functor.mapBinaryBicone (singleFunctor C 0) (BinaryBiproduct.bicone X₁ X₂))))
      β.hom)
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) (biprod.{v, u} X₁ X₂))
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    α.hom β.hom
have h₄ : Eq (α :=
  Quiver.Hom (V := DerivedCategory C)
    (Functor.obj (pair (Functor.obj (singleFunctor C 0) X₁) (Functor.obj (singleFunctor C 0) X₂))
      { as := WalkingPair.right : Discrete WalkingPair })
    (Functor.obj (shiftFunctor (DerivedCategory C) (A := ℤ) (↑n : ℤ)) (Functor.obj (singleFunctor C 0) Y)))
  (CategoryStruct.comp (Y :=
    Functor.obj
      (Functor.obj (Functor.const (Discrete WalkingPair))
        (Cocone.pt (F := pair (Functor.obj (singleFunctor C 0) X₁) (Functor.obj (singleFunctor C 0) X₂))
          (BinaryBicone.toCocone (Functor.mapBinaryBicone (singleFunctor C 0) (BinaryBiproduct.bicone X₁ X₂)))))
      { as := WalkingPair.right : Discrete WalkingPair })
    (BinaryCofan.inr
      (BinaryBicone.toCocone (Functor.mapBinaryBicone (singleFunctor C 0) (BinaryBiproduct.bicone X₁ X₂))))
    α.hom)
  (CategoryStruct.comp (Y :=
    Functor.obj
      (Functor.obj (Functor.const (Discrete WalkingPair))
        (Cocone.pt (F := pair (Functor.obj (singleFunctor C 0) X₁) (Functor.obj (singleFunctor C 0) X₂))
          (BinaryBicone.toCocone (Functor.mapBinaryBicone (singleFunctor C 0) (BinaryBiproduct.bicone X₁ X₂)))))
      { as := WalkingPair.right : Discrete WalkingPair })
    (BinaryCofan.inr
      (BinaryBicone.toCocone (Functor.mapBinaryBicone (singleFunctor C 0) (BinaryBiproduct.bicone X₁ X₂))))
    β.hom)
Tactic: apply BinaryCofan.IsColimit.hom_ext
    (isBinaryBilimitOfPreserves (singleFunctor C 0)
      (BinaryBiproduct.isBilimit X₁ X₂)).isColimit