-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris (goal)
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)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have 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
        sorry)
      (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
        sorry))
    sorry =
  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))
Tactic: rw [Ext.biprodAddEquiv_symm_apply,
    Iso.addCommGroupIsoToAddEquiv_symm_apply,
    fromBiprod_biprodIsoProd_inv_apply]