-- 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
φ :
  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)))

Tactic:
ConcreteCategory.congr_hom ((presheafHom F.1 G.1).map_comp f g) φ.1

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerLeft, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.presheafHom, CategoryTheory.Functor.map_comp, CategoryTheory.ConcreteCategory.congr_hom