-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafHom (goal)
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
⊢ 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))
have 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)))
Tactic: ext φ : 4