-- 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_1 G_1 : Functor.{v, v', u, u'} Cᵒᵖ A
F G : Sheaf.{v, v', u, u'} J A
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
h :
  ∀
    (φ :
      Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop X)) (J.over (unop X)) A)
        (Functor.obj (J.overPullback A (unop X)) F) (Functor.obj (J.overPullback A (unop X)) G)),
    Eq (α :=
      Quiver.Hom (V := (Over.{v, u} (unop Z))ᵒᵖ ⥤ A)
        (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (J.over (unop Z)))
          (Functor.obj (J.overPullback A (unop Z)) F))
        (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (J.over (unop Z)))
          (Functor.obj (J.overPullback A (unop Z)) G)))
      (InducedCategory.Hom.hom
          (TypeCat.Fun.toFun
            (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (↾Functor.map (J.overMapPullback A (f ≫ g).unop))) φ) :
        Quiver.Hom (V := (Over.{v, u} (unop Z))ᵒᵖ ⥤ A)
          (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (J.over (unop Z)))
            (Functor.obj (J.overPullback A (unop Z)) F))
          (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (J.over (unop Z)))
            (Functor.obj (J.overPullback A (unop Z)) G)))
      (InducedCategory.Hom.hom
          (TypeCat.Fun.toFun
            (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (CategoryStruct.comp (Y :=
                Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop Y)) (J.over (unop Y)) A)
                  (Functor.obj (J.overPullback A (unop Y)) F) (Functor.obj (J.overPullback A (unop Y)) G))
                (↾Functor.map (J.overMapPullback A f.unop) :
                  Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop X)) (J.over (unop X)) A)
                      (Functor.obj (J.overPullback A (unop X)) F) (Functor.obj (J.overPullback A (unop X)) G) ⟶
                    Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop Y)) (J.over (unop Y)) A)
                      (Functor.obj (J.overPullback A (unop Y)) F) (Functor.obj (J.overPullback A (unop Y)) G))
                (↾Functor.map (J.overMapPullback A g.unop) :
                  Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop Y)) (J.over (unop Y)) A)
                      (Functor.obj (J.overPullback A (unop Y)) F) (Functor.obj (J.overPullback A (unop Y)) G) ⟶
                    Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop Z)) (J.over (unop Z)) A)
                      (Functor.obj (J.overPullback A (unop Z)) F) (Functor.obj (J.overPullback A (unop Z)) G))))
            φ) :
        Quiver.Hom (V := (Over.{v, u} (unop Z))ᵒᵖ ⥤ A)
          (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (J.over (unop Z)))
            (Functor.obj (J.overPullback A (unop Z)) F))
          (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (J.over (unop Z)))
            (Functor.obj (J.overPullback A (unop Z)) G)))
⊢ Eq (α :=
    Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop X)) (J.over (unop X)) A) (Functor.obj (J.overPullback A (unop X)) F)
        (Functor.obj (J.overPullback A (unop X)) G) ⟶
      Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop Z)) (J.over (unop Z)) A)
        (Functor.obj (J.overPullback A (unop Z)) F) (Functor.obj (J.overPullback A (unop Z)) G))
    (↾Functor.map (J.overMapPullback A (f ≫ g).unop) :
      Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop X)) (J.over (unop X)) A)
          (Functor.obj (J.overPullback A (unop X)) F) (Functor.obj (J.overPullback A (unop X)) G) ⟶
        Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop Z)) (J.over (unop Z)) A)
          (Functor.obj (J.overPullback A (unop Z)) F) (Functor.obj (J.overPullback A (unop Z)) G))
    (CategoryStruct.comp (Y :=
        Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop Y)) (J.over (unop Y)) A)
          (Functor.obj (J.overPullback A (unop Y)) F) (Functor.obj (J.overPullback A (unop Y)) G))
        (↾Functor.map (J.overMapPullback A f.unop) :
          Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop X)) (J.over (unop X)) A)
              (Functor.obj (J.overPullback A (unop X)) F) (Functor.obj (J.overPullback A (unop X)) G) ⟶
            Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop Y)) (J.over (unop Y)) A)
              (Functor.obj (J.overPullback A (unop Y)) F) (Functor.obj (J.overPullback A (unop Y)) G))
        (↾Functor.map (J.overMapPullback A g.unop) :
          Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop Y)) (J.over (unop Y)) A)
              (Functor.obj (J.overPullback A (unop Y)) F) (Functor.obj (J.overPullback A (unop Y)) G) ⟶
            Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop Z)) (J.over (unop Z)) A)
              (Functor.obj (J.overPullback A (unop Z)) F) (Functor.obj (J.overPullback A (unop Z)) G)) :
      Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop X)) (J.over (unop X)) A)
          (Functor.obj (J.overPullback A (unop X)) F) (Functor.obj (J.overPullback A (unop X)) G) ⟶
        Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop Z)) (J.over (unop Z)) A)
          (Functor.obj (J.overPullback A (unop Z)) F) (Functor.obj (J.overPullback A (unop Z)) G))

Tactic:
ext φ : 4