-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (hypothesis)
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 g₁.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op ((fun (i : I) ↦ (Over.map p).obj (Y i)) i₁)))) →
            (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((fun (i : I) ↦ (↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i) i₁) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op ((fun (i : I) ↦ (Over.map p).obj (Y i)) i₂)))) →
            (fun (X : Type w) ↦ X) (P.obj (op Z)))
        ((fun (i : I) ↦ (↑s : (i : I) → ((Over.map p).op ⋙ P).obj (op (Y i))) i) i₂) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
have this₁ : 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₁) sorry).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₂) sorry).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
Cleared hypotheses: this