-- 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 : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible (R := S.arrows)
g : Y ⟶ X
Z₁ : Over.{v, u} Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over.{v, u} Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
H :
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Over.Hom.left f).op) :
        (a : (Over.forget Z₁.left).op ⋙ F ⟶ (Over.forget Z₁.left).op ⋙ G) →
          (Over.forget Z₂.left).op ⋙ F ⟶ (Over.forget Z₂.left).op ⋙ G)
      (x (Z₁.hom ≫ g) hZ₁) =
    x (Z₂.hom ≫ g) hZ₂
φ : Over.mk (Over.Hom.left f) ⟶ Over.mk (𝟙 Z₁.left) := Over.homMk (Over.Hom.left f) ⋯
H' :
  F.map (Over.Hom.left φ).op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left φ).op
erw :
  F.map Z₂.hom.op ≫
      NatTrans.app
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Over.Hom.left f).op) :
            (a : (Over.forget Z₁.left).op ⋙ F ⟶ (Over.forget Z₁.left).op ⋙ G) →
              (Over.forget Z₂.left).op ⋙ F ⟶ (Over.forget Z₂.left).op ⋙ G)
          (x (Z₁.hom ≫ g) hZ₁))
        (op (Over.mk (𝟙 Z₂.left))) =
    F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left f).op
erw₁ :
  F.map Z₂.hom.op ≫
      NatTrans.app
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Over.Hom.left f).op) :
            (a : (Over.forget Z₁.left).op ⋙ F ⟶ (Over.forget Z₁.left).op ⋙ G) →
              (Over.forget Z₂.left).op ⋙ F ⟶ (Over.forget Z₂.left).op ⋙ G)
          (x (Z₁.hom ≫ g) hZ₁))
        (op (Over.mk (𝟙 Z₂.left))) =
    F.map Z₁.hom.op ≫ F.map (Over.Hom.left φ).op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f)))
erw₂ :
  F.map Z₂.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    F.map Z₁.hom.op ≫ F.map (Over.Hom.left φ).op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f)))
erw₃ :
  F.map Z₂.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    F.map (Z₁.hom.op ≫ (Over.Hom.left φ).op) ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f)))
erw₄ :
  F.map Z₂.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    F.map (Over.Hom.left φ ≫ Z₁.hom).op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f)))
erw₅ erw₆ :
  F.map Z₂.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    F.map Z₂.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f)))
⊢ F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
    F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left f).op

Tactic:
erw [← H, ← H', presheafHom_map_app_op_mk_id, ← F.map_comp_assoc,
              ← op_comp, Over.w f]

Premises used: CategoryTheory.op_comp, CategoryTheory.Over.w, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.presheafHom_map_app_op_mk_id