-- Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasWeakSheafify J (Type v)
inst_2 : HasSheafify J AddCommGrpCat
inst_3 : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n : ℕ
x₂ : (↑(F.H' n S.X₂) : Type w)
x₃ : (↑(F.H' n S.X₃) : Type w)
rw :
  Ext.comp
      (Ext.mk₀
        (biprod.lift
          (Functor.map (presheafToSheaf J AddCommGrpCat)
            (Functor.whiskerRight (Functor.map yoneda S.f₁₂) AddCommGrpCat.free))
          (-Functor.map (presheafToSheaf J AddCommGrpCat)
              (Functor.whiskerRight (Functor.map yoneda S.f₁₃) AddCommGrpCat.free))))
      (HAdd.hAdd (α :=
        Ext
          (Functor.obj (presheafToSheaf J AddCommGrpCat) (Functor.obj yoneda S.X₂ ⋙ AddCommGrpCat.free) ⊞
            Functor.obj (presheafToSheaf J AddCommGrpCat) (Functor.obj yoneda S.X₃ ⋙ AddCommGrpCat.free))
          F n)
        (Ext.comp (Ext.mk₀ biprod.fst)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                  AddCommGrpCat.carrier) (X := F.H' n S.X₂ ⊞ F.H' n S.X₃)
                  (Iso.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃))) :
                (a : (↑(F.H' n S.X₂ ⊞ F.H' n S.X₃) : Type w)) → (↑(F.H' n S.X₂) : Type w) × (↑(F.H' n S.X₃) : Type w))
              ((AddCommGrpCat.Hom.hom (Iso.inv ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃))) :
                    (a : (↑(AddCommGrpCat.of ((↑(F.H' n S.X₂) : Type w) × (↑(F.H' n S.X₃) : Type w))) : Type w)) →
                      (↑(F.H' n S.X₂ ⊞ F.H' n S.X₃) : Type w))
                  (x₂, x₃) :
                (↑(F.H' n S.X₂ ⊞ F.H' n S.X₃) : Type w))).1
          ⋯)
        (Ext.comp (Ext.mk₀ biprod.snd)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                  AddCommGrpCat.carrier) (X := F.H' n S.X₂ ⊞ F.H' n S.X₃)
                  (Iso.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃))) :
                (a : (↑(F.H' n S.X₂ ⊞ F.H' n S.X₃) : Type w)) → (↑(F.H' n S.X₂) : Type w) × (↑(F.H' n S.X₃) : Type w))
              ((AddCommGrpCat.Hom.hom (Iso.inv ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃))) :
                    (a : (↑(AddCommGrpCat.of ((↑(F.H' n S.X₂) : Type w) × (↑(F.H' n S.X₃) : Type w))) : Type w)) →
                      (↑(F.H' n S.X₂ ⊞ F.H' n S.X₃) : Type w))
                  (x₂, x₃) :
                (↑(F.H' n S.X₂ ⊞ F.H' n S.X₃) : Type w))).2
          ⋯))
      ⋯ =
    HSub.hSub (α := (↑((F.cohomologyPresheaf n).obj (op S.X₁)) : Type w)) (β :=
      (↑((F.cohomologyPresheaf n).obj (op S.X₁)) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              AddCommGrpCat.carrier) ((F.cohomologyPresheaf n).map S.f₁₂.op) :
            (a : (↑((F.cohomologyPresheaf n).obj (op S.X₂)) : Type w)) →
              (↑((F.cohomologyPresheaf n).obj (op S.X₁)) : Type w))
          x₂ :
        (↑((F.cohomologyPresheaf n).obj (op S.X₁)) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              AddCommGrpCat.carrier) ((F.cohomologyPresheaf n).map S.f₁₃.op) :
            (a : (↑((F.cohomologyPresheaf n).obj (op S.X₃)) : Type w)) →
              (↑((F.cohomologyPresheaf n).obj (op S.X₁)) : Type w))
          x₃ :
        (↑((F.cohomologyPresheaf n).obj (op S.X₁)) : Type w))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [Ext.biprodAddEquiv_symm_apply,
    Iso.addCommGroupIsoToAddEquiv_symm_apply,
    fromBiprod_biprodIsoProd_inv_apply]

Premises used: CategoryTheory.Iso.addCommGroupIsoToAddEquiv_symm_apply, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_biprodIsoProd_inv_apply, CategoryTheory.Abelian.Ext.biprodAddEquiv_symm_apply