awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ⟨4, ⋯⟩) : Type w)),
    Eq (α := (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : Type w))
      ((AddCommGrpCat.Hom.hom
              ((S.sequence F n₀ n₁ h).map' 4 5 _proof_453✝ _proof_454✝ ≫
                Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 5 _proof_454✝))) :
            (a : (↑((S.sequence F n₀ n₁ h).obj ⟨4, ⋯⟩) : Type w)) →
              (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : Type w))
          x :
        (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : 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' 4 5 _proof_453✝ _proof_454✝) :
            (a : (↑((S.sequence F n₀ n₁ h).obj ⟨4, ⋯⟩) : Type w)) →
              (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : Type w))
          x :
        (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : Type w))
⊢ (S.sequence F n₀ n₁ h).map' 4 5 _proof_453✝ _proof_454✝ ≫
      Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 5 _proof_454✝)) =
    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' 4 5 _proof_453✝ _proof_454✝

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 ⟨4, ⋯⟩) : Type w)
hf :
  Eq (α := (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : 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' 4 5 _proof_453✝ _proof_454✝) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨4, ⋯⟩) : Type w)) →
            (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            ((S.sequence F n₀ n₁ h).map' 4 5 _proof_453✝ _proof_454✝ ≫
              Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 5 _proof_454✝))) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨4, ⋯⟩) : Type w)) →
            (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : Type w))
⊢ Eq (α := (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            ((S.sequence F n₀ n₁ h).map' 4 5 _proof_453✝ _proof_454✝ ≫
              Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 5 _proof_454✝))) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨4, ⋯⟩) : Type w)) →
            (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : 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' 4 5 _proof_453✝ _proof_454✝) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨4, ⋯⟩) : Type w)) →
            (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : 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 ⟨4, ⋯⟩) : Type w)
⊢ Eq (α := (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : 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' 4 5 _proof_453✝ _proof_454✝) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨4, ⋯⟩) : Type w)) →
            (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : Type w))
    ((AddCommGrpCat.Hom.hom
            ((S.sequence F n₀ n₁ h).map' 4 5 _proof_453✝ _proof_454✝ ≫
              Iso.hom (Iso.refl ((S.sequence F n₀ n₁ h).obj' 5 _proof_454✝))) :
          (a : (↑((S.sequence F n₀ n₁ h).obj ⟨4, ⋯⟩) : Type w)) →
            (↑((Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : Type w))
        x :
      (↑((Ext.contravariantSequence (S := S.shortComplex) ⋯ F n₀ n₁ ⋯).obj' 5 _proof_454✝) : 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₁
⊢ (S.sequence F n₀ n₁ h).Exact

Tactic:
exact_of_iso (S.sequenceIso F n₀ n₁ h).symm (Ext.contravariantSequence_exact _ _ _ _ _)

Premises used: CategoryTheory.ComposableArrows.exact_of_iso, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sequenceIso, CategoryTheory.Iso.symm, CategoryTheory.Abelian.Ext.contravariantSequence_exact
-- 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₁
⊢ Eq.{w + 1} (α := F.H' n₀ S.X₁ ⟶ F.H' n₁ S.X₂ ⊞ F.H' n₁ S.X₃) (S.δ F n₀ n₁ h ≫ S.toBiprod F n₁) 0

Tactic:
(S.sequence_exact F n₀ n₁ h).zero 2

Premises used: CategoryTheory.ComposableArrows.Mk₁.obj, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sequence_exact, CategoryTheory.ComposableArrows.Exact.toIsComplex, CategoryTheory.ComposableArrows.Precomp.obj, OfNat.ofNat, CategoryTheory.ComposableArrows.IsComplex.zero
-- 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₁
⊢ Eq.{w + 1} (α := F.H' n₀ S.X₂ ⊞ F.H' n₀ S.X₃ ⟶ F.H' n₁ S.X₄) (S.fromBiprod F n₀ ≫ S.δ F n₀ n₁ h) 0

Tactic:
(S.sequence_exact F n₀ n₁ h).zero 1

Premises used: CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sequence_exact, CategoryTheory.ComposableArrows.Exact.toIsComplex, CategoryTheory.ComposableArrows.Precomp.obj, OfNat.ofNat, CategoryTheory.ComposableArrows.IsComplex.zero
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
h :
  ∀ (φ : Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G)
    (Y : Over.{v, u} (unop (op X))),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op Y) ⟶ (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op Y))
      (NatTrans.app
          (TypeCat.Fun.toFun
            (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (↾Functor.whiskerLeft (Functor.op (Over.map (Quiver.Hom.unop (𝟙 (op X)))))))
            φ)
          (op Y) :
        (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op Y) ⟶
          (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op Y))
      (((ConcreteCategory.hom (FC := TypeCat.Fun)
                (𝟙 (Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G))).toFun
            φ).app
        (op Y))
⊢ Eq (α :=
    (Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G) ⟶
      Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G)
    (↾Functor.whiskerLeft (Functor.op (Over.map (Quiver.Hom.unop (𝟙 (op X))))) :
      (Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G) ⟶
        Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G)
    (𝟙 (Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G) :
      (Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G) ⟶
        Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G)

Tactic:
ext φ ⟨Y⟩
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
φ : Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G
Y : Over.{v, u} (unop (op X))
⊢ Eq (α :=
    (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op Y) ⟶ (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op Y))
    (NatTrans.app
        (TypeCat.Fun.toFun
          (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (↾Functor.whiskerLeft (Functor.op (Over.map (Quiver.Hom.unop (𝟙 (op X)))))))
          φ)
        (op Y) :
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op Y) ⟶ (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op Y))
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
              (𝟙 (Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G))).toFun
          φ).app
      (op Y))

Tactic:
simpa [Over.mapId] using φ.naturality ((Over.mapId X).hom.app Y).op

Premises used: Quiver.Hom.op, CategoryTheory.NatTrans.naturality, CategoryTheory.Over.mapId, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
h :
  ∀ (φ : Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G)
    (W : Over.{v, u} (unop (op Z))),
    Eq (α :=
      (Functor.op (Over.forget (unop (op Z))) ⋙ F).obj (op W) ⟶ (Functor.op (Over.forget (unop (op Z))) ⋙ G).obj (op W))
      (NatTrans.app
          (TypeCat.Fun.toFun
            (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (↾Functor.whiskerLeft (Functor.op (Over.map (Quiver.Hom.unop (op f ≫ op g))))))
            φ)
          (op W) :
        (Functor.op (Over.forget (unop (op Z))) ⋙ F).obj (op W) ⟶
          (Functor.op (Over.forget (unop (op Z))) ⋙ G).obj (op W))
      ((TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾(Over.map (Quiver.Hom.unop (op f))).op.whiskerLeft ≫
                ↾(Over.map (Quiver.Hom.unop (op g))).op.whiskerLeft))
            φ).app
        (op W))
⊢ Eq (α :=
    (Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G) ⟶
      Functor.op (Over.forget (unop (op Z))) ⋙ F ⟶ Functor.op (Over.forget (unop (op Z))) ⋙ G)
    (↾Functor.whiskerLeft (Functor.op (Over.map (Quiver.Hom.unop (op f ≫ op g)))) :
      (Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G) ⟶
        Functor.op (Over.forget (unop (op Z))) ⋙ F ⟶ Functor.op (Over.forget (unop (op Z))) ⋙ G)
    (↾(Over.map (Quiver.Hom.unop (op f))).op.whiskerLeft ≫ ↾(Over.map (Quiver.Hom.unop (op g))).op.whiskerLeft :
      (Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G) ⟶
        Functor.op (Over.forget (unop (op Z))) ⋙ F ⟶ Functor.op (Over.forget (unop (op Z))) ⋙ G)

Tactic:
ext φ ⟨W⟩
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
φ : Functor.op (Over.forget (unop (op X))) ⋙ F ⟶ Functor.op (Over.forget (unop (op X))) ⋙ G
W : Over.{v, u} (unop (op Z))
⊢ Eq (α :=
    (Functor.op (Over.forget (unop (op Z))) ⋙ F).obj (op W) ⟶ (Functor.op (Over.forget (unop (op Z))) ⋙ G).obj (op W))
    (NatTrans.app
        (TypeCat.Fun.toFun
          (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (↾Functor.whiskerLeft (Functor.op (Over.map (Quiver.Hom.unop (op f ≫ op g))))))
          φ)
        (op W) :
      (Functor.op (Over.forget (unop (op Z))) ⋙ F).obj (op W) ⟶ (Functor.op (Over.forget (unop (op Z))) ⋙ G).obj (op W))
    ((TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾(Over.map (Quiver.Hom.unop (op f))).op.whiskerLeft ≫ ↾(Over.map (Quiver.Hom.unop (op g))).op.whiskerLeft))
          φ).app
      (op W))

Tactic:
simpa [Over.mapComp] using φ.naturality ((Over.mapComp g f).hom.app W).op

Premises used: CategoryTheory.Over.mapComp, Quiver.Hom.op, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X Y Z : C
f : Z ⟶ Y
g : Y ⟶ X
h : Z ⟶ X
w : f ≫ g = h
α : (presheafHom F G).obj (op X)
subst :
  Eq.{v' + 1} (α :=
    (Functor.op (Over.forget (unop (op Y))) ⋙ F).obj (op (Over.mk f)) ⟶
      (Functor.op (Over.forget (unop (op Y))) ⋙ G).obj (op (Over.mk f)))
    (NatTrans.app
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map g.op) :
          (a : (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op X))) →
            (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Y)))
        α)
      (op (Over.mk f)))
    (α.app (op (Over.mk (f ≫ g))))
⊢ Eq.{v' + 1} (α :=
    (Functor.op (Over.forget (unop (op Y))) ⋙ F).obj (op (Over.mk f)) ⟶
      (Functor.op (Over.forget (unop (op Y))) ⋙ G).obj (op (Over.mk f)))
    (NatTrans.app
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map g.op) :
          (a : (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op X))) →
            (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Y)))
        α)
      (op (Over.mk f)))
    (α.app (op (Over.mk h)))

Tactic:
subst w
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X Y Z : C
f : Z ⟶ Y
g : Y ⟶ X
α : (presheafHom F G).obj (op X)
⊢ Eq.{v' + 1} (α :=
    (Functor.op (Over.forget (unop (op Y))) ⋙ F).obj (op (Over.mk f)) ⟶
      (Functor.op (Over.forget (unop (op Y))) ⋙ G).obj (op (Over.mk f)))
    (NatTrans.app
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map g.op) :
          (a : (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op X))) →
            (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Y)))
        α)
      (op (Over.mk f)))
    (α.app (op (Over.mk (f ≫ g))))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X Y : C
g : Y ⟶ X
α : (presheafHom F G).obj (op X)
⊢ 𝟙 Y ≫ g = g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
s : (↑(presheafHom F G).sections : Type (max (max u v) v'))
X₁ X₂ : C
f : X₂ ⟶ X₁
dsimp :
  Eq (α := F.obj (op X₁) ⟶ G.obj (op X₂))
    (F.map (op f) ≫
      ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₂)).app
        (op (Over.mk (𝟙 X₂))))
    (((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₁)).app
        (op (Over.mk (𝟙 X₁))) ≫
      G.map (op f))
⊢ Eq (α := F.obj (op X₁) ⟶ G.obj (op X₂))
    (F.map (op f) ≫ ((↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op X₂)).app (op (Over.mk (𝟙 (unop (op X₂))))))
    (((↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op X₁)).app (op (Over.mk (𝟙 (unop (op X₁))))) ≫ G.map (op f))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
s : (↑(presheafHom F G).sections : Type (max (max u v) v'))
X₁ X₂ : C
f : X₂ ⟶ X₁
⊢ Eq (α := F.obj (op X₁) ⟶ G.obj (op X₂))
    (F.map (op f) ≫
      ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₂)).app
        (op (Over.mk (𝟙 X₂))))
    (((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₁)).app
        (op (Over.mk (𝟙 X₁))) ≫
      G.map (op f))

Tactic:
Eq.trans ?_ ((s.1 ⟨X₁⟩).naturality
          (Over.homMk f : Over.mk f ⟶ Over.mk (𝟙 X₁)).op)

Premises used: Quiver.Hom.op, CategoryTheory.Over.homMk, Opposite.op, CategoryTheory.NatTrans.naturality, Subtype.val, Eq.trans
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
s : (↑(presheafHom F G).sections : Type (max (max u v) v'))
X₁ X₂ : C
f : X₂ ⟶ X₁
refine :
  Eq (α := F.obj (op X₁) ⟶ G.obj (op X₂))
    (F.map (op f) ≫
      ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₂)).app
        (op (Over.mk (𝟙 X₂))))
    ((Functor.op (Over.forget (unop (op X₁))) ⋙ F).map (Quiver.Hom.op (Over.homMk f ⋯)) ≫
      ((↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op X₁)).app (op (Over.mk f)))
⊢ Eq (α := F.obj (op X₁) ⟶ G.obj (op X₂))
    (F.map (op f) ≫
      ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₂)).app
        (op (Over.mk (𝟙 X₂))))
    (((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₁)).app
        (op (Over.mk (𝟙 X₁))) ≫
      G.map (op f))

Tactic:
refine Eq.trans ?_ ((s.1 ⟨X₁⟩).naturality
          (Over.homMk f : Over.mk f ⟶ Over.mk (𝟙 X₁)).op)

Premises used: Quiver.Hom.op, CategoryTheory.Over.homMk, Opposite.op, CategoryTheory.NatTrans.naturality, Subtype.val, Eq.trans
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
s : (↑(presheafHom F G).sections : Type (max (max u v) v'))
X₁ X₂ : C
f : X₂ ⟶ X₁
rw :
  Eq (α := F.obj (op X₁) ⟶ G.obj (op X₂))
    (F.map (op f) ≫
      NatTrans.app
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map f.op) :
            (a : (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op X₁))) →
              (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op X₂)))
          ((↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op X₁)))
        (op (Over.mk (𝟙 X₂))))
    ((Functor.op (Over.forget (unop (op X₁))) ⋙ F).map (Quiver.Hom.op (Over.homMk f ⋯)) ≫
      ((↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op X₁)).app (op (Over.mk f)))
⊢ Eq (α := F.obj (op X₁) ⟶ G.obj (op X₂))
    (F.map (op f) ≫
      ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₂)).app
        (op (Over.mk (𝟙 X₂))))
    ((Functor.op (Over.forget (unop (op X₁))) ⋙ F).map (Quiver.Hom.op (Over.homMk f ⋯)) ≫
      ((↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op X₁)).app (op (Over.mk f)))

Tactic:
rw [← s.2 f.op]

Premises used: Quiver.Hom.op, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
s : (↑(presheafHom F G).sections : Type (max (max u v) v'))
X₁ X₂ : C
f : X₂ ⟶ X₁
dsimp :
  Eq (α := F.obj (op X₁) ⟶ G.obj (op X₂))
    (F.map (op f) ≫
      NatTrans.app
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map f.op) :
            (a : (Over.forget X₁).op ⋙ F ⟶ (Over.forget X₁).op ⋙ G) → (Over.forget X₂).op ⋙ F ⟶ (Over.forget X₂).op ⋙ G)
          ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₁)))
        (op (Over.mk (𝟙 X₂))))
    (F.map f.op ≫
      ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₁)).app (op (Over.mk f)))
⊢ Eq (α := F.obj (op X₁) ⟶ G.obj (op X₂))
    (F.map (op f) ≫
      NatTrans.app
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map f.op) :
            (a : (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op X₁))) →
              (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op X₂)))
          ((↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op X₁)))
        (op (Over.mk (𝟙 X₂))))
    ((Functor.op (Over.forget (unop (op X₁))) ⋙ F).map (Quiver.Hom.op (Over.homMk f ⋯)) ≫
      ((↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op X₁)).app (op (Over.mk f)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
s : (↑(presheafHom F G).sections : Type (max (max u v) v'))
X₁ X₂ : C
f : X₂ ⟶ X₁
rw :
  Eq (α := F.obj (op X₁) ⟶ G.obj (op X₂))
    (F.map (op f) ≫
      ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₁)).app (op (Over.mk f)))
    (F.map f.op ≫
      ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₁)).app (op (Over.mk f)))
⊢ Eq (α := F.obj (op X₁) ⟶ G.obj (op X₂))
    (F.map (op f) ≫
      NatTrans.app
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map f.op) :
            (a : (Over.forget X₁).op ⋙ F ⟶ (Over.forget X₁).op ⋙ G) → (Over.forget X₂).op ⋙ F ⟶ (Over.forget X₂).op ⋙ G)
          ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₁)))
        (op (Over.mk (𝟙 X₂))))
    (F.map f.op ≫
      ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₁)).app (op (Over.mk f)))

Tactic:
rw [presheafHom_map_app_op_mk_id]

Premises used: CategoryTheory.presheafHom_map_app_op_mk_id