awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasSheafify J AddCommGrpCat
inst_2 : HasExt (Sheaf J AddCommGrpCat)
T : C
hT : Limits.IsTerminal.{v, u} T
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
x : (↑(F.obj (P := Presheaf.IsSheaf J).obj (op T)) : Type w)
⊢ Eq.{w + 1} (α := (↑(G.obj (P := Presheaf.IsSheaf J).obj (op T)) : Type w))
    ((equiv₀ G hT : (a : G.H 0) → (↑(G.obj.obj (op T)) : Type w))
        ((map f 0 : (a : F.H 0) → G.H 0)
          ((AddEquiv.symm (equiv₀ F hT) : (a : (↑(F.obj.obj (op T)) : Type w)) → F.H 0) x : F.H 0)) :
      (↑(G.obj (P := Presheaf.IsSheaf J).obj (op T)) : Type w))
    ((equiv₀ G hT : (a : G.H 0) → (↑(G.obj.obj (op T)) : Type w))
        ((AddEquiv.symm (equiv₀ G hT) : (a : (↑(G.obj.obj (op T)) : Type w)) → G.H 0)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                carrier) (X := F.obj (P := Presheaf.IsSheaf J).obj (op T)) (f.hom.app (op T)) :
              (a : (↑(F.obj.obj (op T)) : Type w)) → (↑(G.obj.obj (op T)) : Type w))
            x)) :
      (↑(G.obj (P := Presheaf.IsSheaf J).obj (op T)) : Type w))

Tactic:
simp [← H.equiv₀_naturality]

Premises used: CategoryTheory.Sheaf.H.equiv₀_naturality
-- Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasSheafify J AddCommGrpCat
inst_2 : HasExt (Sheaf J AddCommGrpCat)
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
n : ℕ
x : F.H n
⊢ (map f n : (a : F.H n) → G.H n) x = Ext.comp x (Ext.mk₀ f) ⋯

Tactic:
rfl

Premises used: CategoryTheory.Abelian.Ext.comp, CategoryTheory.Localization.SmallHom.comp, CategoryTheory.Localization.SmallShiftedHom.comp, rfl
-- Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasSheafify J AddCommGrpCat
inst_2 : HasExt (Sheaf J AddCommGrpCat)
F : Sheaf J AddCommGrpCat
n : ℕ
x : F.H n
⊢ (map (𝟙 F) n : (a : F.H n) → F.H n) x = x

Tactic:
simp [H.map_apply]

Premises used: CategoryTheory.Sheaf.H.map_apply
-- Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasSheafify J AddCommGrpCat
inst_2 : HasExt (Sheaf J AddCommGrpCat)
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
n : ℕ
G' : Sheaf J AddCommGrpCat
g : G ⟶ G'
x : F.H n
⊢ Eq (α := G'.H n) ((map (f ≫ g) n : (a : F.H n) → G'.H n) x : G'.H n)
    ((map g n : (a : G.H n) → G'.H n) ((map f n : (a : F.H n) → G.H n) x : G.H n) : G'.H n)

Tactic:
simp [H.map_apply]

Premises used: CategoryTheory.Sheaf.H.map_apply
-- Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasSheafify J AddCommGrpCat
inst_2 : HasExt (Sheaf J AddCommGrpCat)
F G : Sheaf J AddCommGrpCat
n : ℕ
f g : F ⟶ G
x : F.H n
⊢ (map (f + g) n : (a : F.H n) → G.H n) x =
    HAdd.hAdd (α := G.H n) (β := G.H n) ((map f n : (a : F.H n) → G.H n) x : G.H n)
      ((map g n : (a : F.H n) → G.H n) x : G.H n)

Tactic:
simp [map, Ext.mk₀_add]

Premises used: CategoryTheory.Abelian.Ext.mk₀_add, CategoryTheory.Sheaf.H.map
-- Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasSheafify J AddCommGrpCat
inst_2 : HasExt (Sheaf J AddCommGrpCat)
F : Sheaf J AddCommGrpCat
h : Limits.IsZero F
n : ℕ
h₁ : Limits.IsZero ((functorH J n).obj F)
⊢ Subsingleton.{w' + 1} (↑((functorH J n).obj F) : Type w')

Tactic:
apply AddCommGrpCat.subsingleton_of_isZero

Premises used: AddCommGrpCat.subsingleton_of_isZero
-- Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasSheafify J AddCommGrpCat
inst_2 : HasExt (Sheaf J AddCommGrpCat)
F : Sheaf J AddCommGrpCat
h : Limits.IsZero F
n : ℕ
⊢ Limits.IsZero ((functorH J n).obj F)

Tactic:
Functor.map_isZero (functorH J n) h

Premises used: CategoryTheory.Sheaf.functorH, CategoryTheory.Functor.map_isZero
-- Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : HasSheafify J AddCommGrpCat
inst_2 : HasExt (Sheaf J AddCommGrpCat)
F : Sheaf J AddCommGrpCat
h : Limits.IsZero F
n : ℕ
⊢ Limits.IsZero ((functorH J n).obj F)

Tactic:
exact Functor.map_isZero (functorH J n) h

Premises used: CategoryTheory.Sheaf.functorH, CategoryTheory.Functor.map_isZero
-- 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 : ℕ
⊢ Eq.{w + 1} (α := F.H' n S.X₄ ⟶ F.H' n S.X₁) (S.toBiprod F n ≫ S.fromBiprod F n) 0

Tactic:
simp only [toBiprod, fromBiprod, biprod.lift_desc, Preadditive.comp_neg,
    ← sub_eq_add_neg, sub_eq_zero, ← Functor.map_comp, ← op_comp, S.toSquare.fac]

Premises used: CategoryTheory.op_comp, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod, sub_eq_zero, CategoryTheory.Preadditive.comp_neg, sub_eq_add_neg, CategoryTheory.Square.fac, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toSquare, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.biprod.lift_desc
-- 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 : ℕ
y₁ : (↑(F.H' n S.X₂) : Type w)
y₂ : (↑(F.H' n S.X₃) : Type w)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
          AddCommGrpCat.carrier)
          (Iso.inv ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)) ≫
            biprod.desc ((F.cohomologyPresheaf n).map S.f₁₂.op) (-(F.cohomologyPresheaf n).map S.f₁₃.op)) :
        (a : (↑(AddCommGrpCat.of ((↑(F.H' n S.X₂) : Type w) × (↑(F.H' n S.X₃) : Type w))) : Type w)) →
          (↑(F.H' n S.X₁) : Type w))
      (y₁, y₂) =
    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))
          y₁ :
        (↑((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))
          y₂ :
        (↑((F.cohomologyPresheaf n).obj (op S.X₁)) : Type w))

Tactic:
simp [AddCommGrpCat.biprodIsoProd_inv_comp_desc, sub_eq_add_neg]

Premises used: sub_eq_add_neg, AddCommGrpCat.biprodIsoProd_inv_comp_desc
-- 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₂ ⊞ F.H' n S.X₃) : Type w)
obtain : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
obtain ⟨⟨x₂, x₃⟩, rfl⟩ :=
    (AddCommGrpCat.biprodIsoProd _ _).addCommGroupIsoToAddEquiv.symm.surjective x

Premises used: AddCommGrpCat.biprodIsoProd, AddEquiv.surjective, CategoryTheory.Iso.addCommGroupIsoToAddEquiv, rfl, AddEquiv.symm
-- 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₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ 1 + n₀ = n₁

Tactic:
omega
-- 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₀ n₁ : ℕ
h : n₀ + 1 = n₁
hf :
  ∀ (x : (↑((S.sequence F n₀ n₁ h).obj ⟨0, ⋯⟩) : Type w)),
    Eq (α := (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 1 _proof_450✝) : Type w))
      ((AddCommGrpCat.Hom.hom
              ((S.sequence F n₀ n₁ h).map' 0 1 homMk₁._proof_4 _proof_450✝ ≫
                Iso.hom
                  ((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫
                    AddEquiv.toAddCommGrpIso (AddEquiv.symm Ext.biprodAddEquiv))) :
            (a : (↑((S.sequence F n₀ n₁ h).obj ⟨0, ⋯⟩) : Type w)) →
              (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 1 _proof_450✝) : Type w))
          x :
        (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 1 _proof_450✝) : Type w))
      ((AddCommGrpCat.Hom.hom
              (Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 0 _proof_449✝)) ≫
                (Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).map' 0 1 homMk₁._proof_4 _proof_450✝) :
            (a : (↑((S.sequence F n₀ n₁ h).obj ⟨0, ⋯⟩) : Type w)) →
              (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 1 _proof_450✝) : Type w))
          x :
        (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 1 _proof_450✝) : Type w))
⊢ (S.sequence F n₀ n₁ h).map' 0 1 homMk₁._proof_4 _proof_450✝ ≫
      Iso.hom
        ((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫ AddEquiv.toAddCommGrpIso (AddEquiv.symm Ext.biprodAddEquiv)) =
    Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 0 _proof_449✝)) ≫
      (Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).map' 0 1 homMk₁._proof_4 _proof_450✝

Tactic:
ext
-- 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₀ n₁ : ℕ
h : n₀ + 1 = n₁
x : (↑((S.sequence F n₀ n₁ h).obj ⟨0, ⋯⟩) : Type w)
⊢ Eq (α := (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 1 _proof_450✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            ((S.sequence F n₀ n₁ h).map' 0 1 homMk₁._proof_4 _proof_450✝ ≫
              Iso.hom
                ((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫
                  AddEquiv.toAddCommGrpIso (AddEquiv.symm Ext.biprodAddEquiv))) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨0, ⋯⟩) : Type w)) →
            (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 1 _proof_450✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 1 _proof_450✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            (Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 0 _proof_449✝)) ≫
              (Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).map' 0 1 homMk₁._proof_4 _proof_450✝) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨0, ⋯⟩) : Type w)) →
            (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 1 _proof_450✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 1 _proof_450✝) : Type w))

Tactic:
apply biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply

Premises used: CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply
-- 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₀ n₁ : ℕ
h : n₀ + 1 = n₁
hf :
  ∀ (x : (↑((S.sequence F n₀ n₁ h).obj ⟨1, ⋯⟩) : Type w)),
    Eq (α := (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))
      ((AddCommGrpCat.Hom.hom
              ((S.sequence F n₀ n₁ h).map' 1 2 _proof_246✝ _proof_451✝ ≫
                Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 2 _proof_451✝))) :
            (a : (↑((S.sequence F n₀ n₁ h).obj ⟨1, ⋯⟩) : Type w)) →
              (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))
          x :
        (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))
      ((AddCommGrpCat.Hom.hom
              (Iso.hom
                  ((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫
                    AddEquiv.toAddCommGrpIso (AddEquiv.symm Ext.biprodAddEquiv)) ≫
                (Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).map' 1 2 _proof_246✝ _proof_451✝) :
            (a : (↑((S.sequence F n₀ n₁ h).obj ⟨1, ⋯⟩) : Type w)) →
              (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))
          x :
        (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))
⊢ (S.sequence F n₀ n₁ h).map' 1 2 _proof_246✝ _proof_451✝ ≫
      Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 2 _proof_451✝)) =
    Iso.hom
        ((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫ AddEquiv.toAddCommGrpIso (AddEquiv.symm Ext.biprodAddEquiv)) ≫
      (Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).map' 1 2 _proof_246✝ _proof_451✝

Tactic:
ext
-- 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₀ n₁ : ℕ
h : n₀ + 1 = n₁
x : (↑((S.sequence F n₀ n₁ h).obj ⟨1, ⋯⟩) : Type w)
hf :
  Eq (α := (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            (Iso.hom
                ((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫
                  AddEquiv.toAddCommGrpIso (AddEquiv.symm Ext.biprodAddEquiv)) ≫
              (Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).map' 1 2 _proof_246✝ _proof_451✝) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨1, ⋯⟩) : Type w)) →
            (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            ((S.sequence F n₀ n₁ h).map' 1 2 _proof_246✝ _proof_451✝ ≫
              Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 2 _proof_451✝))) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨1, ⋯⟩) : Type w)) →
            (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))
⊢ Eq (α := (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            ((S.sequence F n₀ n₁ h).map' 1 2 _proof_246✝ _proof_451✝ ≫
              Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 2 _proof_451✝))) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨1, ⋯⟩) : Type w)) →
            (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            (Iso.hom
                ((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫
                  AddEquiv.toAddCommGrpIso (AddEquiv.symm Ext.biprodAddEquiv)) ≫
              (Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).map' 1 2 _proof_246✝ _proof_451✝) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨1, ⋯⟩) : Type w)) →
            (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))

Tactic:
symm
-- 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₀ n₁ : ℕ
h : n₀ + 1 = n₁
x : (↑((S.sequence F n₀ n₁ h).obj ⟨1, ⋯⟩) : Type w)
⊢ Eq (α := (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            (Iso.hom
                ((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫
                  AddEquiv.toAddCommGrpIso (AddEquiv.symm Ext.biprodAddEquiv)) ≫
              (Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).map' 1 2 _proof_246✝ _proof_451✝) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨1, ⋯⟩) : Type w)) →
            (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            ((S.sequence F n₀ n₁ h).map' 1 2 _proof_246✝ _proof_451✝ ≫
              Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 2 _proof_451✝))) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨1, ⋯⟩) : Type w)) →
            (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 2 _proof_451✝) : Type w))

Tactic:
apply mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom

Premises used: CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom
-- 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₀ n₁ : ℕ
h : n₀ + 1 = n₁
rw :
  Precomp.map
      (mk₄ (X₀ := F.H' n₀ S.X₂ ⊞ F.H' n₀ S.X₃) (S.fromBiprod F n₀) (S.δ F n₀ n₁ h) (S.toBiprod F n₁)
        (S.fromBiprod F n₁))
      (S.toBiprod F n₀) 2 3 ⋯ =
    (Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).map (homOfLE ⋯)
⊢ Precomp.map
        (mk₄ (X₀ := F.H' n₀ S.X₂ ⊞ F.H' n₀ S.X₃) (S.fromBiprod F n₀) (S.δ F n₀ n₁ h) (S.toBiprod F n₁)
          (S.fromBiprod F n₁))
        (S.toBiprod F n₀) 2 3 ⋯ ≫
      𝟙
        (Precomp.obj
          (mk₄ (X₀ := F.H' n₀ S.X₂ ⊞ F.H' n₀ S.X₃) (S.fromBiprod F n₀) (S.δ F n₀ n₁ h) (S.toBiprod F n₁)
            (S.fromBiprod F n₁))
          (F.H' n₀ S.X₄) 3) =
    𝟙
        (Precomp.obj
          (mk₄ (X₀ := F.H' n₀ S.X₂ ⊞ F.H' n₀ S.X₃) (S.fromBiprod F n₀) (S.δ F n₀ n₁ h) (S.toBiprod F n₁)
            (S.fromBiprod F n₁))
          (F.H' n₀ S.X₄) 2) ≫
      (Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).map (homOfLE ⋯)

Tactic:
rw [comp_id, id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- 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₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ Precomp.map
      (mk₄ (X₀ := F.H' n₀ S.X₂ ⊞ F.H' n₀ S.X₃) (S.fromBiprod F n₀) (S.δ F n₀ n₁ h) (S.toBiprod F n₁)
        (S.fromBiprod F n₁))
      (S.toBiprod F n₀) 2 3 ⋯ =
    (Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).map (homOfLE ⋯)

Tactic:
rfl
-- 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₀ n₁ : ℕ
h : n₀ + 1 = n₁
hf :
  ∀ (x : (↑((S.sequence F n₀ n₁ h).obj ⟨3, ⋯⟩) : Type w)),
    Eq (α := (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 4 _proof_453✝) : Type w))
      ((AddCommGrpCat.Hom.hom
              ((S.sequence F n₀ n₁ h).map' 3 4 _proof_364✝ _proof_453✝ ≫
                Iso.hom
                  ((F.H' n₁ S.X₂).biprodIsoProd (F.H' n₁ S.X₃) ≪≫
                    AddEquiv.toAddCommGrpIso (AddEquiv.symm Ext.biprodAddEquiv))) :
            (a : (↑((S.sequence F n₀ n₁ h).obj ⟨3, ⋯⟩) : Type w)) →
              (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 4 _proof_453✝) : Type w))
          x :
        (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 4 _proof_453✝) : Type w))
      ((AddCommGrpCat.Hom.hom
              (Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 3 _proof_452✝)) ≫
                (Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).map' 3 4 _proof_364✝ _proof_453✝) :
            (a : (↑((S.sequence F n₀ n₁ h).obj ⟨3, ⋯⟩) : Type w)) →
              (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 4 _proof_453✝) : Type w))
          x :
        (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 4 _proof_453✝) : Type w))
⊢ (S.sequence F n₀ n₁ h).map' 3 4 _proof_364✝ _proof_453✝ ≫
      Iso.hom
        ((F.H' n₁ S.X₂).biprodIsoProd (F.H' n₁ S.X₃) ≪≫ AddEquiv.toAddCommGrpIso (AddEquiv.symm Ext.biprodAddEquiv)) =
    Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 3 _proof_452✝)) ≫
      (Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).map' 3 4 _proof_364✝ _proof_453✝

Tactic:
ext
-- 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₀ n₁ : ℕ
h : n₀ + 1 = n₁
x : (↑((S.sequence F n₀ n₁ h).obj ⟨3, ⋯⟩) : Type w)
⊢ Eq (α := (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 4 _proof_453✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            ((S.sequence F n₀ n₁ h).map' 3 4 _proof_364✝ _proof_453✝ ≫
              Iso.hom
                ((F.H' n₁ S.X₂).biprodIsoProd (F.H' n₁ S.X₃) ≪≫
                  AddEquiv.toAddCommGrpIso (AddEquiv.symm Ext.biprodAddEquiv))) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨3, ⋯⟩) : Type w)) →
            (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 4 _proof_453✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 4 _proof_453✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            (Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 3 _proof_452✝)) ≫
              (Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).map' 3 4 _proof_364✝ _proof_453✝) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨3, ⋯⟩) : Type w)) →
            (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 4 _proof_453✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 4 _proof_453✝) : Type w))

Tactic:
apply biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply

Premises used: CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply