-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
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)
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)
⊢ 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

Tactic:
apply BinaryCofan.IsColimit.hom_ext
    (isBinaryBilimitOfPreserves (singleFunctor C 0)
      (BinaryBiproduct.isBilimit X₁ X₂)).isColimit

Premises used: CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext, OfNat.ofNat, DerivedCategory.singleFunctor, CategoryTheory.Limits.BinaryBiproduct.isBilimit, CategoryTheory.Limits.BinaryBicone.IsBilimit.isColimit, CategoryTheory.Limits.isBinaryBilimitOfPreserves