∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.GrothendieckTopology C}
  {inst_1 : CategoryTheory.HasWeakSheafify J (Type v)} {toSquare : CategoryTheory.Square C}
  {mono_f₁₃ :
    autoParam (CategoryTheory.Mono toSquare.f₁₃)
      CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mono_f₁₃._autoParam}
  {isPushout : (toSquare.map (CategoryTheory.yoneda.comp (CategoryTheory.presheafToSheaf J (Type v)))).IsPushout}
  {toSquare_1 : CategoryTheory.Square C}
  {mono_f₁₃_1 :
    autoParam (CategoryTheory.Mono toSquare_1.f₁₃)
      CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mono_f₁₃._autoParam}
  {isPushout_1 : (toSquare_1.map (CategoryTheory.yoneda.comp (CategoryTheory.presheafToSheaf J (Type v)))).IsPushout},
  { toSquare := toSquare, mono_f₁₃ := mono_f₁₃, isPushout := isPushout } =
      { toSquare := toSquare_1, mono_f₁₃ := mono_f₁₃_1, isPushout := isPushout_1 } →
    toSquare = toSquare_1