∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.InjectiveResolution Y) {n : ℕ}
  (f g : X ⟶ R.cocomplex.X n) (m : ℕ) (hm : n + 1 = m)
  (hf : CategoryTheory.CategoryStruct.comp f (R.cocomplex.d n m) = 0)
  (hg : CategoryTheory.CategoryStruct.comp g (R.cocomplex.d n m) = 0),
  R.extMk f m hm hf + R.extMk g m hm hg = R.extMk (f + g) m hm ⋯