-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over.{v₁, u₁} B')ᵒᵖ ⥤ Type w
X : Over.{v₁, u₁} B
Y : I → Over.{v₁, u₁} B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over.{v₁, u₁} B'
g₁ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun (i : I) ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
this :
  Eq (α :=
    (fun (X : Type w) ↦ X) (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((Over.map p).op ⋙ P).map (Over.homMk (Over.Hom.left g₁) ⋯).op) :
          (a : (fun (X : Type w) ↦ X) (((Over.map p).op ⋙ P).obj (op (Y i₁)))) →
            (fun (X : Type w) ↦ X)
              (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
        ((↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i₁) :
      (fun (X : Type w) ↦ X)
        (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((Over.map p).op ⋙ P).map (Over.homMk (Over.Hom.left g₂) ⋯).op) :
          (a : (fun (X : Type w) ↦ X) (((Over.map p).op ⋙ P).obj (op (Y i₂)))) →
            (fun (X : Type w) ↦ X)
              (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
        ((↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i₂) :
      (fun (X : Type w) ↦ X)
        (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
φ : Z ⟶ (Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)) := Over.homMk (𝟙 Z.left) ⋯
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map φ.op) :
          (a :
              (fun (X : Type w) ↦ X)
                (P.obj (op ((Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))) →
            (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (((Over.map p).op ⋙ P).map (Over.homMk (Over.Hom.left g₁) ⋯).op) :
              (a : (fun (X : Type w) ↦ X) (((Over.map p).op ⋙ P).obj (op (Y i₁)))) →
                (fun (X : Type w) ↦ X)
                  (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
            ((↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i₁) :
          (fun (X : Type w) ↦ X)
            (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom))))) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map φ.op) :
          (a :
              (fun (X : Type w) ↦ X)
                (P.obj (op ((Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))) →
            (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (((Over.map p).op ⋙ P).map (Over.homMk (Over.Hom.left g₂) ⋯).op) :
              (a : (fun (X : Type w) ↦ X) (((Over.map p).op ⋙ P).obj (op (Y i₂)))) →
                (fun (X : Type w) ↦ X)
                  (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)))))
            ((↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i₂) :
          (fun (X : Type w) ↦ X)
            (((Over.map p).op ⋙ P).obj (op (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom))))) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))

Tactic:
replace this := congr_arg (P.map φ.op) this