[GOAL]
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{?u.7905, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
E : ((Functor.leftDerived ((linearYoneda R C).obj Y).rightOp (n + 1)).obj X).unop ≅ 0.unop :=
  (Iso.unop (Functor.leftDerivedObjProjectiveSucc ((linearYoneda R C).obj Y).rightOp n X)).symm
⊢ 0 ≫ 0 = 𝟙 0.unop
[PROOFSTEP]
let Z : (ModuleCat R)ᵒᵖ := 0
[GOAL]
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{?u.7905, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
E : ((Functor.leftDerived ((linearYoneda R C).obj Y).rightOp (n + 1)).obj X).unop ≅ 0.unop :=
  (Iso.unop (Functor.leftDerivedObjProjectiveSucc ((linearYoneda R C).obj Y).rightOp n X)).symm
Z : (ModuleCat R)ᵒᵖ := 0
⊢ 0 ≫ 0 = 𝟙 0.unop
[PROOFSTEP]
rw [← (0 : 0 ⟶ Z.unop).unop_op, ← (0 : Z.unop ⟶ 0).unop_op, ← unop_id, ← unop_comp]
[GOAL]
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{?u.10674, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
E : ((Functor.leftDerived ((linearYoneda R C).obj Y).rightOp (n + 1)).obj X).unop ≅ 0.unop :=
  (Iso.unop (Functor.leftDerivedObjProjectiveSucc ((linearYoneda R C).obj Y).rightOp n X)).symm
Z : (ModuleCat R)ᵒᵖ := 0
⊢ (0.op ≫ 0.op).unop = (𝟙 0).unop
[PROOFSTEP]
aesop
