-- 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
X Y : C
n : ℕ
inst_3 : HasDerivedCategory.{w', v, u} C
α β : Ext.{w, v, u} X Y n
α' : Ext.{w, v, u} (biprod.{v, u} X X) Y n := comp (mk₀ biprod.fst) α ⋯
β' : Ext.{w, v, u} (biprod.{v, u} X X) Y n := comp (mk₀ biprod.snd) β ⋯
eq₁ : α + β = comp (mk₀ (biprod.lift (𝟙 X) (𝟙 X))) (α' + β') ⋯
eq₂ :
  α' + β' =
    (Equiv.symm homEquiv :
        (a : ShiftedHom ((singleFunctor C 0).obj (X ⊞ X)) ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext (X ⊞ X) Y n)
      (HAdd.hAdd (α :=
        ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) (biprod.{v, u} X X))
          (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
        α'.hom β'.hom)
e_a :
  Eq.{w' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (ShiftedHom.comp
      (ShiftedHom.mk₀ 0 mk₀._proof_1
        (CategoryStruct.comp (Y := Functor.obj (singleFunctor C 0) (biprod.{v, u} X X))
          (Functor.map (singleFunctor C 0) (biprod.lift (𝟙 X) (𝟙 X))) (Functor.map (singleFunctor C 0) biprod.fst)))
      α.hom ⋯)
    α.hom
e_a₁ :
  Eq.{w' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (ShiftedHom.comp
      (ShiftedHom.mk₀ 0 mk₀._proof_1
        (Functor.map (singleFunctor C 0)
          (CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) biprod.fst)))
      α.hom ⋯)
    α.hom
e_a₂ :
  Eq.{w' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (ShiftedHom.comp (ShiftedHom.mk₀ 0 mk₀._proof_1 (Functor.map (singleFunctor C 0) (𝟙 X))) α.hom ⋯) α.hom
e_a₃ :
  Eq.{w' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (ShiftedHom.comp (ShiftedHom.mk₀ 0 mk₀._proof_1 (𝟙 (Functor.obj (singleFunctor C 0) X))) α.hom ⋯) α.hom
e_a₄ e_a₅ :
  Eq.{w' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    α.hom α.hom
⊢ Eq.{w' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (ShiftedHom.comp (Y := Functor.obj (singleFunctor C 0) (biprod.{v, u} X X))
      (ShiftedHom.mk₀ 0 mk₀._proof_1 (Functor.map (singleFunctor C 0) (biprod.lift (𝟙 X) (𝟙 X))))
      (ShiftedHom.comp (ShiftedHom.mk₀ 0 mk₀._proof_1 (Functor.map (singleFunctor C 0) biprod.fst)) α.hom ⋯) ⋯)
    α.hom

Tactic:
rw [ShiftedHom.mk₀_comp_mk₀_assoc, ← Functor.map_comp,
      biprod.lift_fst, Functor.map_id, ShiftedHom.mk₀_id_comp]

Premises used: CategoryTheory.ShiftedHom.mk₀_id_comp, CategoryTheory.Limits.biprod.lift_fst, CategoryTheory.ShiftedHom.mk₀_comp_mk₀_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp