∀ {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)