-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Ext (goal)
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
⊢ 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))
have 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))
Tactic: obtain rfl : x = 0 := (HomologicalComplex.isZero_single_obj_X
    (ComplexShape.down ℕ) 0 X (n + 1) (by simp)).eq_of_src _ _
Cleared hypotheses: x