mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Subobject.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasPullbacks C
x✝¹ : Cᵒᵖ
x✝ : Subobject (Opposite.unop x✝¹)
⊢ (ConcreteCategory.hom (↾(pullback (𝟙 x✝¹).unop).obj)).toFun x✝ =
    (ConcreteCategory.hom (𝟙 (Subobject (Opposite.unop x✝¹)))).toFun x✝

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasPullbacks C
x✝¹ : Cᵒᵖ
x✝ : Subobject (Opposite.unop x✝¹)
⊢ (ConcreteCategory.hom (↾(pullback (𝟙 x✝¹).unop).obj)).toFun x✝ =
    (ConcreteCategory.hom (𝟙 (Subobject (Opposite.unop x✝¹)))).toFun x✝
Module: Mathlib.CategoryTheory.Subobject.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasPullbacks C
X✝ Y✝ Z✝ : Cᵒᵖ
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : Subobject (Opposite.unop X✝)
⊢ (ConcreteCategory.hom (↾(pullback (x✝² ≫ x✝¹).unop).obj)).toFun x✝ =
    (ConcreteCategory.hom (↾(pullback x✝².unop).obj ≫ ↾(pullback x✝¹.unop).obj)).toFun x✝

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasPullbacks C
X✝ Y✝ Z✝ : Cᵒᵖ
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : Subobject (Opposite.unop X✝)
⊢ (ConcreteCategory.hom (↾(pullback (x✝² ≫ x✝¹).unop).obj)).toFun x✝ =
    (ConcreteCategory.hom (↾(pullback x✝².unop).obj ≫ ↾(pullback x✝¹.unop).obj)).toFun x✝
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
M N : ↑(F.obj { as := op S })
X : C
g : X ⟶ S
f : Over.mk g ⟶ Over.mk (𝟙 S)
hf : R.arrows (Over.Hom.left f)
⊢ Over.Hom.left f = Over.Hom.left (Over.homMk g ⋯)

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
M N : ↑(F.obj { as := op S })
X : C
g : X ⟶ S
f : Over.mk g ⟶ Over.mk (𝟙 S)
hf : R.arrows (Over.Hom.left f)
⊢ Over.Hom.left f = Over.Hom.left (Over.homMk g ⋯)
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
U X : C
m : U ⟶ X
inst✝ : Mono m
χ' : X ⟶ Ω
π : U ⟶ underlying.obj h.Ω₀
sq : IsPullback m π χ' h.Ω₀.arrow
⊢ (Subobject.pullback χ').obj h.Ω₀ = Subobject.mk m

Tactic:
simpa using! Subobject.pullback_obj_mk sq.flip

Goal state after:
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
X : Cᵒᵖ
⊢ m.app X ≫ (χ m).app X = ((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X ≫ (truth C).app X ∧
    (∀ (x₁ y₁ : (fun X ↦ X) (F.obj X)),
        (ConcreteCategory.hom (m.app X)) x₁ = (ConcreteCategory.hom (m.app X)) y₁ ∧
            (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) x₁ =
              (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) y₁ →
          x₁ = y₁) ∧
      ∀ (x₂ : (fun X ↦ X) (G.obj X)) (x₃ : (fun X ↦ X) (((Functor.const Cᵒᵖ).obj PUnit.{(max u v) + 1}).obj X)),
        (ConcreteCategory.hom ((χ m).app X)) x₂ = (ConcreteCategory.hom ((truth C).app X)) x₃ →
          ∃ x₁,
            (ConcreteCategory.hom (m.app X)) x₁ = x₂ ∧
              (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) x₁ = x₃

Tactic:
refine ⟨congr(($(comp_χ_eq m)).app X), ?_, ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
X : Cᵒᵖ
⊢ ∀ (x₁ y₁ : (fun X ↦ X) (F.obj X)),
    (ConcreteCategory.hom (m.app X)) x₁ = (ConcreteCategory.hom (m.app X)) y₁ ∧
        (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) x₁ =
          (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) y₁ →
      x₁ = y₁

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
X : Cᵒᵖ
⊢ ∀ (x₂ : (fun X ↦ X) (G.obj X)) (x₃ : (fun X ↦ X) (((Functor.const Cᵒᵖ).obj PUnit.{(max u v) + 1}).obj X)),
    (ConcreteCategory.hom ((χ m).app X)) x₂ = (ConcreteCategory.hom ((truth C).app X)) x₃ →
      ∃ x₁,
        (ConcreteCategory.hom (m.app X)) x₁ = x₂ ∧
          (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) x₁ = x₃
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasPullbacks C
Ω : C
h : (Subobject.presheaf C).RepresentableBy Ω
⊢ Nonempty (Subobject.Classifier C)

Tactic:
;

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasPullbacks C
Ω : C
h : (Subobject.presheaf C).RepresentableBy Ω
⊢ Nonempty (Subobject.Classifier C)
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : 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, ⋯⟩)
⊢ (AddCommGrpCat.Hom.hom
        ((S.sequence F n₀ n₁ h).map' 0 1 homMk₁._proof_4 _proof_450✝ ≫
          ((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫ Ext.biprodAddEquiv.symm.toAddCommGrpIso).hom))
      x✝ =
    (AddCommGrpCat.Hom.hom
        ((Iso.refl ((S.sequence F n₀ n₁ h).obj' 0 _proof_449✝)).hom ≫
          (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map' 0 1 homMk₁._proof_4 _proof_450✝))
      x✝

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : 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, ⋯⟩)
⊢ (AddCommGrpCat.Hom.hom
        ((S.sequence F n₀ n₁ h).map' 0 1 homMk₁._proof_4 _proof_450✝ ≫
          ((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫ Ext.biprodAddEquiv.symm.toAddCommGrpIso).hom))
      x✝ =
    (AddCommGrpCat.Hom.hom
        ((Iso.refl ((S.sequence F n₀ n₁ h).obj' 0 _proof_449✝)).hom ≫
          (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map' 0 1 homMk₁._proof_4 _proof_450✝))
      x✝
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : 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, ⋯⟩)
⊢ (AddCommGrpCat.Hom.hom
        ((S.sequence F n₀ n₁ h).map' 1 2 _proof_246✝ _proof_451✝ ≫
          (Iso.refl ((S.sequence F n₀ n₁ h).obj' 2 _proof_451✝)).hom))
      x✝ =
    (AddCommGrpCat.Hom.hom
        (((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫ Ext.biprodAddEquiv.symm.toAddCommGrpIso).hom ≫
          (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map' 1 2 _proof_246✝ _proof_451✝))
      x✝

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : 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, ⋯⟩)
⊢ (AddCommGrpCat.Hom.hom
        ((S.sequence F n₀ n₁ h).map' 1 2 _proof_246✝ _proof_451✝ ≫
          (Iso.refl ((S.sequence F n₀ n₁ h).obj' 2 _proof_451✝)).hom))
      x✝ =
    (AddCommGrpCat.Hom.hom
        (((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫ Ext.biprodAddEquiv.symm.toAddCommGrpIso).hom ≫
          (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map' 1 2 _proof_246✝ _proof_451✝))
      x✝
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : 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, ⋯⟩)
⊢ (AddCommGrpCat.Hom.hom
        (((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫ Ext.biprodAddEquiv.symm.toAddCommGrpIso).hom ≫
          (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map' 1 2 _proof_246✝ _proof_451✝))
      x✝ =
    (AddCommGrpCat.Hom.hom
        ((S.sequence F n₀ n₁ h).map' 1 2 _proof_246✝ _proof_451✝ ≫
          (Iso.refl ((S.sequence F n₀ n₁ h).obj' 2 _proof_451✝)).hom))
      x✝

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : 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, ⋯⟩)
⊢ (AddCommGrpCat.Hom.hom
        (((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫ Ext.biprodAddEquiv.symm.toAddCommGrpIso).hom ≫
          (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map' 1 2 _proof_246✝ _proof_451✝))
      x✝ =
    (AddCommGrpCat.Hom.hom
        ((S.sequence F n₀ n₁ h).map' 1 2 _proof_246✝ _proof_451✝ ≫
          (Iso.refl ((S.sequence F n₀ n₁ h).obj' 2 _proof_451✝)).hom))
      x✝
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ Precomp.map (mk₄ (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₄ (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₄ (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 ⋯ F n₀ n₁ ⋯).map (homOfLE ⋯)

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ Precomp.map (mk₄ (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₄ (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₄ (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 ⋯ F n₀ n₁ ⋯).map (homOfLE ⋯)
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ Precomp.map (mk₄ (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 ⋯ F n₀ n₁ ⋯).map (homOfLE ⋯)

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ Precomp.map (mk₄ (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 ⋯ F n₀ n₁ ⋯).map (homOfLE ⋯)
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : 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, ⋯⟩)
⊢ (AddCommGrpCat.Hom.hom
        ((S.sequence F n₀ n₁ h).map' 3 4 _proof_364✝ _proof_453✝ ≫
          ((F.H' n₁ S.X₂).biprodIsoProd (F.H' n₁ S.X₃) ≪≫ Ext.biprodAddEquiv.symm.toAddCommGrpIso).hom))
      x✝ =
    (AddCommGrpCat.Hom.hom
        ((Iso.refl ((S.sequence F n₀ n₁ h).obj' 3 _proof_452✝)).hom ≫
          (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map' 3 4 _proof_364✝ _proof_453✝))
      x✝

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : 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, ⋯⟩)
⊢ (AddCommGrpCat.Hom.hom
        ((S.sequence F n₀ n₁ h).map' 3 4 _proof_364✝ _proof_453✝ ≫
          ((F.H' n₁ S.X₂).biprodIsoProd (F.H' n₁ S.X₃) ≪≫ Ext.biprodAddEquiv.symm.toAddCommGrpIso).hom))
      x✝ =
    (AddCommGrpCat.Hom.hom
        ((Iso.refl ((S.sequence F n₀ n₁ h).obj' 3 _proof_452✝)).hom ≫
          (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map' 3 4 _proof_364✝ _proof_453✝))
      x✝
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : 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 ⟨4, ⋯⟩)
⊢ (AddCommGrpCat.Hom.hom
        ((S.sequence F n₀ n₁ h).map' 4 5 _proof_453✝ _proof_454✝ ≫
          (Iso.refl ((S.sequence F n₀ n₁ h).obj' 5 _proof_454✝)).hom))
      x✝ =
    (AddCommGrpCat.Hom.hom
        (((F.H' n₁ S.X₂).biprodIsoProd (F.H' n₁ S.X₃) ≪≫ Ext.biprodAddEquiv.symm.toAddCommGrpIso).hom ≫
          (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map' 4 5 _proof_453✝ _proof_454✝))
      x✝

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : 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 ⟨4, ⋯⟩)
⊢ (AddCommGrpCat.Hom.hom
        ((S.sequence F n₀ n₁ h).map' 4 5 _proof_453✝ _proof_454✝ ≫
          (Iso.refl ((S.sequence F n₀ n₁ h).obj' 5 _proof_454✝)).hom))
      x✝ =
    (AddCommGrpCat.Hom.hom
        (((F.H' n₁ S.X₂).biprodIsoProd (F.H' n₁ S.X₃) ≪≫ Ext.biprodAddEquiv.symm.toAddCommGrpIso).hom ≫
          (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map' 4 5 _proof_453✝ _proof_454✝))
      x✝
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : 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 ⟨4, ⋯⟩)
⊢ (AddCommGrpCat.Hom.hom
        (((F.H' n₁ S.X₂).biprodIsoProd (F.H' n₁ S.X₃) ≪≫ Ext.biprodAddEquiv.symm.toAddCommGrpIso).hom ≫
          (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map' 4 5 _proof_453✝ _proof_454✝))
      x✝ =
    (AddCommGrpCat.Hom.hom
        ((S.sequence F n₀ n₁ h).map' 4 5 _proof_453✝ _proof_454✝ ≫
          (Iso.refl ((S.sequence F n₀ n₁ h).obj' 5 _proof_454✝)).hom))
      x✝

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : 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 ⟨4, ⋯⟩)
⊢ (AddCommGrpCat.Hom.hom
        (((F.H' n₁ S.X₂).biprodIsoProd (F.H' n₁ S.X₃) ≪≫ Ext.biprodAddEquiv.symm.toAddCommGrpIso).hom ≫
          (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map' 4 5 _proof_453✝ _proof_454✝))
      x✝ =
    (AddCommGrpCat.Hom.hom
        ((S.sequence F n₀ n₁ h).map' 4 5 _proof_453✝ _proof_454✝ ≫
          (Iso.refl ((S.sequence F n₀ n₁ h).obj' 5 _proof_454✝)).hom))
      x✝
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
a✝ b✝ : ℤ
⊢ -(a✝ + b✝) = -a✝ + -b✝

Tactic:
;

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
a✝ b✝ : ℤ
⊢ -(a✝ + b✝) = -a✝ + -b✝
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasShift C ℤ
inst✝³ : HasShift D ℤ
F : C ⥤ D
inst✝² : F.CommShift ℤ
G : C ⥤ D
inst✝¹ : G.CommShift ℤ
τ : F ⟶ G
inst✝ : NatTrans.CommShift τ ℤ
a✝ b✝ : ℤ
⊢ -(a✝ + b✝) = -a✝ + -b✝

Tactic:
;

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasShift C ℤ
inst✝³ : HasShift D ℤ
F : C ⥤ D
inst✝² : F.CommShift ℤ
G : C ⥤ D
inst✝¹ : G.CommShift ℤ
τ : F ⟶ G
inst✝ : NatTrans.CommShift τ ℤ
a✝ b✝ : ℤ
⊢ -(a✝ + b✝) = -a✝ + -b✝
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasShift C ℤ
inst✝³ : HasShift D ℤ
F : C ⥤ D
inst✝² : F.CommShift ℤ
G : D ⥤ C
inst✝¹ : G.CommShift ℤ
adj : F ⊣ G
inst✝ : adj.CommShift ℤ
a✝ b✝ : ℤ
⊢ -(a✝ + b✝) = -a✝ + -b✝

Tactic:
;

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasShift C ℤ
inst✝³ : HasShift D ℤ
F : C ⥤ D
inst✝² : F.CommShift ℤ
G : D ⥤ C
inst✝¹ : G.CommShift ℤ
adj : F ⊣ G
inst✝ : adj.CommShift ℤ
a✝ b✝ : ℤ
⊢ -(a✝ + b✝) = -a✝ + -b✝
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasShift C ℤ
inst✝³ : HasShift D ℤ
F : C ⥤ D
inst✝² : F.CommShift ℤ
G : D ⥤ C
inst✝¹ : G.CommShift ℤ
adj : F ⊣ G
inst✝ : adj.CommShift ℤ
eq : adj.op = PullbackShift.adjunction (AddMonoidHom.mk' (fun n ↦ -n) ⋯) (OppositeShift.adjunction ℤ adj)
a✝ b✝ : ℤ
⊢ -(a✝ + b✝) = -a✝ + -b✝

Tactic:
;

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasShift C ℤ
inst✝³ : HasShift D ℤ
F : C ⥤ D
inst✝² : F.CommShift ℤ
G : D ⥤ C
inst✝¹ : G.CommShift ℤ
adj : F ⊣ G
inst✝ : adj.CommShift ℤ
eq : adj.op = PullbackShift.adjunction (AddMonoidHom.mk' (fun n ↦ -n) ⋯) (OppositeShift.adjunction ℤ adj)
a✝ b✝ : ℤ
⊢ -(a✝ + b✝) = -a✝ + -b✝
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n m : ℤ
h : n + m = 0
⊢ (commShiftIso F.op n).hom.app X =
    (F.map ((shiftFunctorOpIso C n m h).hom.app X).unop).op ≫
      ((commShiftIso F m).inv.app (unop X)).op ≫ (shiftFunctorOpIso D n m h).inv.app (op (F.obj (unop X)))

Tactic:
obtain rfl : m = -n := by lia

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
h : n + -n = 0
⊢ (commShiftIso F.op n).hom.app X =
    (F.map ((shiftFunctorOpIso C n (-n) h).hom.app X).unop).op ≫
      ((commShiftIso F (-n)).inv.app (unop X)).op ≫ (shiftFunctorOpIso D n (-n) h).inv.app (op (F.obj (unop X)))
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : HasShift D ℤ
F : C ⥤ D
inst✝⁸ : F.CommShift ℤ
inst✝⁷ : HasZeroObject C
inst✝⁶ : Preadditive C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasZeroObject D
inst✝² : Preadditive D
inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝ : Pretriangulated D
X✝ Y✝ : (Triangle C)ᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ (F.mapTriangle.op ⋙ (triangleOpEquivalence D).functor).map f✝ ≫
      (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop Y✝)).hom =
    (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop X✝)).hom ≫
      ((triangleOpEquivalence C).functor ⋙ F.op.mapTriangle).map f✝

Tactic:
;

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : HasShift D ℤ
F : C ⥤ D
inst✝⁸ : F.CommShift ℤ
inst✝⁷ : HasZeroObject C
inst✝⁶ : Preadditive C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasZeroObject D
inst✝² : Preadditive D
inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝ : Pretriangulated D
X✝ Y✝ : (Triangle C)ᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ (F.mapTriangle.op ⋙ (triangleOpEquivalence D).functor).map f✝ ≫
      (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop Y✝)).hom =
    (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop X✝)).hom ≫
      ((triangleOpEquivalence C).functor ⋙ F.op.mapTriangle).map f✝
Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : C
n m : ℤ
hnm : n + m = 0
⊢ (iso C n).hom.app X =
    ((shiftFunctorOpIso C m n ⋯).hom.app (op X)).op ≫ (shiftFunctorOpIso Cᵒᵖ n m hnm).inv.app (op (op X))

Tactic:
obtain rfl : m = -n := by lia

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : C
n : ℤ
hnm : n + -n = 0
⊢ (iso C n).hom.app X =
    ((shiftFunctorOpIso C (-n) n ⋯).hom.app (op X)).op ≫ (shiftFunctorOpIso Cᵒᵖ n (-n) hnm).inv.app (op (op X))
Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : C
n m : ℤ
hnm : n + m = 0
⊢ (iso C n).inv.app X =
    (shiftFunctorOpIso Cᵒᵖ n m hnm).hom.app (op (op X)) ≫ ((shiftFunctorOpIso C m n ⋯).inv.app (op X)).op

Tactic:
obtain rfl : m = -n := by lia

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : C
n : ℤ
hnm : n + -n = 0
⊢ (iso C n).inv.app X =
    (shiftFunctorOpIso Cᵒᵖ n (-n) hnm).hom.app (op (op X)) ≫ ((shiftFunctorOpIso C (-n) n ⋯).inv.app (op X)).op
Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖᵒᵖ
n m : ℤ
hnm : n + m = 0
⊢ (iso C n).hom.app X =
    ((shiftFunctorOpIso Cᵒᵖ n m hnm).hom.app X).unop.unop ≫ ((shiftFunctorOpIso C m n ⋯).inv.app (unop X)).unop

Tactic:
obtain rfl : m = -n := by lia

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖᵒᵖ
n : ℤ
hnm : n + -n = 0
⊢ (iso C n).hom.app X =
    ((shiftFunctorOpIso Cᵒᵖ n (-n) hnm).hom.app X).unop.unop ≫ ((shiftFunctorOpIso C (-n) n ⋯).inv.app (unop X)).unop
Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖᵒᵖ
n m : ℤ
hnm : n + m = 0
⊢ (iso C n).inv.app X =
    ((shiftFunctorOpIso C m n ⋯).hom.app (unop X)).unop ≫ ((shiftFunctorOpIso Cᵒᵖ n m hnm).inv.app X).unop.unop

Tactic:
obtain rfl : m = -n := by lia

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖᵒᵖ
n : ℤ
hnm : n + -n = 0
⊢ (iso C n).inv.app X =
    ((shiftFunctorOpIso C (-n) n ⋯).hom.app (unop X)).unop ≫ ((shiftFunctorOpIso Cᵒᵖ n (-n) hnm).inv.app X).unop.unop