-- Module: Mathlib.CategoryTheory.Abelian.Ext
Goal:
R : Type u_1
inst : Ring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Abelian.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : EnoughProjectives.{v_1, u_2} C
X Y : C
inst_5 : Projective.{v_1, u_2} X
n : ℕ
x :
  Opposite.unop (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1))) ⟶ Y
hf :
  Eq.{v_1 + 1} (α :=
    (↑(Functor.obj (Functor.obj (linearYoneda R C) Y)
          (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1)))) :
      Type v_1))
    ((ModuleCat.Hom.hom
            (𝟙
              (Functor.obj (Functor.obj (linearYoneda R C) Y)
                (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1))))) :
          (a :
              (↑(((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1)))) :
                Type v_1)) →
            (↑(((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1)))) : Type v_1))
        0 :
      (↑(Functor.obj (Functor.obj (linearYoneda R C) Y)
            (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1)))) :
        Type v_1))
    ((ModuleCat.Hom.hom 0 :
          (a :
              (↑(((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1)))) :
                Type v_1)) →
            (↑(((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1)))) : Type v_1))
        0 :
      (↑(Functor.obj (Functor.obj (linearYoneda R C) Y)
            (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1)))) :
        Type v_1))
⊢ Eq (α :=
    (↑(Functor.obj (Functor.obj (linearYoneda R C) Y)
          (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1)))) :
      Type v_1))
    ((ModuleCat.Hom.hom
            (𝟙
              (Functor.obj (Functor.obj (linearYoneda R C) Y)
                (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1))))) :
          (a :
              (↑(((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1)))) :
                Type v_1)) →
            (↑(((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1)))) : Type v_1))
        x :
      (↑(Functor.obj (Functor.obj (linearYoneda R C) Y)
            (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1)))) :
        Type v_1))
    ((ModuleCat.Hom.hom 0 :
          (a :
              (↑(((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1)))) :
                Type v_1)) →
            (↑(((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1)))) : Type v_1))
        x :
      (↑(Functor.obj (Functor.obj (linearYoneda R C) Y)
            (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1)))) :
        Type v_1))

Tactic:
obtain rfl : x = 0 := (HomologicalComplex.isZero_single_obj_X
    (ComplexShape.down ℕ) 0 X (n + 1) (by simp)).eq_of_src _ _

Premises used: HomologicalComplex.isZero_single_obj_X, HAdd.hAdd, CategoryTheory.Limits.IsZero.eq_of_src, Nat, ComplexShape.down, OfNat.ofNat, rfl