∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_3 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare)
  (F : CategoryTheory.Sheaf J AddCommGrpCat) {n : ℕ} (x : ↑(F.H' n S.X₂ ⊞ F.H' n S.X₃)),
  (CategoryTheory.Abelian.Ext.mk₀ S.shortComplex.f).comp
      (CategoryTheory.Abelian.Ext.biprodAddEquiv.symm
        ((CategoryTheory.ConcreteCategory.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).hom) x))
      ⋯ =
    (CategoryTheory.ConcreteCategory.hom (S.fromBiprod F n)) x