∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (n : ℕ) {X₁ X₂ X₃ : Cᵒᵖ} (f : X₁ ⟶ X₂) (f' : X₂ ⟶ X₃),
  {
      app := fun Y =>
        AddCommGrpCat.ofHom
          (AddMonoidHom.mk'
            (fun α => (CategoryTheory.Abelian.Ext.mk₀ (CategoryTheory.CategoryStruct.comp f f').unop).comp α ⋯) ⋯),
      naturality := ⋯ } =
    CategoryTheory.CategoryStruct.comp
      {
        app := fun Y =>
          AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun α => (CategoryTheory.Abelian.Ext.mk₀ f.unop).comp α ⋯) ⋯),
        naturality := ⋯ }
      {
        app := fun Y =>
          AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun α => (CategoryTheory.Abelian.Ext.mk₀ f'.unop).comp α ⋯) ⋯),
        naturality := ⋯ }